Instrument after pre-processor

Author: yav

.github/workflows/proof.yml

@@ -22,7 +22,7 @@ jobs:
         # version: [4.12.0, 4.14.1]
         version: [4.14.1]
 
-    runs-on: ubuntu-22.04
+    runs-on: ubuntu-latest
 
     steps:
 
@@ -46,7 +46,7 @@ jobs:
         opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }}
         eval $(opam env --switch=${{ matrix.version }})
         opam repo add --yes --this-switch coq-released https://coq.inria.fr/opam/released
-        opam install --deps-only --yes ./cn.opam
+        opam install --deps-only --yes ./cn.opam z3
 
     - name: Save OPAM cache
       uses: actions/cache/save@v4

.github/workflows/spec-testing.yml

@@ -46,7 +46,7 @@ jobs:
         opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }}
         eval $(opam env --switch=${{ matrix.version }})
         opam repo add --yes --this-switch coq-released https://coq.inria.fr/opam/released
-        opam install --deps-only --yes ./cn.opam
+        opam install --deps-only --yes ./cn.opam z3
 
     - name: Save OPAM cache
       uses: actions/cache/save@v4

bin/instrument.ml

@@ -2,16 +2,10 @@ module CF = Cerb_frontend
 module CB = Cerb_backend
 open Cn
 
-let pick_cpp_file_name outdir filename =
-  let cpp_name = Filename.remove_extension filename ^ "-preproc.c" in
-  match outdir with None -> cpp_name | Some d -> Filename.concat d cpp_name
-
-
 let run_instrumented_file ~filename ~output ~output_dir ~print_steps =
   let instrumented_filename =
     Option.value ~default:(Fulminate.get_instrumented_filename filename) output
   in
-  let cn_helper_filename = Fulminate.get_cn_helper_filename filename in
   let output_dir = Option.value ~default:"." output_dir in
   let in_folder ?ext fn =
     Filename.concat
@@ -25,21 +19,6 @@ let run_instrumented_file ~filename ~output ~output_dir ~print_steps =
     print_endline
       ("Could not find CN's runtime directory (looked at: '" ^ runtime_prefix ^ "')");
     exit 1);
