Tweak goto branching and reduction error handling

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

Hide file tree

Showing 2 changed files with 13 additions and 9 deletions.
diff --git a/GillianCore/engine/general_semantics/general/g_interpreter.ml b/GillianCore/engine/general_semantics/general/g_interpreter.ml
@@ -1336,18 +1336,18 @@ struct
         in
         List.mapi
           (fun j ((state, next), case) ->
+            let new_branches =
+              if j <> 0 then []
+              else
+                sp |> List.tl
+                |> List.map (fun ((state, next), case) ->
+                       (state, next, GuardedGoto case))
+            in
             make_confcont ~state
               ~callstack:(if j = 0 then cs else Call_stack.copy cs)
               ~invariant_frames:iframes ~prev_idx:i ~loop_ids ~next_idx:next
               ~branch_count:b_counter ~branch_case:(GuardedGoto case)
-              ~new_branches:
-                (if j = 0 then
-                 List.map
-                   (fun ((state, next), case) ->
-                     (state, next, GuardedGoto case))
-                   (List.tl sp)
-                else [])
-              ())
+              ~new_branches ())
           sp
 
       let eval_phi_assignment lxarr eval_state =

diff --git a/GillianCore/engine/symbolic_semantics/SState.ml b/GillianCore/engine/symbolic_semantics/SState.ml
@@ -214,7 +214,11 @@ module Make (SMemory : SMemory.S) :
       in
       (* Perform reduction *)
       if no_reduce then result
-      else Reduction.reduce_lexpr ~gamma ~reduce_lvars:true ~pfs result
+      else
+        try Reduction.reduce_lexpr ~gamma ~reduce_lvars:true ~pfs result
+        with Reduction.ReductionException (expr, msg) ->
+          let msg = Fmt.str "Couldn't reduce %a - %s" Expr.pp expr msg in
+          raise (Internal_State_Error ([ StateErr.EOther msg ], state))
     in
     symb_evaluate_expr e