Model with entry point

CHANGES.md

@@ -41,6 +41,7 @@
 - add `owi_label_is_covered` primitive
 - add scopes with `owi_open_scope` and `owi_close_scope` primitives
 - start support for simd instructions
+- add `--model-with-entry-point` option
 
 ## 0.2 - 2024-04-24
 

doc/src/manpages/owi-c.md

@@ -56,6 +56,9 @@ OPTIONS
            given this is used as a prefix and the ouputed files would have
            PREFIX_%d.
 
+       --model-with-entry-point
+           Add the entry point in the generated model for easier replay.
+
        --no-assert-failure-expression-printing
            do not display the expression in the assert failure
 

doc/src/manpages/owi-conc.md

@@ -41,6 +41,9 @@ OPTIONS
            given this is used as a prefix and the ouputed files would have
            PREFIX_%d.
 
+       --model-with-entry-point
+           Add the entry point in the generated model for easier replay.
+
        --no-assert-failure-expression-printing
            do not display the expression in the assert failure
 

doc/src/manpages/owi-cpp.md

@@ -51,6 +51,9 @@ OPTIONS
            given this is used as a prefix and the ouputed files would have
            PREFIX_%d.
 
+       --model-with-entry-point
+           Add the entry point in the generated model for easier replay.
+
        --no-assert-failure-expression-printing
            do not display the expression in the assert failure
 

doc/src/manpages/owi-rust.md

@@ -51,6 +51,9 @@ OPTIONS
            given this is used as a prefix and the ouputed files would have
            PREFIX_%d.
 
+       --model-with-entry-point
+           Add the entry point in the generated model for easier replay.
+
        --no-assert-failure-expression-printing
            do not display the expression in the assert failure
 

doc/src/manpages/owi-sym.md

@@ -41,6 +41,9 @@ OPTIONS
            given this is used as a prefix and the ouputed files would have
            PREFIX_%d.
 
+       --model-with-entry-point
+           Add the entry point in the generated model for easier replay.
+
        --no-assert-failure-expression-printing
            do not display the expression in the assert failure
 

doc/src/manpages/owi-zig.md

@@ -48,6 +48,9 @@ OPTIONS
            given this is used as a prefix and the ouputed files would have
            PREFIX_%d.
 
+       --model-with-entry-point
+           Add the entry point in the generated model for easier replay.
+
        --no-assert-failure-expression-printing
            do not display the expression in the assert failure
 

src/bin/owi.ml

@@ -150,6 +150,10 @@ let model_out_file =
     & opt (some path_conv) None
     & info [ "model-out-file" ] ~docv:"FILE" ~doc )
 
+let model_with_entry_point =
+  let doc = "Add the entry point in the generated model for easier replay." in
+  Arg.(value & flag & info [ "model-with-entry-point" ] ~doc)
+
 let rac =
   let doc = "runtime assertion checking mode" in
   Arg.(value & flag & info [ "rac" ] ~doc)
@@ -247,12 +251,14 @@ let c_cmd =
   and+ out_file
   and+ model_out_file
   and+ with_breadcrumbs
+  and+ model_with_entry_point
   and+ entry_point in
   Cmd_c.cmd ~arch ~property ~testcomp ~workspace ~workers ~opt_lvl ~includes
     ~files ~unsafe ~optimize ~no_stop_at_failure ~no_value
     ~no_assert_failure_expression_printing ~deterministic_result_order
     ~fail_mode ~concolic ~eacsl ~solver ~model_format ~entry_point
     ~invoke_with_symbols ~out_file ~model_out_file ~with_breadcrumbs
+    ~model_with_entry_point
 (* owi cpp *)
 
 let cpp_info =
@@ -284,12 +290,13 @@ let cpp_cmd =
   and+ workspace
   and+ model_out_file
   and+ with_breadcrumbs
