Add naive handling of Return for Kani C WPST

kanillian/lib/compiler/compile.ml

@@ -144,7 +144,7 @@ let set_global_env_proc (ctx : Ctx.t) =
       proc_calls = [];
     }
 
-let compile_free_locals (ctx : Ctx.t) =
+let compile_free_locals ~cmd_kind (ctx : Ctx.t) =
   let open Kutils.Prelude in
   let locals = Hashtbl.copy ctx.locals in
   let () =
@@ -156,7 +156,7 @@ let compile_free_locals (ctx : Ctx.t) =
       locals
   in
   Hashtbl.to_seq_values locals
-  |> Seq.map (Memory.dealloc_local ~ctx ~cmd_kind:(Normal false))
+  |> Seq.map (Memory.dealloc_local ~ctx ~cmd_kind)
   |> List.of_seq
 
 let compile_alloc_params ~ctx params =
@@ -257,16 +257,19 @@ let compile_function ?map_body ~ctx (func : Program.Func.t) :
       func.params
   in
   let proc_spec = None in
-  let free_locals = compile_free_locals ctx in
+  let free_locals = compile_free_locals ~cmd_kind:Hidden ctx in
   (* We add a return undef in case the function has no return *)
-  let b = Body_item.make_hloc ~loc:func.location ~cmd_kind:(Normal false) in
+  let b ?(cmd_kind = K_annot.Hidden) =
+    Body_item.make_hloc ~loc:func.location ~cmd_kind
+  in
   let return_undef =
     b (Assignment (Kutils.Names.return_variable, Lit Undefined))
   in
   let return_block =
-    set_first_label ~annot:(b ~loop:[] ?tl_ref:None)
+    set_first_label
+      ~annot:(b ~loop:[] ?tl_ref:None ?cmd_kind:None)
       Constants.Kanillian_names.ret_label
-      (free_locals @ [ b ReturnNormal ])
+      (free_locals @ [ b ~cmd_kind:Return ReturnNormal ])
   in
   let alloc_params = compile_alloc_params ~ctx proc_params |> List.map b in
   let _, comp_body = compile_statement ~ctx body in

kanillian/lib/compiler/k_annot.ml

@@ -8,6 +8,7 @@ type cmd_kind =
   | Hidden  (** Hidden commands, e.g. the =skip= at the end of an if/else *)
   | Normal of bool  (** Is this the final GIL cmd for the C stmt/expr? *)
   | Func_call of { is_internal : bool; is_end : bool }
+  | Return
   | Unknown
 [@@deriving yojson, eq, show]
 

kanillian/lib/lifter/kani_c_lifter.ml

@@ -156,6 +156,7 @@ struct
         | Internal | Hidden -> Ok false
         | Harness as k ->
             Fmt.error "%a cmd should have been skipped!" Annot.pp_cmd_kind k
+        | Return -> Ok true
         | Unknown -> Error "HORROR - unknown cmd kind"
 
       let resolve_case
@@ -177,7 +178,8 @@ struct
         let ({ id; kind; _ } : exec_data) = exec_data in
         let { ends; unexplored_paths; _ } = partial in
         match (kind, is_end) with
-        | Final, _ | Normal, false ->
+        | Final, _ -> Ok ()
+        | Normal, false ->
             Stack.push (id, None) unexplored_paths;
             Ok ()
         | Branch cases, false ->
@@ -196,11 +198,21 @@ struct
                    in
                    Ext_list.add (case, (id, Some gil_case)) ends)
 
+      let update_return_cmd_info ~id (partial : partial_data) =
+        partial.id <- Some id;
+        partial.display <- Some "<end of func>";
+        Ok ()
+
       let update_canonical_cmd_info
           ~id
           ~(tl_ast : tl_ast)
           ~(annot : Annot.t)
           (partial : partial_data) =
+        let- () =
+          match annot.cmd_kind with
+          | Return -> Some (update_return_cmd_info ~id partial)
+          | _ -> None
+        in
         match (annot.cmd_kind, partial.display, annot.tl_ref) with
         | (Harness | Unknown), _, _ ->
             Fmt.error "HORROR - trying to get display of %a" Annot.pp_cmd_kind
@@ -441,7 +453,7 @@ struct
           in
           DL.failwith json "Kani_c_lifter: Encountered unknown cmd kind"
       | Harness -> ExecNext (None, None)
-      | Normal _ | Func_call _ | Internal | Hidden -> (
+      | Normal _ | Func_call _ | Internal | Return | Hidden -> (
           let get_prev = get_prev ~state ~gil_case ~prev_id in
           let partial_result =
             Partial_cmds.handle ~get_prev ~tl_ast ~partials ~prev_id exec_data