CT extraction: fix #202

jasmin-lang · Sep 1, 2022 · 57694f6 · 57694f6
1 parent 3d40bc8
commit 57694f6
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 1 deletion.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -33,6 +33,10 @@
   ([PR #227](https://github.com/jasmin-lang/jasmin/pull/227);
   fixes [#190](https://github.com/jasmin-lang/jasmin/issues/190)).
 
+- Fix a failing assertion in extraction to EasyCrypt for constant-time
+  ([PR #229](https://github.com/jasmin-lang/jasmin/pull/229);
+  fixes [#202](https://github.com/jasmin-lang/jasmin/issues/202)).
+
 ## New features
 
 - Fill an array with “random” data using `p = #randombytes(p);`

diff --git a/compiler/src/toEC.ml b/compiler/src/toEC.ml
@@ -1086,7 +1086,7 @@ module Leak = struct
 
   let rec init_aux_i env i = 
     match i.i_desc with
-    | Cassgn (lv, _, _, _) -> add_aux env [ty_lval lv]
+    | Cassgn (lv, _, _, e) -> add_aux (add_aux env [ty_lval lv]) [ty_expr e]
     | Copn (lvs, _, _, _) -> add_aux env (List.map ty_lval lvs)
     | Ccall(_, lvs, _, _) | Csyscall(lvs, _, _)->
       if lvs = [] then env