+  and+ model_with_entry_point
   and+ entry_point in
   Cmd_cpp.cmd ~arch ~workers ~opt_lvl ~includes ~files ~unsafe ~optimize
     ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing
     ~deterministic_result_order ~fail_mode ~concolic ~solver ~model_format
     ~entry_point ~invoke_with_symbols ~out_file ~workspace ~model_out_file
-    ~with_breadcrumbs
+    ~with_breadcrumbs ~model_with_entry_point
 
 (* owi conc *)
 
@@ -317,11 +324,13 @@ let conc_cmd =
   and+ model_out_file
   and+ invoke_with_symbols
   and+ with_breadcrumbs
+  and+ model_with_entry_point
   and+ entry_point in
   Cmd_conc.cmd ~unsafe ~rac ~srac ~optimize ~workers ~no_stop_at_failure
     ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order
     ~fail_mode ~workspace ~solver ~files ~model_format ~entry_point
     ~invoke_with_symbols ~model_out_file ~with_breadcrumbs
+    ~model_with_entry_point
 
 (* owi fmt *)
 
@@ -475,12 +484,13 @@ let rust_cmd =
   and+ workspace
   and+ model_out_file
   and+ with_breadcrumbs
+  and+ model_with_entry_point
   and+ entry_point in
   Cmd_rust.cmd ~arch ~workers ~opt_lvl ~includes ~files ~unsafe ~optimize
     ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing
     ~deterministic_result_order ~fail_mode ~concolic ~solver ~model_format
     ~entry_point ~invoke_with_symbols ~out_file ~workspace ~model_out_file
-    ~with_breadcrumbs
+    ~with_breadcrumbs ~model_with_entry_point
 
 (* owi script *)
 
@@ -525,11 +535,13 @@ let sym_cmd =
   and+ entry_point
   and+ model_out_file
   and+ with_breadcrumbs
+  and+ model_with_entry_point
   and+ invoke_with_symbols in
   Cmd_sym.cmd ~unsafe ~rac ~srac ~optimize ~workers ~no_stop_at_failure
     ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order
     ~fail_mode ~workspace ~solver ~files ~model_format ~entry_point
     ~invoke_with_symbols ~model_out_file ~with_breadcrumbs
+    ~model_with_entry_point
 
 (* owi validate *)
 
@@ -619,11 +631,13 @@ let zig_cmd =
   and+ model_out_file
   and+ () = setup_log
   and+ with_breadcrumbs
+  and+ model_with_entry_point
   and+ entry_point in
   Cmd_zig.cmd ~includes ~workers ~files ~unsafe ~optimize ~no_stop_at_failure
     ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order
     ~fail_mode ~concolic ~solver ~model_format ~entry_point ~invoke_with_symbols
     ~out_file ~workspace ~model_out_file ~with_breadcrumbs
+    ~model_with_entry_point
 
 (* owi *)
 

src/cmd/cmd_c.ml

@@ -177,8 +177,8 @@ let cmd ~arch ~property ~testcomp:_ ~workspace ~workers ~opt_lvl ~includes
   ~files ~unsafe ~optimize ~no_stop_at_failure ~no_value
   ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode
   ~concolic ~eacsl ~solver ~model_format ~(entry_point : string option)
-  ~invoke_with_symbols ~out_file ~model_out_file ~with_breadcrumbs :
-  unit Result.t =
+  ~invoke_with_symbols ~out_file ~model_out_file ~with_breadcrumbs
+  ~model_with_entry_point : unit Result.t =
   let* workspace =
     match workspace with
     | Some path -> Ok path
@@ -201,3 +201,4 @@ let cmd ~arch ~property ~testcomp:_ ~workspace ~workers ~opt_lvl ~includes
     ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order
     ~fail_mode ~workspace ~solver ~files ~model_format ~entry_point
     ~invoke_with_symbols ~model_out_file ~with_breadcrumbs
+    ~model_with_entry_point

src/cmd/cmd_c.mli

