Fixes for fulminate

.github/workflows/ci.yml

@@ -70,6 +70,6 @@ jobs:
       run: |
         opam switch ${{ matrix.version }}
         eval $(opam env --switch=${{ matrix.version }})
-        cd tests; USE_OPAM='' ./run-ci.sh
+        cd tests; USE_OPAM='' ./run-ci.sh --both-callconvs
         ./diff-prog.py cerberus bytes/elab.json
         ./diff-prog.py cerberus bytes/exec.json

.gitignore

@@ -23,7 +23,6 @@ generated_tex/
 /public/node_modules/
 /cerberus-webserver
 /webcerb.concrete
-/webcerb.symbolic
 /webcerb.vip
 /public/dist/main.bundle.js
 /public/dist/main.bundle.js.map

Makefile

@@ -115,9 +115,8 @@ web: cerberus-web
 cerberus-web: prelude-src web-deployment
 	@echo "[DUNE] web"
 	$(Q)dune build $(DUNEFLAGS) cerberus-lib.install cerberus-web.install
-	$(Q) rm -f webcerb.concrete webcerb.symbolic webcerb.vip cerberus-webserver
+	$(Q) rm -f webcerb.concrete webcerb.vip cerberus-webserver
 	$(Q)cp -L _build/default/backend/web/instance.exe webcerb.concrete
-	$(Q)cp -L _build/default/backend/web/instance_symbolic.exe webcerb.symbolic
 	$(Q)cp -L _build/default/backend/web/instance_vip.exe webcerb.vip
 	$(Q)cp -L _build/default/backend/web/web.exe cerberus-webserver
 
@@ -149,8 +148,7 @@ LEM_CORE_TO_CORE  = core_sequentialise.lem core_indet.lem core_rewrite.lem \
                     core_unstruct.lem
 LEM_CORE_DYNAMICS = core_run_aux.lem core_eval.lem core_run.lem core_reduction.lem core_reduction_aux.lem driver.lem
 LEM_ELABORATION   = translation_effect.lem translation_aux.lem translation.lem 
-LEM_DEFACTO       = mem_common.lem defacto_memory_types.lem \
-                    defacto_memory_aux.lem defacto_memory.lem mem.lem \
+LEM_DEFACTO       = mem_common.lem mem.lem \
                     mem_aux.lem
 LEM_CONC_INTERF   = cmm_aux.lem
 LEM_CONC          = cmm_csem.lem cmm_op.lem linux.lem
@@ -276,7 +274,7 @@ clean-sibylfs-src:
 
 .PHONY: clean-web distclean-web
 clean-web:
-	$(Q)rm -f webcerb.concrete webcerb.symbolic webcerb.vip cerberus-webserver
+	$(Q)rm -f webcerb.concrete webcerb.vip cerberus-webserver
 distclean-web:
 	$(Q)rm -f public/dist/main.bundle.js public/dist/main.bundle.js.map
 	$(Q)rm -f public/dist/style.bundle.css public/dist/style.bundle.css.map

backend/bmc/bmc_common.ml

@@ -135,13 +135,13 @@ let integer_value_to_z3 (ival: Impl_mem.integer_value) : Expr.expr =
   | None -> assert false
   | Some i -> big_num_to_z3 i
 
-let object_value_to_z3 (oval: object_value) : Expr.expr =
+let object_value_to_z3 ~tagDefs (oval: object_value) : Expr.expr =
   match oval with
   | OVinteger ival -> integer_value_to_z3 ival
   | OVfloating _ ->
         failwith "Floats are not supported."
   | OVpointer pv ->
-      assert (is_null pv);
+      assert (is_null ~tagDefs pv);
       PointerSort.mk_null
   | OVarray _
   | OVstruct _
@@ -163,7 +163,7 @@ let value_to_z3 (value: value) (file: unit typed_file) : Expr.expr =
   | Vlist _      -> assert false
   | Vtuple _     -> assert false
   | Vctype cty   -> CtypeSort.mk_expr cty
-  | Vobject oval -> object_value_to_z3 oval
+  | Vobject oval -> object_value_to_z3 ~tagDefs:file.tagDefs oval
   | Vloaded (LVspecified oval) ->
       begin match oval with
        | OVinteger ival ->

backend/bmc/bmc_utils.ml

@@ -191,10 +191,10 @@ let ident_cmp = fun ident1 ident2 ->
 
 
 (* ========== Core memory functions ============= *)
-let is_null (ptr: Impl_mem.pointer_value) : bool =
+let is_null ~tagDefs (ptr: Impl_mem.pointer_value) : bool =
   let (Nondeterminism.ND f) =
     Impl_mem.eq_ptrval Cerb_location.unknown ptr (Impl_mem.null_ptrval Ctype.void) in
