Safety checker: fix lattice operations of the Init domain

CHANGELOG.md

@@ -61,7 +61,8 @@
 
 - Fixes to the safety checker
   ([PR #315](https://github.com/jasmin-lang/jasmin/pull/315),
-  ([PR #343](https://github.com/jasmin-lang/jasmin/pull/343);
+  ([PR #343](https://github.com/jasmin-lang/jasmin/pull/343),
+  ([PR #365](https://github.com/jasmin-lang/jasmin/pull/365);
   fixes [#314](https://github.com/jasmin-lang/jasmin/issues/314)).
 
 - Safety checker better handles integer shift operators

compiler/safety/fail/init-join.jazz

@@ -0,0 +1,13 @@
+export
+fn main(reg u64 x) -> reg u64 {
+  reg u64 r;
+  if x > 0 {
+    r = 0;
+  }
+  return r;
+}
+
+inline fn test() {
+#inline _ = main(0);
+}
+exec test()

compiler/safety/success/align2.jazz

@@ -1,12 +1,14 @@
 export
 fn main(reg u64 pt) -> reg u64 {
-  reg u64 tmp, i;
+  reg u64 tmp res i;
 
+  res = 0;
   i = 0;
   while (i < 16) {
     tmp = (u64)[pt + 8*i];
+    res += tmp;
     i += 1;
   }
-  
-  return tmp;
+
+  return res;
 }

compiler/src/safety/domains/safetyBoolean.ml

@@ -323,12 +323,12 @@ module Init : InitT = struct
   let meet = Mm.merge (fun _ b b' ->
       let b = odfl false b
       and b' = odfl false b' in
-      Some (b && b'))
+      Some (b || b'))
 
   let join = Mm.merge (fun _ b b' ->
       let b = odfl false b
       and b' = odfl false b' in
-      Some (b || b'))
+      Some (b && b'))
 
   let widening = join
 
@@ -469,11 +469,10 @@ module AbsBoolNoRel (AbsNum : AbsNumT) (Pt : PointsTo) (Sym : SymExpr)
       (* TODO: check why not NR.meet ? *)
       EMs.map2 AbsNum.NR.unify eb eb'
 
-  let meet ~join_align ~join_init t t' =
+  let meet ~join_align t t' =
     let t,t'    = merge_bool_dom t t' in
     { bool      = Mbv2.map2 AbsNum.NR.meet t.bool t'.bool;
-      init      =
-        (if join_init then Init.join else Init.meet) t.init t'.init;
+      init      = Init.meet t.init t'.init;
       num       = AbsNum.R.meet t.num t'.num;
       points_to = Pt.meet t.points_to t'.points_to;
       sym       = Sym.meet t.sym t'.sym;

compiler/src/safety/domains/safetyInterfaces.ml

@@ -216,7 +216,7 @@ module type AbsNumBoolType = sig
   (* Make a top value defined on the given variables *)
   val make : mvar list -> mem_loc list -> t
 
-  val meet : join_align:bool -> join_init:bool -> t -> t -> t    
+  val meet : join_align:bool -> t -> t -> t
   val join : t -> t -> t
   val widening : Mtcons.t option -> t -> t -> t
 

compiler/src/safety/safetyInterpreter.ml

@@ -866,7 +866,7 @@ end = struct
        Also, every variable (of the callee or caller) which was initalized
        remains so. *)   
     let abs = AbsDom.meet
-        ~join_align:true ~join_init:true
+        ~join_align:true
         state.abs fstate.abs in
     let state = { abs = abs;
                   it = fstate.it;