SCT: fix checking of while loops

CHANGELOG.md

@@ -11,6 +11,10 @@
   ([PR #880](https://github.com/jasmin-lang/jasmin/pull/880);
   fixes [#842](https://github.com/jasmin-lang/jasmin/issues/842)).
 
+- Fix SCT check of `while` loops
+  ([PR #888](https://github.com/jasmin-lang/jasmin/pull/888));
+  fixes [#887](https://github.com/jasmin-lang/jasmin/issues/887)).
+
 ## Other changes
 
 - The deprecated legacy interface to the LATEX pretty-printer has been removed

compiler/src/sct_checker_forward.ml

@@ -1127,9 +1127,9 @@ let rec ty_instr is_ct_asm fenv env ((msf,venv) as msf_e :msf_e) i =
     let (msf2, venv2) = ty_cmd is_ct_asm fenv env (msf1, venv1) c1 in
     ensure_public env venv2 loc e;
     let (msf', venv') = ty_cmd is_ct_asm fenv env (MSF.enter_if msf2 e, venv2) c2 in
-    let msf' = MSF.end_loop loc msf1 msf' in
+    let _ = MSF.end_loop loc msf1 msf' in
     Env.ensure_le loc venv' venv1; (* venv' <= venv1 *)
-    MSF.enter_if msf' (Papp1(Onot, e)), venv1
+    MSF.enter_if msf2 (Papp1(Onot, e)), venv2
 
   | Ccall (xs, f, es) ->
     let fty = FEnv.get_fty fenv f in

compiler/tests/sct-checker/accept.expected

@@ -148,6 +148,19 @@ output corruption: #public
  constraints:
 
 
+File bug_887.jazz:
+modmsf test_msf : #secret * #transient ->
+
+output corruption: #public
+ constraints:
+
+
+modmsf test_venv : #secret ->
+#public
+output corruption: #public
+ constraints:
+
+
 File corruption.jazz:
 nomodmsf corrupts_memory : #public * #secret *
                            #[ptr = public, val = secret] *

compiler/tests/sct-checker/fail/bug_887.jazz

@@ -0,0 +1,14 @@
+/* In this example, r is public most of the time, except when the loop exits. */
+#[sct="secret → ()"]
+fn test_venv(reg u64 s) {
+  reg u64 i r;
+  r = 0;
+  i = 0;
+  while {
+    r = s;
+  } (i < 10) {
+    r = 0;
+    i += 1;
+  }
+  [r] = 0;
+}

compiler/tests/sct-checker/reject.expected

@@ -27,6 +27,9 @@ Failed as expected after_branch: "fail/basic.jazz", line 10 (18-19):
                                    } are
 Failed as expected leak_transient: "fail/basic.jazz", line 1 (42-50):
                                    speculative constant type checker: x has type #transient but should be at most #public
+File bug_887.jazz:
+Failed as expected test_venv: "fail/bug_887.jazz", line 13 (3-4):
+                              speculative constant type checker: r has type #secret but should be at most #public
 File corruption.jazz:
 Failed as expected does_corrupt_memory: "fail/corruption.jazz", line 26 (12-13):
                                         speculative constant type checker: return type for y is #[ptr = public, val = transient] it should be less than #[ptr = public, val = public]

compiler/tests/sct-checker/success/bug_887.jazz

@@ -0,0 +1,23 @@
+fn test_msf(reg u64 msf x) {
+  while {
+    msf = #init_msf();
+  } (x != 0) {
+    msf = #update_msf(x != 0, msf);
+    x = 0;
+  }
+  msf = #update_msf(! (x != 0), msf);
+}
+
+#[sct="secret → public"]
+fn test_venv(reg u64 s) -> reg u64 {
+  reg u64 i r;
+  r = 0;
+  i = 0;
+  while {
+    r = 0;
+  } (i < 10) {
+    r = s;
+    i += 1;
+  }
+  return r;
+}