[ASL] Fix bug where environment updates from IF test expressions were reverted (herd#1800)

Author: solswords

asllib/Interpreter.ml

@@ -632,7 +632,7 @@ module Make (B : Backend.S) (C : Config) = struct
               (fun () -> eval_expr_sef env1 e1)
               (fun () -> eval_expr_sef env1 e2)
           in
-          return_normal (v, env) |: SemanticsRule.ECondSimple
+          return_normal (v, env1)
         else
           choice_with_branch_effect env1 m_cond e_cond e1 e2 (fun (env, v) ->
               eval_expr env v)

asllib/instrumentation.ml

@@ -36,7 +36,6 @@ module SemanticsRule = struct
     | BinopOr
     | BinopImpl
     | Unop
-    | ECondSimple
     | ECond
     | ESlice
     | ECall
@@ -138,7 +137,6 @@ module SemanticsRule = struct
     | ETuple -> "ETuple"
     | EArray -> "EArray"
     | EEnumArray -> "EEnumArray"
-    | ECondSimple -> "ECondSimple"
     | EGetArray -> "EGetArray"
     | EGetEnumArray -> "EGetEnumArray"
     | ESliceError -> "ESliceError"
@@ -221,7 +219,6 @@ module SemanticsRule = struct
       BinopOr;
       BinopImpl;
       Unop;
-      ECondSimple;
       ECond;
       ESlice;
       ECall;
@@ -353,7 +350,6 @@ module TypingRule = struct
     | EVar
     | Binop
     | Unop
-    | ECondSimple
     | ECond
     | ESlice
     | ECall
@@ -558,7 +554,6 @@ module TypingRule = struct
     | EGetFields -> "EGetFields"
     | EConcat -> "EConcat"
     | ETuple -> "ETuple"
-    | ECondSimple -> "ECondSimple"
     | EGetArray -> "EGetArray"
     | ESliceError -> "ESliceError"
     | EArbitrary -> "EArbitrary"
@@ -752,7 +747,6 @@ module TypingRule = struct
       EPattern;
       EGetArray;
       ESliceError;
-      ECondSimple;
       EConcat;
       ETuple;
       LEDiscard;

asllib/tests/regressions.t/if-test-env-updated.asl

@@ -0,0 +1,12 @@
+var myglob : integer = 0;
+func mytest () => boolean
+begin
+  myglob = 1;
+  return TRUE;
+end;
+func main () => integer
+begin
+  var test = if mytest() then 0 else 1;
+  assert myglob == 1;
+  return 0;
+end;

asllib/tests/regressions.t/run.t

@@ -722,3 +722,7 @@ Bounds checks
   ASL Dynamic error: Mismatch type:
     value 100 does not belong to type integer {0..3}.
   [1]
+
+If test environment reversion bug
+  $ aslref if-test-env-updated.asl
+