@@ -27,4 +27,5 @@ val cmd :
   -> out_file:Fpath.t option
   -> model_out_file:Fpath.t option
   -> with_breadcrumbs:bool
+  -> model_with_entry_point:bool
   -> unit Result.t

src/cmd/cmd_conc.ml

@@ -433,7 +433,8 @@ let assignments_to_model (assignments : (Smtml.Symbol.t * V.t) list) :
 let cmd ~unsafe ~rac ~srac ~optimize ~workers:_ ~no_stop_at_failure:_ ~no_value
   ~no_assert_failure_expression_printing ~deterministic_result_order:_
   ~fail_mode:_ ~workspace ~solver ~files ~model_format ~entry_point
-  ~invoke_with_symbols ~model_out_file ~with_breadcrumbs:_ =
+  ~invoke_with_symbols ~model_out_file ~with_breadcrumbs:_
+  ~model_with_entry_point:_ =
   let* workspace =
     match workspace with
     | Some path -> Ok path

src/cmd/cmd_conc.mli

@@ -21,4 +21,5 @@ val cmd :
   -> invoke_with_symbols:bool
   -> model_out_file:Fpath.t option
   -> with_breadcrumbs:bool
+  -> model_with_entry_point:bool
   -> unit Result.t

src/cmd/cmd_cpp.ml

@@ -103,7 +103,7 @@ let cmd ~arch:_ ~workers ~opt_lvl ~includes ~files ~unsafe ~optimize
   ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing
   ~deterministic_result_order ~fail_mode ~concolic ~solver ~model_format
   ~entry_point ~invoke_with_symbols ~out_file ~workspace ~model_out_file
-  ~with_breadcrumbs : unit Result.t =
+  ~with_breadcrumbs ~model_with_entry_point : unit Result.t =
   let* workspace =
     match workspace with
     | Some path -> Ok path
@@ -124,3 +124,4 @@ let cmd ~arch:_ ~workers ~opt_lvl ~includes ~files ~unsafe ~optimize
     ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order
     ~fail_mode ~workspace ~solver ~files ~model_format ~entry_point
     ~invoke_with_symbols ~model_out_file ~with_breadcrumbs
+    ~model_with_entry_point

src/cmd/cmd_cpp.mli

@@ -24,4 +24,5 @@ val cmd :
   -> workspace:Fpath.t option
   -> model_out_file:Fpath.t option
   -> with_breadcrumbs:bool
+  -> model_with_entry_point:bool
   -> unit Result.t

src/cmd/cmd_iso.ml

@@ -443,5 +443,6 @@ let cmd ~deterministic_result_order ~fail_mode ~files ~model_format
       Cmd_sym.handle_result ~fail_mode ~workers ~solver
         ~deterministic_result_order ~model_format ~no_value
         ~no_assert_failure_expression_printing ~workspace ~no_stop_at_failure
-        ~model_out_file ~with_breadcrumbs result )
+        ~model_out_file ~with_breadcrumbs ~model_with_entry_point:false
+        ~entry_point:None result )
     () common_exports

src/cmd/cmd_replay.ml

@@ -261,19 +261,19 @@ let run_file ~unsafe ~optimize ~entry_point ~invoke_with_symbols filename model
 
 let cmd ~unsafe ~optimize ~replay_file ~source_file ~entry_point
   ~invoke_with_symbols =
+  let file_ext = Fpath.get_ext replay_file in
   let* parse_fn =
-    let ext = Fpath.get_ext replay_file in
-    match String.lowercase_ascii ext with
+    match String.lowercase_ascii file_ext with
     | ".json" -> Ok Symbol_scope.model_of_json
     | ".scfg" -> Ok Symbol_scope.model_of_scfg
-    | _ -> Error (`Unsupported_file_extension ext)
+    | _ -> Error (`Unsupported_file_extension file_ext)
   in
   let* file_content = Bos.OS.File.read replay_file in
