Wint2

CHANGELOG.md

@@ -22,11 +22,43 @@
   [PR #972](https://github.com/jasmin-lang/jasmin/pull/972),
   [PR #995](https://github.com/jasmin-lang/jasmin/pull/995)).
 
+- Introduction of types siXX and uiXX (XX in [8,16,32,64,128, 256]).
+  New notation for type uXX/sXX : wXX.
+  siXX represents signed integer of size XX, i.e in the range [-2^XX/2, 2^XX/2).
+  uiXX represents unsigned integer of size XX, i.e in the range [0, 2^XX).
+  Introduction of a new cast operorators:
+   (sint) e : from wXX/siXX to int, signed interpretation
+   (uint) e : from wXX/uiXX to int, unsigned interpretation
+  The previous cast operator (int) e stand for:
+   (uint) e if e has type wXX/uiXX
+   (sint) e if e has type siXX
+  All basic operations on uiXX/siXX perform the corresponding int operation and check
+  that the result is in the range of uiXX/siXX, if not it is a safety violation.
+  They can be selected explicitly using notation "e1 +XX(ui/si) e2"
+  Introduction of new cast operators:
+   (XXw) e : from siXX/uiXX to wXX
+   (XXsi) e :
+     if e has type wXX it the identity
+     if e has type int ensure that e is in the range of siXX, else it is a safety violation.
+   (XXui) e :
+     if e has type wXX it the identity
+     if e has type int ensure that e is in the range of siXX, else it is a safety violation.
+  Introduce zquot and zrem operators on int : "e1 /s e2" and "e1 %s e2".
+  The key feature of this new type are for the extraction to easycrypt.
+  They are extracted to int, removing the need to deal with modulus 2^XX operations.
+  ([PR #1071](https://github.com/jasmin-lang/jasmin/pull/1071)).
+
 ## Bug fixes
 
 - Fix EC extraction in case on nested loops
   ([PR #971](https://github.com/jasmin-lang/jasmin/pull/971)).
 
+- Fix semantics of (e1 /XXu e2) and (e1 %XXu e2), the safety condition only require that e2 <> 0.
+  ([PR #1071](https://github.com/jasmin-lang/jasmin/pull/1071)).
+
+- Fix extraction of (e1 /XXs e2) and (e1 %XXs e2) they are now correctly extracted to zquot and zrem.
+  ([PR #1071](https://github.com/jasmin-lang/jasmin/pull/1071)).
+
 ## Other changes
 
 - The deprecated legacy interface to the LATEX pretty-printer has been removed

compiler/entry/commonCLI.ml

@@ -73,7 +73,7 @@ let parse_and_compile (type reg regx xreg rflag cond asm_op extra_op)
        and type rflag = rflag
        and type cond = cond
        and type asm_op = asm_op
-       and type extra_op = extra_op) pass file idirs =
+       and type extra_op = extra_op) ~wi2i pass file idirs =
   let _env, pprog, _ast =
     try Compile.parse_file Arch.arch_info ~idirs file with
     | Annot.AnnotationError (loc, code) ->
@@ -90,6 +90,10 @@ let parse_and_compile (type reg regx xreg rflag cond asm_op extra_op)
       hierror ~loc:(Lmore loc) ~kind:"typing error" "%s" code
   in
 
+  let prog =
+    if not wi2i then prog
+    else Compile.do_wint_int (module Arch) prog in
+
   let prog =
     if pass <= Compiler.ParamsExpansion then prog
     else
@@ -112,3 +116,4 @@ let parse_and_compile (type reg regx xreg rflag cond asm_op extra_op)
       | exception E.Found -> !res
   in
   prog
+

compiler/entry/commonCLI.mli

@@ -17,10 +17,11 @@ val parse_and_compile :
       and type regx = 'regx
       and type rflag = 'rflag
       and type xreg = 'xreg) ->
+  wi2i:bool -> (* true => start by replacing wint operation by int operation *)
   Compiler.compiler_step ->
   string ->
   (string * string) list ->
-  ( unit,
+  (unit,
     ( 'reg,
       'regx,
       'xreg,

compiler/entry/jasmin2ec.ml

@@ -36,8 +36,7 @@ let parse_and_extract arch call_conv idirs =
   let module A = (val get_arch_module arch call_conv) in
 
   let extract model amodel functions array_dir output pass file =
-    let prog = parse_and_compile (module A) pass file idirs in
-
+    let prog = parse_and_compile (module A) ~wi2i:true pass file idirs in
     extract_to_file prog arch A.reg_size A.asmOp model amodel functions
       array_dir output
   in

compiler/entry/jasmin_ct.ml

@@ -6,7 +6,7 @@ open Utils
 let parse_and_check arch call_conv idirs =
   let module A = (val get_arch_module arch call_conv) in
   let check ~doit infer ct_list speculative pass file =
-    let prog = parse_and_compile (module A) pass file idirs in
+    let prog = parse_and_compile (module A) ~wi2i:false pass file idirs in
 
     if speculative then
       let prog =