model with entry point: replay

Author: S41d

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/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/symbolic/symbol_scope.ml

@@ -204,7 +204,10 @@ let model_of_json json_str =
     match List.assoc_opt "model" root with
     | Some items ->
       let+ () = process_json (Util.to_list items) in
-      tbl
+      let entry_point =
+        Option.map Util.to_string (List.assoc_opt "entry_point" root)
+      in
+      (entry_point, tbl)
     | None -> Fmt.error_msg "JSON does not contain model field" )
   | _ ->
     Fmt.error_msg "Invalid JSON format for symbol scope:@. %a"
@@ -238,6 +241,10 @@ let model_of_scfg scfg =
   match Query.get_dir "model" scfg with
   | Some model ->
     let+ () = process_dirs model.children in
-    tbl
+    let entry_point =
+      let dir = Query.get_dir "entry_point" model.children in
+      Option.bind dir (fun dir -> Result.to_option @@ Query.get_param 0 dir)
+    in
+    (entry_point, tbl)
   | None ->
     Fmt.error_msg "Could not find the directive `model` in the scfg config"

src/symbolic/symbol_scope.mli

@@ -24,6 +24,6 @@ val to_json :
   -> t
   -> [> `Assoc of (string * Yojson.Basic.t) list ]
 
-val model_of_json : string -> Smtml.Model.t Result.t
+val model_of_json : string -> (string option * Smtml.Model.t) Result.t
 
-val model_of_scfg : string -> Smtml.Model.t Result.t
+val model_of_scfg : string -> (string option * Smtml.Model.t) Result.t

test/c/dune

@@ -15,6 +15,7 @@
   main.c
   malloc_aligned.c
   malloc_zero.c
+  model_with_entry_point.c
   multi_model.c
   range.c
   scopes.c))