-  let* model =
+  let* model_entry_point, model =
     match parse_fn file_content with
     | Error (`Msg msg) -> Error (`Invalid_model msg)
     | Error err -> Error err
-    | Ok model ->
+    | Ok (entry_point, model) ->
       let bindings = Smtml.Model.get_bindings model in
       let+ model =
         list_map
@@ -298,8 +298,13 @@ let cmd ~unsafe ~optimize ~replay_file ~source_file ~entry_point
                    (Fmt.str "unexpected value type: %a" Smtml.Value.pp v) ) )
           bindings
       in
-      Array.of_list model
+      (entry_point, Array.of_list model)
   in
+  let entry_point =
+    if Option.is_none entry_point then model_entry_point else entry_point
+  in
+  Logs.debug (fun m -> m "%s" (Option.value ~default:"na" entry_point));
+  Logs.debug (fun m -> m "%s" (Option.value ~default:"na" model_entry_point));
   let+ () =
     run_file ~unsafe ~optimize ~entry_point ~invoke_with_symbols source_file
       model

src/cmd/cmd_rust.ml

@@ -50,7 +50,7 @@ let cmd ~arch:_ ~workers ~opt_lvl ~includes ~files ~unsafe ~optimize
   ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing
   ~deterministic_result_order ~fail_mode ~concolic ~solver ~model_format
   ~entry_point ~invoke_with_symbols ~out_file ~(workspace : Fpath.t option)
-  ~model_out_file ~with_breadcrumbs : unit Result.t =
+  ~model_out_file ~with_breadcrumbs ~model_with_entry_point : unit Result.t =
   let* workspace =
     match workspace with
     | Some path -> Ok path
@@ -68,3 +68,4 @@ let cmd ~arch:_ ~workers ~opt_lvl ~includes ~files ~unsafe ~optimize
     ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order
     ~fail_mode ~workspace ~solver ~files ~model_format ~entry_point
     ~invoke_with_symbols ~model_out_file ~with_breadcrumbs
+    ~model_with_entry_point

src/cmd/cmd_rust.mli

@@ -24,4 +24,5 @@ val cmd :
   -> workspace:Fpath.t option
   -> model_out_file:Fpath.t option
   -> with_breadcrumbs:bool
+  -> model_with_entry_point:bool
   -> unit Result.t

src/cmd/cmd_sym.ml

@@ -34,7 +34,8 @@ let run_file ~entry_point ~unsafe ~rac ~srac ~optimize ~invoke_with_symbols _pc
   Interpret.Symbolic.modul link_state.envs m
 
 let print_bug ~model_format ~model_out_file ~id ~no_value ~no_stop_at_failure
-  ~no_assert_failure_expression_printing ~with_breadcrumbs bug =
+  ~no_assert_failure_expression_printing ~with_breadcrumbs
+  ~model_with_entry_point ~entry_point bug =
   let pp fmt (model, labels, breadcrumbs, scoped_values) =
     match model_format with
     | Cmd_utils.Json ->
@@ -62,7 +63,8 @@ let print_bug ~model_format ~model_out_file ~id ~no_value ~no_stop_at_failure
             } )
           labels
       in
-      let children =
+      let model = { model with children = model.children @ lbls } in
+      let model =
         if with_breadcrumbs then
           let bcrumbs =
             [ { Scfg.Types.name = "breadcrumbs"
@@ -71,10 +73,22 @@ let print_bug ~model_format ~model_out_file ~id ~no_value ~no_stop_at_failure
               }
             ]
           in
-          model.children @ lbls @ bcrumbs
-        else model.children @ lbls
+          { model with children = model.children @ bcrumbs }
+        else model
       in
