fixes from a while back that I forgot to commit

PLSysSec · Oct 18, 2018 · 4d58856 · 4d58856
1 parent 9e1880e
commit 4d58856
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 7 deletions.
diff --git a/src/sanitycheck.ml b/src/sanitycheck.ml
@@ -126,11 +126,17 @@ class sanitychecker post_transform m =
                 if not (is_bool cty) then
                   raise @@ err p;
                 let e2_ty = type_of e2 in
+                let new_ty = match (label_of cty).data with
+                  | Public -> e2_ty
+                  | Secret -> classify e2_ty in
                   begin
                     match e1_ty.data with
                       | Ref (subty,{data=W|RW}) ->
-                        if not (e2_ty =: subty) then
-                          raise @@ err p
+                        if not (new_ty =: subty) then
+                          raise @@ cerr p
+                                     "mismatch: %s vs %s"
+                                     (ps#bty new_ty)
+                                     (ps#bty subty)
                       | _ -> raise @@ err p
                   end
             | Assume e -> ()

diff --git a/src/tast_util.ml b/src/tast_util.ml
@@ -171,7 +171,7 @@ let meet_mut p m1 m2 =
 
 let rec ( =: ) b1 b2 =
   match b1.data,b2.data with
-    | Bool l1,Bool l2 -> true
+    | Bool l1,Bool l2 -> l1 =$ l2
     | UInt (n,l1),UInt (m,l2) -> n = m && l1 =$ l2
     | Int (n,l1),Int (m,l2) -> n = m && l1 =$ l2
     | Ref (rb1,m1),Ref (rb2,m2) -> rb1 =: rb2 && m1 =* m2

diff --git a/src/typecheck.ml b/src/typecheck.ml
@@ -1005,13 +1005,17 @@ class typechecker =
             in
             let e2' = visit#expr ~lookahead_bty:unref_ty e2 in
             let e2_ty = type_of e2' in
-              if e2_ty <: unref_ty then
+            let new_ty = match stmlbl.data with
+              | Public -> e2_ty
+              | Secret -> classify e2_ty in
+              if new_ty <: unref_ty then
                 Assign (e1',expr_fix p unref_ty e2')
               else
                 raise @@ cerr p
-                           "expected %s, got %s"
-                           (show_base_type unref_ty)
-                           (show_base_type e2_ty)
+                           "expected %s, got %s (in %s context)"
+                           (ps#bty unref_ty)
+                           (ps#bty e2_ty)
+                           (ps#lbl stmlbl)
           | Ast.If _ -> raise @@ err p
           | Ast.RangeFor _ -> raise @@ err p
           | Ast.ArrayFor _ -> raise @@ err p