-  if
-    Sys.command
-      ("cc -c "
-       ^ includes
-       ^ " -o "
-       ^ in_folder ~ext:".o" cn_helper_filename
-       ^ " "
-       ^ in_folder cn_helper_filename)
-    == 0
-  then (
-    if print_steps then
-      print_endline ("Compiled '" ^ cn_helper_filename ^ "'"))
-  else (
-    print_endline ("Failed to compile '" ^ cn_helper_filename ^ "'");
-    exit 1);
   if
     Sys.command
       ("cc -c "
@@ -64,8 +43,6 @@ let run_instrumented_file ~filename ~output ~output_dir ~print_steps =
        ^ " "
        ^ in_folder ~ext:".o" instrumented_filename
        ^ " "
-       ^ in_folder ~ext:".o" cn_helper_filename
-       ^ " "
        ^ Filename.concat runtime_prefix "libcn_exec.a")
     == 0
   then (
@@ -105,7 +82,6 @@ let generate_executable_specs
       without_loop_invariants
       with_loop_leak_checks
       with_test_gen
-      copy_source_dir
       run
       print_steps
   =
@@ -126,16 +102,10 @@ let generate_executable_specs
     Pp.error e.loc report.short (Option.to_list report.descr);
     match e.msg with TypeErrors.Unsupported _ -> exit 2 | _ -> exit 1
   in
-  (* XXX temporary: should we inject in the pre-processed file or original one *)
   let filename = Common.there_can_only_be_one filename in
-  let use_preproc = false in
-  let exec_spec_file, save =
-    if use_preproc then (
-      let pp_file = pick_cpp_file_name output_dir filename in
-      (pp_file, Some pp_file))
-    else
-      (filename, None)
-  in
+  let basefile = Filename.basename filename in
+  let pp_file = Filename.temp_file "cn_" basefile in
+  let out_file = Fulminate.get_output_filename output_dir output basefile in
   Common.with_well_formedness_check (* CLI arguments *)
     ~filename
     ~macros
@@ -150,7 +120,7 @@ let generate_executable_specs
     ~astprints
     ~no_inherit_loc
     ~magic_comment_char_dollar (* Callbacks *)
-    ~save_cpp:save
+    ~save_cpp:(Some pp_file)
     ~handle_error
     ~f:(fun ~cabs_tunit:_ ~prog5 ~ail_prog ~statement_locs:_ ~paused:_ ->
       Cerb_colour.without_colour
@@ -161,12 +131,9 @@ let generate_executable_specs
                 ~without_loop_invariants
                 ~with_loop_leak_checks
                 ~with_test_gen
-                ~copy_source_dir
-                exec_spec_file
-                ~use_preproc
+                pp_file
+                out_file
                 ail_prog
-                output
-                output_dir
                 prog5
             with
             | e -> Common.handle_error_with_user_guidance ~label:"CN-Exec" e);
@@ -224,11 +191,6 @@ module Flags = struct
     Arg.(value & flag & info [ "with-test-gen" ] ~doc)
 
 
-  let copy_source_dir =
-    let doc = "Copy non-CN annotated files into output_dir for CN runtime testing" in
-    Arg.(value & flag & info [ "copy-source-dir" ] ~doc)
-
-
   let run =
     let doc = "Run the instrumented program" in
     Arg.(value & flag & info [ "run" ] ~doc)
@@ -281,7 +243,6 @@ let cmd =
     $ Flags.without_loop_invariants
     $ Flags.with_loop_leak_checks
     $ Flags.with_test_gen
-    $ Flags.copy_source_dir
     $ Flags.run
     $ Flags.print_steps
   in

bin/seqTest.ml

@@ -36,6 +36,13 @@ let run_seq_tests
     match e.msg with TypeErrors.Unsupported _ -> exit 2 | _ -> exit 1
   in
   let filename = Common.there_can_only_be_one filename in
+  let basefile = Filename.basename filename in
+  let pp_file = Filename.temp_file "cn_" basefile in
+  let output_dir =
+    let dir, mk = output_dir in
+    mk dir
+  in
+  let out_file = Fulminate.get_output_filename (Some output_dir) None basefile in
   Common.with_well_formedness_check (* CLI arguments *)
     ~filename
     ~macros
@@ -50,7 +57,7 @@ let run_seq_tests
     ~astprints
     ~no_inherit_loc
     ~magic_comment_char_dollar (* Callbacks *)
-    ~save_cpp:None (* XXX *)
+    ~save_cpp:(Some pp_file)
     ~handle_error
     ~f:(fun ~cabs_tunit ~prog5 ~ail_prog ~statement_locs:_ ~paused:_ ->
       Cerb_colour.without_colour
@@ -67,22 +74,15 @@ let run_seq_tests
              print_endline "No testable functions, trivially passing";
              exit 0);
            let _, sigma = ail_prog in
-           let output_dir =
-             let dir, mk = output_dir in
-             mk dir
-           in
            Fulminate.Cn_to_ail.augment_record_map (BaseTypes.Record []);
            Fulminate.main
              ~without_ownership_checking
              ~without_loop_invariants:true
              ~with_loop_leak_checks:false
              ~with_test_gen:true
-             ~copy_source_dir:false
-             filename
-             ~use_preproc:false
+             pp_file
+             out_file
              ail_prog
-             None
-             (Some output_dir)
              prog5;
            let config : SeqTests.seq_config =
              { print_steps;

bin/test.ml

@@ -65,6 +65,13 @@ let run_tests
     match e.msg with TypeErrors.Unsupported _ -> exit 2 | _ -> exit 1
   in
   let filename = Common.there_can_only_be_one filename in
+  let basefile = Filename.basename filename in
+  let output_dir =
+    let dir, mk = output_dir in
+    mk dir
+  in
+  let pp_file = Filename.temp_file "cn_" basefile in
+  let out_file = Fulminate.get_output_filename (Some output_dir) None basefile in
   Common.with_well_formedness_check (* CLI arguments *)
     ~filename
     ~macros
@@ -79,7 +86,7 @@ let run_tests
     ~astprints
     ~no_inherit_loc
     ~magic_comment_char_dollar (* Callbacks *)
-    ~save_cpp:None (* XXX *)
+    ~save_cpp:(Some pp_file)
     ~handle_error
     ~f:(fun ~cabs_tunit ~prog5 ~ail_prog ~statement_locs:_ ~paused:_ ->
       let config : TestGeneration.config =
@@ -125,23 +132,16 @@ let run_tests
         exit 0);
       Cerb_colour.without_colour
         (fun () ->
-           let output_dir =
-             let dir, mk = output_dir in
-             mk dir
-           in
            Fulminate.Cn_to_ail.augment_record_map (BaseTypes.Record []);
            (try
               Fulminate.main
                 ~without_ownership_checking
                 ~without_loop_invariants:true
                 ~with_loop_leak_checks:false
                 ~with_test_gen:true
-                ~copy_source_dir:false
-                filename
-                ~use_preproc:false (* XXX *)
+                pp_file
+                out_file
                 ail_prog
-                None
-                (Some output_dir)
                 prog5
             with
             | e -> Common.handle_error_with_user_guidance ~label:"CN-Exec" e);

lib/fulminate/cn_to_ail.ml

@@ -100,6 +100,8 @@ let create_id_from_sym ?(lowercase = false) sym =
 
 let create_sym_from_id id = Sym.fresh (Id.get_string id)
 
+let ail_null = A.(AilEconst (ConstantInteger (IConstant (Z.zero, Decimal, None))))
+
 let generate_error_msg_info_update_stats ?(cn_source_loc_opt = None) () =
   let cn_source_loc_arg =
     match cn_source_loc_opt with
@@ -120,7 +122,7 @@ let generate_error_msg_info_update_stats ?(cn_source_loc_opt = None) () =
               (None, [ (Cerb_location.unknown, [ loc_str_2_escaped ^ loc_str_escaped ]) ]))
       in
       cn_source_loc_str
-    | None -> mk_expr A.(AilEconst ConstantNull)
+    | None -> mk_expr ail_null
   in
   let update_fn_sym = Sym.fresh "update_cn_error_message_info" in
   [ A.(
@@ -542,11 +544,7 @@ let cn_to_ail_const const basetype =
     | MemByte { alloc_id = _; value = i } ->
       wrap (A.AilEconst (ConstantInteger (IConstant (i, Decimal, None))))
     | Bits ((sgn, sz), i) ->
-      let z_min, z_max = BT.bits_range (sgn, sz) in
-      let ity =
-        let ibt = CF.IntegerType.IntN_t sz in
-        match sgn with Signed -> C.Signed ibt | Unsigned -> C.Unsigned ibt
-      in
+      let z_min, _ = BT.bits_range (sgn, sz) in
       let suffix =
         let size_of = Memory.size_of_integer_type in
         match sgn with
@@ -566,14 +564,17 @@ let cn_to_ail_const const basetype =
             Some A.LL
       in
       let ail_const =
-        if Z.equal i z_max then
-          A.ConstantInteger (IConstantMax ity)
-        else if Z.equal i z_min && BT.equal_sign sgn BT.Signed then
-          A.ConstantInteger (IConstantMin ity)
+        let k a = A.(AilEconst (ConstantInteger (IConstant (a, Decimal, suffix)))) in
+        if Z.equal i z_min && BT.equal_sign sgn BT.Signed then
+          A.(
+            AilEbinary
+              ( mk_expr (k (Z.neg (Z.sub (Z.neg i) Z.one))),
+                Arithmetic Sub,
+                mk_expr (k Z.one) ))
         else
-          ConstantInteger (IConstant (i, Decimal, suffix))
+          k i
       in
-      wrap (A.AilEconst ail_const)
+      wrap ail_const
     | Q q -> wrap (A.AilEconst (ConstantFloating (Q.to_string q, None)))
     | Pointer z ->
       let ail_const' =
@@ -584,9 +585,8 @@ let cn_to_ail_const const basetype =
     | Bool b ->
       wrap
         (A.AilEconst (ConstantPredefined (if b then PConstantTrue else PConstantFalse)))
-    | Unit ->
-      wrap (A.AilEconst ConstantNull) (* Gets overridden by dest_with_unit_check *)
-    | Null -> wrap (A.AilEconst ConstantNull)
+    | Unit -> wrap ail_null (* Gets overridden by dest_with_unit_check *)
+    | Null -> wrap ail_null
     | CType_const _ -> failwith (__LOC__ ^ ": TODO CType_const")
     | Default bt -> cn_to_ail_default bt
   in
@@ -705,10 +705,10 @@ let generate_get_or_put_ownership_function ~without_ownership_checking ctype
     if without_ownership_checking then
       ([], [])
     else (
-      let uintptr_t_type = C.uintptr_t in
-      let generic_c_ptr_binding = create_binding generic_c_ptr_sym uintptr_t_type in
+      let void_ptr = C.mk_ctype_pointer C.no_qualifiers C.void in
+      let generic_c_ptr_binding = create_binding generic_c_ptr_sym void_ptr in
       let uintptr_t_cast_expr =
-        mk_expr A.(AilEcast (C.no_qualifiers, uintptr_t_type, cast_expr))
+        mk_expr A.(AilEcast (C.no_qualifiers, void_ptr, cast_expr))
       in
       let generic_c_ptr_assign_stat_ =
         A.(AilSdeclaration [ (generic_c_ptr_sym, Some uintptr_t_cast_expr) ])
@@ -2634,7 +2634,6 @@ let cn_to_ail_resource
       let matching_preds =
         List.filter (fun (pred_sym', _def) -> Sym.equal pname pred_sym') preds
       in
-      Printf.printf "Pred sym: %s\n" (Sym.pp_string pname);
       let pred_sym', pred_def' =
         match matching_preds with
         | [] ->