WIword_of_int -> WIwint_of_int

Author: bgregoir

compiler/safetylib/safetyAbsExpr.ml

@@ -96,11 +96,11 @@ let remove_Owi2 o =
 
 let rec remove_Owi1 sg o e =
   match o with
-  | E.WIword_of_int sz -> Papp1(E.Oword_of_int sz, e)
-  | E.WIint_of_word sz -> Papp1(E.Oint_of_word(sg, sz), e)
+  | E.WIwint_of_int sz -> Papp1(E.Oword_of_int sz, e)
+  | E.WIint_of_wint sz -> Papp1(E.Oint_of_word(sg, sz), e)
   | E.WIword_of_wint _ -> remove_Owi e
   | E.WIwint_of_word _ -> remove_Owi e
-  | E.WIword_ext(szo, szi) ->
+  | E.WIwint_ext(szo, szi) ->
     let o = if sg = Signed then E.Osignext(szo, szi) else E.Ozeroext(szo, szi) in
     Papp1(o, e)
   | E.WIneg sz -> Papp1(E.Oneg (Op_w sz), e)

compiler/safetylib/safetyInterpreter.ml

@@ -279,11 +279,11 @@ let safe_op1 o e1 =
   match o with
   | E.Owi1(sg, o) ->
     begin match o with
-    | E.WIword_of_int sz -> [in_wint_range sg sz e1]
-    | E.WIint_of_word sz -> []
+    | E.WIwint_of_int sz -> [in_wint_range sg sz e1]
+    | E.WIint_of_wint sz -> []
     | E.WIword_of_wint _ -> []
     | E.WIwint_of_word _ -> []
-    | E.WIword_ext(szo, szi) -> [] (* Check this ! *)
+    | E.WIwint_ext(szo, szi) -> [] (* Check this ! *)
     | E.WIneg sz ->
       if sg = Signed then [NotEqual(None, wint_to_int sg sz e1, Pconst (Z.neg (half_modulus sz)))]
       else [InRange(Pconst Z.zero, Pconst Z.zero, wint_to_int sg sz e1)]

compiler/src/pretyping.ml

@@ -1031,12 +1031,12 @@ let wk_s_ws (s: W.signedness option) (ws: W.wsize) =
 let op_word_of_int (wk, s, ws) =
   match wk with
   | Word -> E.Oword_of_int ws
-  | WInt -> E.Owi1(s, E.WIword_of_int ws)
+  | WInt -> E.Owi1(s, E.WIwint_of_int ws)
 
 let op_int_of_word (wk, s, ws) =
   match wk with
   | Word -> E.Oint_of_word (s, ws)
-  | WInt -> E.Owi1(s, E.WIint_of_word ws)
+  | WInt -> E.Owi1(s, E.WIint_of_wint ws)
 
 let cast loc e ety ty =
   match ety, ty with