-  match f (Impl_mem.initial_mem_state) with
+  match f (Impl_mem.initial_mem_state tagDefs) with
   | (Nondeterminism.NDactive b,_) -> b
   | _ -> assert false
 

backend/bmc/main.ml

@@ -11,13 +11,13 @@ let io, get_progress =
   let open Pipeline in
   default_io_helpers, get_progress
 
-let frontend (conf, io) ~is_lib filename core_std =
+let frontend elab_conf (conf, io) ~is_lib filename core_std =
   if not (Sys.file_exists filename) then
     error ("The file `" ^ filename ^ "' doesn't exist.");
   if Filename.check_suffix filename ".co" || Filename.check_suffix filename ".o" then
     read_core_object (conf, io) ~is_lib core_std filename
   else if Filename.check_suffix filename ".c" then
-    c_frontend_and_elaboration (conf, io) core_std ~filename >>= fun (_, _, core_file) ->
+    c_frontend_and_elaboration elab_conf (conf, io) core_std ~filename >>= fun (_, _, core_file) ->
     core_passes (conf, io) ~filename core_file
   else if Filename.check_suffix filename ".core" then
     core_frontend (conf, io) core_std ~filename
@@ -106,16 +106,18 @@ let cerberus debug_level progress core_obj
   let prelude =
     (* Looking for and parsing the core standard library *)
     Switches.set switches;
+    (* TODO: merge this with conf *)
+    let elab_conf = mk_elab_config () in
     load_core_stdlib () >>= fun core_stdlib ->
     io.pass_message "Core standard library loaded." >>
     (* Looking for and parsing the implementation file *)
     load_core_impl core_stdlib impl_name >>= fun core_impl ->
     io.pass_message "Implementation file loaded." >>
-    return (core_stdlib, core_impl)
+    return ((core_stdlib, core_impl), elab_conf)
   in
-  let main core_std =
+  let main core_std elab_conf =
     Exception.except_foldlM (fun core_files (is_lib, file) ->
-      frontend (conf, io) ~is_lib file core_std >>= fun core_file ->
+      frontend elab_conf (conf, io) ~is_lib file core_std >>= fun core_file ->
       return (core_file::core_files)
     ) [] (core_libraries (not nolibc && not core_obj) link_lib_path link_core_obj @ (List.map (fun z -> (false, z)) files))
   in
@@ -187,7 +189,8 @@ let cerberus debug_level progress core_obj
       else
         Pp_errors.fatal "no input file"
     | [file] when core_obj ->
-      prelude >>= frontend (conf, io) ~is_lib:false file >>= fun core_file ->
+      prelude >>= fun (core_std, elab_conf) ->
+      frontend elab_conf (conf, io) ~is_lib:false file core_std >>= fun core_file ->
       begin match output_name with
         | Some output_file ->
           write_core_object core_file output_file
@@ -204,8 +207,8 @@ let cerberus debug_level progress core_obj
       else if bmc then
         begin match files with
           | [filename] ->
-            prelude >>= fun core_std ->
-            c_frontend_and_elaboration (conf, io) core_std ~filename >>= fun (_, ail_opt, core) ->
+            prelude >>= fun (core_std, elab_conf) ->
+            c_frontend_and_elaboration elab_conf (conf, io) core_std ~filename >>= fun (_, ail_opt, core) ->
             core_passes (conf, io) ~filename core >>= fun core ->
             ignore @@ Bmc.bmc core (Option.map snd ail_opt);
             return success
@@ -236,26 +239,26 @@ let cerberus debug_level progress core_obj
         return success
       (* Dump a core object (-c) *)
       else if core_obj then
-        prelude >>= fun core_std ->
+        prelude >>= fun (core_std, elab_conf) ->
         Exception.except_foldlM (fun () file ->
-          frontend (conf, io) ~is_lib:false file core_std >>= fun core_file ->
+          frontend elab_conf (conf, io) ~is_lib:false file core_std >>= fun core_file ->
           let output_file = Filename.remove_extension file ^ ".co" in
           write_core_object core_file output_file;
           return ()
           ) () files >>= fun () ->
         return success
       (* Link and execute *)
       else
-        prelude >>= main >>= begin function
+        prelude >>= fun (core_std, elab_conf) ->
+        main core_std elab_conf >>= begin function
           | [] -> assert false
           | f::fs ->
             (*if cfg then Cfg.mk_dot ~sequentialise:sequentialise_core f;*)
             Core_linking.link (f::fs)
         end >>= fun core_file ->
         if exec then
           let open Driver_ocaml in
-          let () = Tags.set_tagDefs core_file.tagDefs in
-          let driver_conf = {concurrency; exec_mode; fs_dump; trace} in
+          let driver_conf = {exec_mode; do_stepping= false; concurrency; fs_dump; trace} in
           interp_backend io core_file ~args ~batch ~fs ~driver_conf
         else
           match output_name with