-      Scfg.Pp.directive fmt { model with children }
+      let model =
+        if model_with_entry_point then
+          let ep =
+            [ { Scfg.Types.name = "entry_point"
+              ; params = [ entry_point ]
+              ; children = []
+              }
+            ]
+          in
+          { model with children = model.children @ ep }
+        else model
+      in
+      Scfg.Pp.directive fmt model
   in
   let to_file path model labels breadcrumbs symbol_scopes =
     let model_ext = match model_format with Json -> "json" | Scfg -> "scfg" in
@@ -117,7 +131,7 @@ let print_bug ~model_format ~model_out_file ~id ~no_value ~no_stop_at_failure
 
 let print_and_count_failures ~model_format ~model_out_file ~no_value
   ~no_assert_failure_expression_printing ~workspace ~no_stop_at_failure
-  ~count_acc ~results ~with_breadcrumbs =
+  ~count_acc ~results ~with_breadcrumbs ~model_with_entry_point ~entry_point =
   let test_suite_dir = Fpath.(workspace / "test-suite") in
   let* (_created : bool) =
     if not no_value then OS.Dir.create test_suite_dir else Ok false
@@ -133,7 +147,7 @@ let print_and_count_failures ~model_format ~model_out_file ~no_value
           let* () =
             print_bug ~model_format ~model_out_file ~id:count_acc ~no_value
               ~no_stop_at_failure ~no_assert_failure_expression_printing
-              ~with_breadcrumbs bug
+              ~with_breadcrumbs ~model_with_entry_point ~entry_point bug
           in
           Ok model
         | `Error e -> Error e
@@ -162,7 +176,7 @@ let sort_results deterministic_result_order results =
 let handle_result ~workers ~no_stop_at_failure ~no_value
   ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode
   ~workspace ~solver ~model_format ~model_out_file ~with_breadcrumbs
-  (result : unit Symbolic.Choice.t) =
+  ~model_with_entry_point ~entry_point (result : unit Symbolic.Choice.t) =
   let thread = Thread_with_memory.init () in
   let res_queue = Wq.make () in
   let path_count = Atomic.make 0 in
@@ -193,10 +207,16 @@ let handle_result ~workers ~no_stop_at_failure ~no_value
       Array.iter Domain.join join_handles )
   in
   let results = sort_results deterministic_result_order results in
+  let* entry_point =
+    if model_with_entry_point then
+      match entry_point with Some ep -> Ok ep | None -> Fmt.error_msg ""
+    else Ok ""
+  in
   let* count =
     print_and_count_failures ~model_format ~model_out_file ~no_value
       ~no_assert_failure_expression_printing ~workspace ~no_stop_at_failure
-      ~count_acc:0 ~results ~with_breadcrumbs
+      ~count_acc:0 ~results ~with_breadcrumbs ~model_with_entry_point
+      ~entry_point
   in
   Logs.info (fun m -> m "Completed paths: %d" (Atomic.get path_count));
   let+ () = if count > 0 then Error (`Found_bug count) else Ok () in
@@ -209,7 +229,7 @@ let handle_result ~workers ~no_stop_at_failure ~no_value
 let cmd ~unsafe ~rac ~srac ~optimize ~workers ~no_stop_at_failure ~no_value
   ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode
   ~workspace ~solver ~files ~model_format ~entry_point ~invoke_with_symbols
-  ~model_out_file ~with_breadcrumbs =
+  ~model_out_file ~with_breadcrumbs ~model_with_entry_point =
   let* workspace =
     match workspace with
     | Some path -> Ok path
@@ -226,4 +246,5 @@ let cmd ~unsafe ~rac ~srac ~optimize ~workers ~no_stop_at_failure ~no_value
   in
   handle_result ~fail_mode ~workers ~solver ~deterministic_result_order
     ~model_format ~no_value ~no_assert_failure_expression_printing ~workspace
-    ~no_stop_at_failure ~model_out_file ~with_breadcrumbs result
+    ~no_stop_at_failure ~model_out_file ~with_breadcrumbs
+    ~model_with_entry_point ~entry_point result