Add index to SpecExec branch case

GillianPlatform · Sep 29, 2023 · d27239e · d27239e
1 parent f0a2d8d
commit d27239e
Show file tree

Hide file tree

Showing 4 changed files with 26 additions and 9 deletions.
diff --git a/GillianCore/GIL_Syntax/BranchCase.ml b/GillianCore/GIL_Syntax/BranchCase.ml
@@ -1,7 +1,7 @@
 type t =
   | GuardedGoto of bool
   | LCmd of int
-  | SpecExec of Flag.t
+  | SpecExec of Flag.t * int
   | LAction of Yojson.Safe.t list
   | LActionFail of int
 [@@deriving show, yojson]

diff --git a/GillianCore/GIL_Syntax/Gil_syntax.mli b/GillianCore/GIL_Syntax/Gil_syntax.mli
@@ -999,7 +999,7 @@ module BranchCase : sig
   type t =
     | GuardedGoto of bool  (** Effectively if/else; either true or false case *)
     | LCmd of int  (** Logical command *)
-    | SpecExec of Flag.t  (** Spec execution *)
+    | SpecExec of Flag.t * int  (** Spec execution *)
     | LAction of Yojson.Safe.t list  (** Logical action *)
     | LActionFail of int  (** {i Failed} logical action*)
   [@@deriving yojson, show]

diff --git a/GillianCore/debugging/utils/exec_map.ml b/GillianCore/debugging/utils/exec_map.ml
@@ -171,7 +171,8 @@ module Packaged = struct
       match case with
       | GuardedGoto b -> ("GuardedGoto", ("If/Else", Fmt.str "%B" b))
       | LCmd x -> ("LCmd", ("Logical command", Fmt.str "%d" x))
-      | SpecExec fl -> ("SpecExec", ("Spec exec", Fmt.str "%a" Flag.pp fl))
+      | SpecExec (fl, ix) ->
+          ("SpecExec", ("Spec exec", Fmt.str "%a-%d" Flag.pp fl ix))
       | LAction json ->
           let s = Yojson.Safe.to_string (`List json) in
           ("LAction", ("Logical action", s))

diff --git a/GillianCore/engine/general_semantics/general/g_interpreter.ml b/GillianCore/engine/general_semantics/general/g_interpreter.ml
@@ -714,18 +714,31 @@ struct
             | false -> cs
           in
 
-          let branch_case = SpecExec fl in
+          let succ_count = ref 0 in
+          let err_count = ref 0 in
+          let get_count fl =
+            let count =
+              match fl with
+              | Flag.Normal -> succ_count
+              | _ -> err_count
+            in
+            let result = !count in
+            count := result + 1;
+            result
+          in
+          let branch_case = SpecExec (fl, get_count fl) in
           let branch_case, new_branches =
             match (is_first, others) with
             | _, Some (_ :: _ as others) ->
                 let new_branches =
                   Some
                     (List_utils.get_list_somes
                     @@ List.map
-                         (fun conf ->
+                         (fun (conf, fl) ->
                            match conf with
                            | CConf.ConfCont { state; next_idx; _ } ->
-                               Some (state, next_idx, branch_case)
+                               Some
+                                 (state, next_idx, SpecExec (fl, get_count fl))
                            | _ -> None)
                          others)
                 in
@@ -857,13 +870,16 @@ struct
                       let others =
                         List.map
                           (fun (ret_state, fl) ->
-                            process_ret false ret_state fl b_counter None
-                              spec_name)
+                            let conf =
+                              process_ret false ret_state fl b_counter None
+                                spec_name
+                            in
+                            (conf, fl))
                           rest_rets
                       in
                       process_ret true ret_state fl b_counter (Some others)
                         spec_name
-                      :: others
+                      :: List.map fst others
                   | [] -> []
                 in
                 let error_confs =