checksafety: reset A/M-var conversion table

CHANGELOG.md

@@ -45,6 +45,10 @@
   ([PR #313](https://github.com/jasmin-lang/jasmin/pull/313);
   fixes [#310](https://github.com/jasmin-lang/jasmin/issues/310)).
 
+- Fix to the safety checker
+  ([PR #315](https://github.com/jasmin-lang/jasmin/pull/315);
+  fixes [#314](https://github.com/jasmin-lang/jasmin/issues/314)).
+
 ## Other changes
 
 - Explicit if-then-else in flag combinations is no longer supported

compiler/safety/success/bug_314.jazz

@@ -0,0 +1,15 @@
+inline fn f(reg u32 i) {
+  reg bool zf;
+  while {
+    _,_,_,zf,i = #DEC_32(i);
+  } (!zf)
+}
+
+inline fn g() {
+  reg u32 i;
+  i = 42;
+  f(2);
+}
+
+export fn test1() { g(); }
+export fn test2() { g(); }

compiler/src/safety/domains/safetyNum.ml

@@ -268,6 +268,8 @@ module AbsNumI (Manager : AprManager) (PW : ProgWrap) : AbsNumType = struct
   type t = Manager.t Abstract1.t
   let man = Manager.man
 
+  let () = SafetyVar.reset ()
+
   let is_relational () = Ppl.manager_is_ppl man
 
   let make l =

compiler/src/safety/safetyVar.ml

@@ -143,6 +143,7 @@ let get_at = function
 (*---------------------------------------------------------------*)
 (* We log the result to be able to inverse it. *)
 let log_var = Hashtbl.create 16
+let reset () = Hashtbl.reset log_var
 
 let avar_of_mvar a =
   let s = string_of_mvar a in

compiler/src/safety/safetyVar.mli

@@ -49,6 +49,11 @@ val of_scope  : Expr.v_scope -> atype -> mvar
 val get_scope : mvar -> Expr.v_scope
 val get_at    : mvar -> atype
 
+(*---------------------------------------------------------------*)
+(** Resets the conversion table between [mvar] and [avar]. To
+  be called between two analyses. *)
+val reset : unit -> unit
+
 (*---------------------------------------------------------------*)
 val avar_of_mvar : mvar -> Apron.Var.t