fixed ite type-checking bug w/ bool & perm

nyu-acsys · Nov 8, 2024 · a9a1525 · a9a1525
1 parent 91bb68f
commit a9a1525
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 2 deletions.
diff --git a/lib/frontend/typing.ml b/lib/frontend/typing.ml
@@ -335,7 +335,7 @@ let rec process_expr (expr : expr) (expected_typ : type_expr) : expr Rewriter.t
           (* infer and propagate expected type of expr3 *)
           let expected_typ3 =
             match constr with
-            | Ite -> expected_typ2
+            | Ite -> expected_typ
             | MapUpdate -> Type.map_codom typ1
             | _ -> assert false
           in
@@ -344,7 +344,7 @@ let rec process_expr (expr : expr) (expected_typ : type_expr) : expr Rewriter.t
           (* backpropagate typ3 to expr2 if needed *)
           let expected_typ2 =
             match constr with
-            | Ite -> typ3
+            | Ite -> Type.join typ2 typ3
             | MapUpdate -> typ2
             | _ -> assert false
           in

diff --git a/test/ci/front-end/bool_perm_ite.rav b/test/ci/front-end/bool_perm_ite.rav
@@ -0,0 +1,6 @@
+field f: Int
+
+proc p(x: Ref) {
+    inhale !true ? true : own(x, f, 1, 1.0);
+    exhale true ?  own(x, f, 1, 1.0) : true;
+}
diff --git a/test/ci/front-end/bool_perm_ite.t b/test/ci/front-end/bool_perm_ite.t
@@ -0,0 +1,2 @@
+  $ dune exec -- raven --shh ./bool_perm_ite.rav
+  Verification successful.