backend/common/driver_ocaml.ml

@@ -11,6 +11,8 @@ let isActive = function
 type driver_conf = {
 (* TODO: bring back ==> [`Interactive | `Exhaustive | `Random] -> *)
   exec_mode: execution_mode;
+  do_stepping: bool; (* Stepping should only be enabled when really used (e.g. for Web instances)
+                      * because it impacts execution time *)
   concurrency: bool;
   fs_dump: bool;
   trace: bool;
@@ -66,95 +68,111 @@ let string_of_batch_output ?(json=false) ?(is_charon=false) i_opt (z3_strs, exec
       end
     else
       "" in
-  let has_multiple =
-    match i_opt with
-      | Some i ->
-          Printf.bprintf buf "EXECUTION %d" i;
-          true
-      | None ->
-          Buffer.add_string buf constrs_str;
-          false in
-  begin match exec with
-    | Defined { exit; stdout; stderr; blocked } ->
-        let exit_str = Cerb_colour.without_colour string_of_batch_exit exit in
-        if is_charon then begin
-          if has_multiple then begin
-            Printf.bprintf buf " (exit = %s):\n" exit_str;
-            Buffer.add_string buf constrs_str
-          end;
-          Buffer.add_string buf stdout;
-          prerr_string stderr
-        end else if json then begin
-          Yojson.to_buffer buf begin
-            `Assoc [ "status", `String "Defined"
-                   ; "details", `Assoc [ "value", `String exit_str
-                                       ; "stdout", `String (String.escaped stdout)
-                                       ; "stderr", `String (String.escaped stderr) ] ]
-          end
-        end else begin
-          begin if has_multiple then
-            Buffer.add_string buf  ":\n"
-          end;
-          Buffer.add_string buf constrs_str;
-          Printf.bprintf buf "Defined {value: \"%s\", stdout: \"%s\", stderr: \"%s\", blocked: \"%s\"}"
-            exit_str
-            (String.escaped stdout) (String.escaped stderr)
-            (if blocked then "true" else "false")
-        end
-    | Undefined { ub; stderr; loc } ->
-        begin if has_multiple then
-          Buffer.add_string buf  ":\n"
-        end;
-        Buffer.add_string buf constrs_str;
-        if is_charon then begin
-          prerr_string stderr;
-          Printf.bprintf buf "Undefined {ub: \"%s\", loc: \"%s\"}%s"
-          (Undefined.stringFromUndefined_behaviour ub)
-          (Cerb_location.simple_location loc)
-          (if is_charon then "\n" else "")
-        end else if json then begin
-          Yojson.to_buffer buf begin
-            `Assoc [ "status", `String "Undefined"
-                   ; "details", `Assoc [ "ub", `String (Undefined.stringFromUndefined_behaviour ub)
-                                       ; "stderr", `String (String.escaped stderr)
-                                       ; "loc", (Cerb_location.to_json loc :> Yojson.t) ] ]
-          end
-        end else
-          Printf.bprintf buf "Undefined {ub: \"%s\", stderr: \"%s\", loc: \"%s\"}%s"
-          (Undefined.stringFromUndefined_behaviour ub)
-          (String.escaped stderr)
-          (Cerb_location.simple_location loc)
-          (if is_charon then "\n" else "")
-    | Error { msg; stderr } ->
-        if is_charon then
-          prerr_string stderr
-        else if json then begin
-          Yojson.to_buffer buf begin
-            `Assoc [ "status", `String "Error"
-                   ; "details", `Assoc [ "msg", `String msg
-                                       ; "stderr", `String (String.escaped stderr) ] ]
+  if json then begin
+    let execution_fields =
+      match i_opt with
+        | Some i -> [ ("execution", `Int i) ]
+        | None -> [] in
+    let constraints_fields =
+      if !Cerb_debug.debug_level > 0 then
+        [ ("constraints", `List (List.map (fun z -> `String z) z3_strs)) ]
+      else
+        [] in
+    let (status, details) =
+      match exec with
+        | Defined { exit; stdout; stderr; blocked } ->
+            ( "Defined"
+            , [ ("value", `String (Cerb_colour.without_colour string_of_batch_exit exit))
+              ; ("stdout", `String stdout)
+              ; ("stderr", `String stderr)
+              ; ("blocked", `Bool blocked) ] )
+        | Undefined { ub; stderr; loc } ->
+            ( "Undefined"
+            , [ ("ub", `String (Undefined.stringFromUndefined_behaviour ub))
+              ; ("stderr", `String stderr)
+              ; ("loc", (Cerb_location.to_json loc :> Yojson.t)) ] )
+        | Error { msg; stderr } ->
+            ( "Error"
+            , [ ("msg", `String msg)
+              ; ("stderr", `String stderr) ] ) in
+    Yojson.to_buffer buf begin
+      `Assoc (execution_fields @ [ ("status", `String status); ("details", `Assoc details) ]
+        @ constraints_fields)
+    end;
+    Buffer.add_string buf "\n";
+    flush_all ();
+    Buffer.contents buf
+  end else begin
+    let has_multiple =
+      match i_opt with
+        | Some i ->
+            Printf.bprintf buf "EXECUTION %d" i;
+            true
+        | None ->
+            Buffer.add_string buf constrs_str;
+            false in
+    begin match exec with
+      | Defined { exit; stdout; stderr; blocked } ->
+          let exit_str = Cerb_colour.without_colour string_of_batch_exit exit in
+          if is_charon then begin
+            if has_multiple then begin
+              Printf.bprintf buf " (exit = %s):\n" exit_str;
+              Buffer.add_string buf constrs_str
+            end;
+            Buffer.add_string buf stdout;
+            prerr_string stderr
+          end else begin
+            begin if has_multiple then
+              Buffer.add_string buf  ":\n"
+            end;
+            Buffer.add_string buf constrs_str;
+            Printf.bprintf buf "Defined {value: \"%s\", stdout: \"%s\", stderr: \"%s\", blocked: \"%s\"}"
+              exit_str
+              (String.escaped stdout) (String.escaped stderr)
+              (if blocked then "true" else "false")
           end
-        end else begin
+      | Undefined { ub; stderr; loc } ->
           begin if has_multiple then
             Buffer.add_string buf  ":\n"
           end;
           Buffer.add_string buf constrs_str;
-          Printf.bprintf buf "Error {msg: \"%s\"}%s"
-            msg
+          if is_charon then begin
+            prerr_string stderr;
+            Printf.bprintf buf "Undefined {ub: \"%s\", loc: \"%s\"}%s"
+            (Undefined.stringFromUndefined_behaviour ub)
+            (Cerb_location.simple_location loc)
             (if is_charon then "\n" else "")
-        end
-  end;
-  (if not is_charon then Buffer.add_string buf "\n" else ());
-  flush_all ();
-  Buffer.contents buf
+          end else
+            Printf.bprintf buf "Undefined {ub: \"%s\", stderr: \"%s\", loc: \"%s\"}%s"
+            (Undefined.stringFromUndefined_behaviour ub)
+            (String.escaped stderr)
+            (Cerb_location.simple_location loc)
+            (if is_charon then "\n" else "")
+      | Error { msg; stderr } ->
+          if is_charon then
+            prerr_string stderr
+          else begin
+            begin if has_multiple then
+              Buffer.add_string buf  ":\n"
+            end;
+            Buffer.add_string buf constrs_str;
+            Printf.bprintf buf "Error {msg: \"%s\"}%s"
+              msg
+              (if is_charon then "\n" else "")
+          end
+    end;
+    (if not is_charon then Buffer.add_string buf "\n" else ());
+    flush_all ();
+    Buffer.contents buf
+  end
 
 (* TODO: make the output match the json format from charon2 (or at least add a option for that) *)
 let batch_drive (file: 'a Core.file) args fs_state conf =
   Random.self_init ();
   (* changing the annotations type from unit to core_run_annotation *)
   let file = Core_run_aux.convert_file file in
   (* computing the value (or values if exhaustive) *)
-  let initial_dr_st = Driver.initial_driver_state file fs_state in
+  let initial_dr_st = Driver.initial_driver_state file fs_state conf.do_stepping in
   let values = Smt2.runND conf.exec_mode Impl_mem.cs_module (Driver.drive conf.concurrency file args) initial_dr_st in
   List.mapi (fun i (res, z3_strs, nd_st) ->
     let result = begin match res with
@@ -191,7 +209,7 @@ let drive file args fs_state conf : execution_result =
   (* changing the annotations type from unit to core_run_annotation *)
   let file = Core_run_aux.convert_file file in
   (* computing the value (or values if exhaustive) *)
-  let initial_dr_st = Driver.initial_driver_state file fs_state in
+  let initial_dr_st = Driver.initial_driver_state file fs_state conf.do_stepping in
   let values = Smt2.runND conf.exec_mode Impl_mem.cs_module
       (Driver.drive conf.concurrency file args) initial_dr_st in
   let n_actives = List.length (List.filter isActive values) in

backend/common/driver_ocaml.mli

@@ -3,6 +3,8 @@ open Cerb_frontend
 type driver_conf = {
 (* TODO: bring back ==> [`Interactive | `Exhaustive | `Random] -> *)
   exec_mode: Cerb_global.execution_mode;
+  do_stepping: bool; (* Stepping should only be enabled when really used (e.g. for Web instances)
+                      * because it impacts execution time *)
   concurrency: bool;
   fs_dump: bool;
   trace: bool;