@@ -1294,7 +1294,7 @@ let rec tt_expr pd ?(mode=`AllVar) (env : 'asm Env.env) pe =
               s, wie, P.etwi s ws
          | `WInt s, P.ETint ->
              let s = tt_sign s in
-             s, Papp1(E.Owi1(s, E.WIword_of_int sz), e), P.etwi s sz
+             s, Papp1(E.Owi1(s, E.WIwint_of_int sz), e), P.etwi s sz
          | _ -> rs_tyerror ~loc:(L.loc pe) (InvalidCast(ety,rty))
        in
        (* ensures that the size is the expected *)
@@ -1304,9 +1304,9 @@ let rec tt_expr pd ?(mode=`AllVar) (env : 'asm Env.env) pe =
            let op = if s = W.Unsigned then E.Ozeroext(sz, ws) else E.Osignext(sz, ws) in
            P.Papp1(op, e)
          | P.ETword(Some W.Unsigned, ws) when W.wsize_cmp ws sz = Datatypes.Lt ->
-           P.Papp1(E.Owi1(s, E.WIword_ext(sz, ws)), e)
+           P.Papp1(E.Owi1(s, E.WIwint_ext(sz, ws)), e)
          | P.ETword(Some W.Signed, ws) ->
-           P.Papp1(E.Owi1(s, E.WIword_ext(sz, ws)), e)
+           P.Papp1(E.Owi1(s, E.WIwint_ext(sz, ws)), e)
          | _ -> e
        in
        e, rty

compiler/src/printCommon.ml

@@ -63,15 +63,15 @@ let string_of_wi_cast sg sz =
   asprintf "%d%s" (int_of_ws sz) (string_of_wi sg)
 
 let string_of_wiop1 sg = function
-  | E.WIword_of_int sz ->
+  | E.WIwint_of_int sz ->
       asprintf "(%s /* of int */)" (string_of_wi_cast sg sz)
-  | WIint_of_word sz ->
+  | WIint_of_wint sz ->
       asprintf "(%s /* of %s */)" (string_of_int_cast sg) (string_of_wi_ty sg sz)
   | WIword_of_wint sz ->
       asprintf "(%s /* of %s */)" (string_of_w_cast sz) (string_of_wi_ty sg sz)
   | WIwint_of_word sz ->
       asprintf "(%s /* of %s */)" (string_of_wi_cast sg sz) (string_of_w_ty sz)
-  | WIword_ext(szo, _) ->
+  | WIwint_ext(szo, _) ->
       asprintf "(%s)" (string_of_wi_cast sg szo)
   | WIneg sz ->
       asprintf "-%s" (string_of_wi_cast sg sz)

proofs/compiler/wint_int.v

@@ -78,21 +78,15 @@ Definition esubtype (ty1 ty2 : extended_type positive) :=
  | _, _ => false
  end.
 
-(*Definition word_of_int sg ws e :=
-  match e with
-  | Papp1 (Oint_of_word sg' ws') e1 => if (sg == sg') && (ws == ws') then e1 else Papp1 (Oword_of_int ws) e
-  | _ => Papp1 (Oword_of_int ws) e
-  end.*)
-
 Definition wi2i_op1_e (o : sop1) (e : pexpr) :=
   match is_wi1 o with
   | Some (s, o) =>
     match o with
-    | WIword_of_int ws => e
-    | WIint_of_word ws => e
+    | WIwint_of_int ws => e
+    | WIint_of_wint ws => e
     | WIword_of_wint ws => Papp1 (Oword_of_int ws) e
     | WIwint_of_word ws => Papp1 (Oint_of_word s ws) e
-    | WIword_ext szo szi =>
+    | WIwint_ext szo szi =>
       Papp1 (Oint_of_word s szo)
        (Papp1 (signed (Ozeroext szo szi) (Osignext szo szi) s)
          (Papp1 (Oword_of_int szi) e))

proofs/compiler/wint_word.v

@@ -17,11 +17,11 @@ Context `{asmop:asmOp}.
 
 Definition wi2w_wiop1 s (o : wiop1) (e : pexpr) : pexpr :=
   match o with
-  | WIword_of_int sz => Papp1 (Oword_of_int sz) e
-  | WIint_of_word sz => Papp1 (Oint_of_word s sz) e
+  | WIwint_of_int sz => Papp1 (Oword_of_int sz) e
+  | WIint_of_wint sz => Papp1 (Oint_of_word s sz) e
   | WIword_of_wint _ => e
   | WIwint_of_word _ => e
-  | WIword_ext sz1 sz2 =>
+  | WIwint_ext sz1 sz2 =>
     let o := if s is Unsigned then Ozeroext sz1 sz2 else Osignext sz1 sz2 in
     Papp1 o e
   | WIneg sz => Papp1 (Oneg (Op_w sz)) e

proofs/lang/expr.v

@@ -29,11 +29,11 @@ Variant op_kind :=
   | Op_w of wsize.
 
 Variant wiop1 :=
-| WIword_of_int  of wsize              (* int → word *)
-| WIint_of_word  of wsize (* word/uint/sint → int, signed or unsigned interpretation *)
+| WIwint_of_int  of wsize              (* int → word *)
+| WIint_of_wint  of wsize (* word/uint/sint → int, signed or unsigned interpretation *)
 | WIword_of_wint of wsize (* uint/sint -> word *)
 | WIwint_of_word of wsize (* word -> uint/sint *)
-| WIword_ext     of wsize & wsize (* Sign-extension: output-size, input-size *)
+| WIwint_ext     of wsize & wsize (* Sign-extension: output-size, input-size *)
 | WIneg          of wsize
 .
 
@@ -176,21 +176,21 @@ HB.instance Definition _ := hasDecEq.Build opN opN_eq_axiom.
 (* Type of unany operators: input, output *)
 Definition etype_of_wiop1 {len:Type} (s: signedness) (o:wiop1) : extended_type len * extended_type len :=
   match o with
-  | WIword_of_int  sz => (tint, twint s sz)
-  | WIint_of_word  sz => (twint s sz, tint)
+  | WIwint_of_int  sz => (tint, twint s sz)
+  | WIint_of_wint  sz => (twint s sz, tint)
   | WIword_of_wint sz => (twint s sz, tword sz)
   | WIwint_of_word sz => (tword sz, twint s sz)
-  | WIword_ext szo szi => (twint s szi, twint s szo)
+  | WIwint_ext szo szi => (twint s szi, twint s szo)
   | WIneg          sz => (twint s sz, twint s sz)
   end.
 
 Definition type_of_wiop1 (o:wiop1) : stype * stype :=
   match o with
-  | WIword_of_int  sz => (sint, sword sz)
-  | WIint_of_word  sz => (sword sz, sint)
+  | WIwint_of_int  sz => (sint, sword sz)
+  | WIint_of_wint  sz => (sword sz, sint)
   | WIword_of_wint sz => (sword sz, sword sz)
   | WIwint_of_word sz => (sword sz, sword sz)
-  | WIword_ext szo szi => (sword szi, sword szo)
+  | WIwint_ext szo szi => (sword szi, sword szo)
   | WIneg          sz => (sword sz, sword sz)
   end.
 

proofs/lang/sem_op_typed.v

@@ -12,13 +12,13 @@ Definition sem_wiop1_typed (sign : signedness) (o: wiop1) :
   let t := type_of_wiop1 o in
   sem_t t.1 → exec (sem_t t.2) :=
   match o return let t := type_of_wiop1 o in sem_t t.1 → exec (sem_t t.2) with
-  | WIword_of_int sz => wint_of_int sign sz
-  | WIint_of_word sz => mk_sem_sop1 (@int_of_word sign sz)
+  | WIwint_of_int sz => wint_of_int sign sz
+  | WIint_of_wint sz => mk_sem_sop1 (@int_of_word sign sz)
 
   | WIword_of_wint sz => mk_sem_sop1 (fun (w:word sz) => w)
   | WIwint_of_word sz => mk_sem_sop1 (fun (w:word sz) => w)
 
-  | WIword_ext szo szi => mk_sem_sop1 (@sem_word_extend sign szo szi)
+  | WIwint_ext szo szi => mk_sem_sop1 (@sem_word_extend sign szo szi)
 
   | WIneg sz => fun (w: word sz) => wint_of_int sign sz (- int_of_word sign w)
   end.