Improve and extend mechanism for extracting relevant information for …

…executable checking (#713) * revise information extraction for executable checking - move that logic to new module - tidy up the extraction types and code - record relevant information for loop invariants * ocamlformat * ocamlformat specTests.ml * ocamlformat specTests.ml
rems-project · Nov 12, 2024 · a6430b4 · a6430b4
1 parent dfe01d6
commit a6430b4
Show file tree

Hide file tree

Showing 22 changed files with 268 additions and 231 deletions.
diff --git a/backend/cn/bin/main.ml b/backend/cn/bin/main.ml
@@ -477,9 +477,9 @@ let run_tests
         (fun () ->
           if
             prog5
-            |> Core_to_mucore.collect_instrumentation
+            |> Executable_spec_extract.collect_instrumentation
             |> fst
-            |> List.filter (fun (inst : Core_to_mucore.instrumentation) ->
+            |> List.filter (fun (inst : Executable_spec_extract.instrumentation) ->
               Option.is_some inst.internal)
             |> List.is_empty
           then (

diff --git a/backend/cn/lib/check.ml b/backend/cn/lib/check.ml
@@ -2162,7 +2162,7 @@ let check_procedure
            pure
              (match def with
               | Mu.Return _loc -> return ()
-              | Label (loc, label_args_and_body, _annots, _) ->
+              | Label (loc, label_args_and_body, _annots, _, _loop_info) ->
                 debug
                   2
                   (lazy

diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml
@@ -6,6 +6,7 @@ module CF = Cerb_frontend
 open CF.Cn
 open Compile
 open Executable_spec_utils
+module ESE = Executable_spec_extract
 module A = CF.AilSyntax
 module C = CF.Ctype
 module BT = BaseTypes
@@ -3135,9 +3136,7 @@ let rec cn_to_ail_post_aux_internal dts globals preds = function
   | LRT.Define ((name, it), (_loc, _), t) ->
     (* Printf.printf "LRT.Define\n"; *)
     let new_name = generate_sym_with_suffix ~suffix:"_cn" name in
-    let new_lrt =
-      Core_to_mucore.fn_spec_instrumentation_sym_subst_lrt (name, IT.bt it, new_name) t
-    in
+    let new_lrt = LogicalReturnTypes.subst (ESE.sym_subst (name, IT.bt it, new_name)) t in
     let binding = create_binding new_name (bt_to_ail_ctype (IT.bt it)) in
     let decl = A.(AilSdeclaration [ (new_name, None) ]) in
     let b1, s1 = cn_to_ail_expr_internal dts globals it (AssignVar new_name) in
@@ -3150,9 +3149,7 @@ let rec cn_to_ail_post_aux_internal dts globals preds = function
     let b1, s1 =
       cn_to_ail_resource_internal ~is_pre:false new_name dts globals preds loc re
     in
-    let new_lrt =
-      Core_to_mucore.fn_spec_instrumentation_sym_subst_lrt (name, bt, new_name) t
-    in
+    let new_lrt = LogicalReturnTypes.subst (ESE.sym_subst (name, bt, new_name)) t in
     let b2, s2 = cn_to_ail_post_aux_internal dts globals preds new_lrt in
     (b1 @ b2, upd_s @ s1 @ pop_s @ s2)
   | LRT.Constraint (lc, (loc, _str_opt), t) ->
@@ -3276,7 +3273,7 @@ let rec cn_to_ail_lat_internal_2
     let ctype = bt_to_ail_ctype (IT.bt it) in
     let new_name = generate_sym_with_suffix ~suffix:"_cn" name in
     let new_lat =
-      Core_to_mucore.fn_spec_instrumentation_sym_subst_lat (name, IT.bt it, new_name) lat
+      ESE.fn_largs_and_body_subst (ESE.sym_subst (name, IT.bt it, new_name)) lat
     in
     (* let ctype = mk_ctype C.(Pointer (empty_qualifiers, ctype)) in *)
     let binding = create_binding new_name ctype in
@@ -3299,9 +3296,7 @@ let rec cn_to_ail_lat_internal_2
     let b1, s1 =
       cn_to_ail_resource_internal ~is_pre:true new_name dts globals preds loc ret
     in
-    let new_lat =
-      Core_to_mucore.fn_spec_instrumentation_sym_subst_lat (name, bt, new_name) lat
-    in
+    let new_lat = ESE.fn_largs_and_body_subst (ESE.sym_subst (name, bt, new_name)) lat in
     let ail_executable_spec =
       cn_to_ail_lat_internal_2
         without_ownership_checking
@@ -3328,7 +3323,8 @@ let rec cn_to_ail_lat_internal_2
     in
     prepend_to_precondition ail_executable_spec (b1, ss)
   (* Postcondition *)
-  | LAT.I (post, stats) ->
+  | LAT.I (post, (stats, _loop)) ->
+    (*TODO: handle loops *)
     let rec remove_duplicates locs stats =
       match stats with
       | [] -> []
@@ -3405,9 +3401,7 @@ let rec cn_to_ail_pre_post_aux_internal
     let binding = create_binding cn_sym cn_ctype in
     let rhs = wrap_with_convert_to A.(AilEident sym) bt in
     let decl = A.(AilSdeclaration [ (cn_sym, Some (mk_expr rhs)) ]) in
-    let subst_at =
-      Core_to_mucore.fn_spec_instrumentation_sym_subst_at (sym, bt, cn_sym) at
-    in
+    let subst_at = ESE.fn_args_and_body_subst (ESE.sym_subst (sym, bt, cn_sym)) at in
     let ail_executable_spec =
       cn_to_ail_pre_post_aux_internal
         without_ownership_checking

diff --git a/backend/cn/lib/cn_internal_to_ail.mli b/backend/cn/lib/cn_internal_to_ail.mli
@@ -172,7 +172,7 @@ val cn_to_ail_pre_post_internal
   (Sym.t * ResourcePredicates.definition) list ->
   (Sym.t * C.ctype) list ->
   C.ctype ->
-  Core_to_mucore.fn_spec_instrumentation option ->
+  Executable_spec_extract.fn_args_and_body option ->
   ail_executable_spec
 
 val cn_to_ail_assume_predicates_internal

diff --git a/backend/cn/lib/core_to_mucore.ml b/backend/cn/lib/core_to_mucore.ml
@@ -1139,9 +1139,9 @@ let normalise_label
   | Mi_Label (loc, lt, label_args, label_body, annots) ->
     (match CF.Annot.get_label_annot annots with
      | Some (LAloop loop_id) ->
-       let@ desugared_inv, cn_desugaring_state =
+       let@ desugared_inv, cn_desugaring_state, loop_condition_loc =
          match Pmap.lookup loop_id loop_attributes with
-         | Some (marker_id, attrs) ->
+         | Some (marker_id, attrs, loop_condition_loc) ->
            let@ inv = Parse.loop_spec attrs in
            let d_st =
              CAE.
@@ -1153,8 +1153,9 @@ let normalise_label
                }
            in
            let@ inv, d_st = desugar_conds d_st inv in
-           return (inv, d_st.inner.cn_state)
-         | None -> return ([], precondition_cn_desugaring_state)
+           return (inv, d_st.inner.cn_state, loop_condition_loc)
+         | None -> assert false
+         (* return ([], precondition_cn_desugaring_state) *)
        in
        debug 6 (lazy (!^"invariant in function" ^^^ Sym.pp fsym));
        debug 6 (lazy (CF.Pp_ast.pp_doc_tree (dtree_of_inv desugared_inv)));
@@ -1179,7 +1180,12 @@ let normalise_label
        (*     ) label_args_and_body  *)
        (* in *)
        return
-         (Mu.Label (loc, label_args_and_body, annots, { label_spec = desugared_inv }))
+         (Mu.Label
+            ( loc,
+              label_args_and_body,
+              annots,
+              { label_spec = desugared_inv },
+              `Loop loop_condition_loc ))
      (* | Some (LAloop_body _loop_id) -> *)
      (*    assert_error loc !^"body label has not been inlined" *)
      | Some (LAloop_continue _loop_id) ->
@@ -1591,137 +1597,3 @@ let normalise_file ~inherit_loc ((fin_markers_env : CAE.fin_markers_env), ail_pr
   in
   debug 3 (lazy (headline "done core_to_mucore normalising file"));
   return file
-
-
-(* type internal = { pre: unit arguments; post: ReturnTypes.t; inv: (Loc.t * unit
-   arguments); statements: (Locations.t * Cnprog.cn_prog list) list; } *)
-
-type statements = (Locations.t * Cnprog.t list) list
-
-type fn_spec_instrumentation = (ReturnTypes.t * statements) ArgumentTypes.t
-
-type instrumentation =
-  { fn : Sym.t;
-    fn_loc : Locations.t;
-    internal : fn_spec_instrumentation option
-  }
-
-let rt_stmts_subst subst (rt, stmts) =
-  let rt = ReturnTypes.subst subst rt in
-  let stmts =
-    List.map (fun (loc, cn_progs) -> (loc, List.map (Cnprog.subst subst) cn_progs)) stmts
-  in
-  (rt, stmts)
-
-
-let fn_spec_instrumentation_subst_at
-  : _ Subst.t -> fn_spec_instrumentation -> fn_spec_instrumentation
-  =
-  ArgumentTypes.subst rt_stmts_subst
-
-
-let fn_spec_instrumentation_subst_lat
-  :  _ Subst.t -> (ReturnTypes.t * statements) LogicalArgumentTypes.t ->
-  (ReturnTypes.t * statements) LogicalArgumentTypes.t
-  =
-  LogicalArgumentTypes.subst rt_stmts_subst
-
-
-(* substitute `s_with` for `s_replace` of basetype `bt` *)
-let fn_spec_instrumentation_sym_subst_at (s_replace, bt, s_with) fn_spec =
-  let subst =
-    IT.make_subst [ (s_replace, IT.sym_ (s_with, bt, Cerb_location.unknown)) ]
-  in
-  fn_spec_instrumentation_subst_at subst fn_spec
-
-
-let fn_spec_instrumentation_sym_subst_lat (s_replace, bt, s_with) fn_spec =
-  let subst =
-    IT.make_subst [ (s_replace, IT.sym_ (s_with, bt, Cerb_location.unknown)) ]
-  in
-  fn_spec_instrumentation_subst_lat subst fn_spec
-
-
-let fn_spec_instrumentation_sym_subst_lrt (s_replace, bt, s_with) fn_spec =
-  let subst =
-    IT.make_subst [ (s_replace, IT.sym_ (s_with, bt, Cerb_location.unknown)) ]
-  in
-  LRT.subst subst fn_spec
-
-
-let concat2 (x : 'a list * 'b list) (y : 'a list * 'b list) : 'a list * 'b list =
-  let a1, b1 = x in
-  let a2, b2 = y in
-  (a1 @ a2, b1 @ b2)
-
-
-let concat2_map (f : 'a -> 'b list * 'c list) (xs : 'a list) : 'b list * 'c list =
-  List.fold_right (fun x acc -> concat2 (f x) acc) xs ([], [])
-
-
-let rec stmts_in_expr (Mu.Expr (loc, _, _, e_)) =
-  match e_ with
-  | Epure _ -> ([], [])
-  | Ememop _ -> ([], [])
-  | Eaction _ -> ([], [])
-  | Eskip -> ([], [])
-  | Eccall _ -> ([], [])
-  | Elet (_, _, e) -> stmts_in_expr e
-  | Eunseq es -> concat2_map stmts_in_expr es
-  | Ewseq (_, e1, e2) -> concat2 (stmts_in_expr e1) (stmts_in_expr e2)
-  | Esseq (_, e1, e2) -> concat2 (stmts_in_expr e1) (stmts_in_expr e2)
-  | Eif (_, e1, e2) -> concat2 (stmts_in_expr e1) (stmts_in_expr e2)
-  | Ebound e -> stmts_in_expr e
-  | End es -> concat2_map stmts_in_expr es
-  | Erun _ -> ([], [])
-  | CN_progs (stmts_s, stmts_i) -> ([ (loc, stmts_s) ], [ (loc, stmts_i) ])
-
-
-let rec stmts_in_largs f_i = function
-  | Mu.Define (_, _, a) -> stmts_in_largs f_i a
-  | Resource (_, _, a) -> stmts_in_largs f_i a
-  | Constraint (_, _, a) -> stmts_in_largs f_i a
-  | I i -> f_i i
-
-
-let rec stmts_in_args f_i = function
-  | Mu.Computational (_, _, a) -> stmts_in_args f_i a
-  | L a -> stmts_in_largs f_i a
-
-
-let stmts_in_labels labels =
-  Pmap.fold
-    (fun _s def acc ->
-      match def with
-      | Mu.Return _ -> acc
-      | Label (_, a, _, _) -> concat2 (stmts_in_args stmts_in_expr a) acc)
-    labels
-    ([], [])
-
-
-(*
- * let stmts_in_function args_and_body =
- *   stmts_in_args
- *     (fun (body, labels, _rt) -> concat2 (stmts_in_expr body) (stmts_in_labels labels))
- *     args_and_body
- *)
-
-let collect_instrumentation (file : _ Mu.file) =
-  let instrs =
-    List.map
-      (fun (fn, decl) ->
-        match decl with
-        | Mu.Proc { loc = fn_loc; args_and_body; _ } ->
-          let args_and_body = at_of_arguments Fun.id args_and_body in
-          let internal =
-            ArgumentTypes.map
-              (fun (body, labels, rt) ->
-                let _, stmts = concat2 (stmts_in_expr body) (stmts_in_labels labels) in
-                (rt, stmts))
-              args_and_body
-          in
-          { fn; fn_loc; internal = Some internal }
-        | ProcDecl (fn_loc, _fn) -> { fn; fn_loc; internal = None })
-      (Pmap.bindings_list file.funs)
-  in
-  (instrs, C.symtable)
diff --git a/backend/cn/lib/core_to_mucore.mli b/backend/cn/lib/core_to_mucore.mli
@@ -7,34 +7,6 @@ val normalise_file
   ('b, unit) Cerb_frontend.Milicore.mi_file ->
   unit Mucore.file Resultat.m
 
-(* TODO(RB) - Do these belong here? Looks like they can/should be factored out *)
-type statements = (Locations.t * Cnprog.t list) list
-
-type fn_spec_instrumentation = (ReturnTypes.t * statements) ArgumentTypes.t
-
 val arguments_of_at : ('a -> 'b) -> 'a ArgumentTypes.t -> 'b Mucore.arguments
 
-val fn_spec_instrumentation_sym_subst_lrt
-  :  Sym.t * BaseTypes.t * Sym.t ->
-  LogicalReturnTypes.t ->
-  LogicalReturnTypes.t
-
-val fn_spec_instrumentation_sym_subst_lat
-  :  Sym.t * BaseTypes.t * Sym.t ->
-  (ReturnTypes.t * statements) LogicalArgumentTypes.t ->
-  (ReturnTypes.t * statements) LogicalArgumentTypes.t
-
-val fn_spec_instrumentation_sym_subst_at
-  :  Sym.t * BaseTypes.t * Sym.t ->
-  fn_spec_instrumentation ->
-  fn_spec_instrumentation
-
-type instrumentation =
-  { fn : Sym.t;
-    fn_loc : Locations.t;
-    internal : fn_spec_instrumentation option
-  }
-
-val collect_instrumentation
-  :  'a Mucore.file ->
-  instrumentation list * BaseTypes.Surface.t Hashtbl.Make(Sym).t
+val at_of_arguments : ('b -> 'a) -> 'b Mucore.arguments -> 'a ArgumentTypes.t
diff --git a/backend/cn/lib/executable_spec.ml b/backend/cn/lib/executable_spec.ml
@@ -213,7 +213,9 @@ let main
   let oc = Stdlib.open_out (Filename.concat prefix output_filename) in
   let cn_oc = Stdlib.open_out (Filename.concat prefix "cn.c") in
   let cn_header_oc = Stdlib.open_out (Filename.concat prefix "cn.h") in
-  let instrumentation, symbol_table = Core_to_mucore.collect_instrumentation prog5 in
+  let instrumentation, symbol_table =
+    Executable_spec_extract.collect_instrumentation prog5
+  in
   Executable_spec_records.populate_record_map instrumentation prog5;
   let executable_spec =
     generate_c_specs_internal