Small update to trivial sizeof rewrites so we can handle all cases in

aarch64 vector instructions.

There's maybe a better more general way to do this but I'm not sure
what that would be.

3 files changed, 11 insertions, 1 deletions

diff --git a/editors/sail2-mode.el b/editors/sail2-mode.el
index b93542b5..8dde96df 100644
--- a/editors/sail2-mode.el
+++ b/editors/sail2-mode.el
@@ -8,7 +8,7 @@
     "else" "match" "in" "return" "register" "forall" "operator" "effect"
     "overload" "cast" "sizeof" "constraint" "default" "assert"
     "pure" "infixl" "infixr" "infix" "scattered" "end" "try" "catch" "and"
-    "throw" "clause" "as" "repeat" "until" "while" "do"))
+    "throw" "clause" "as" "repeat" "until" "while" "do" "foreach"))
 
 (defconst sail2-kinds
   '("Int" "Type" "Order" "inc" "dec"
diff --git a/lib/ocaml_rts/sail_lib.ml b/lib/ocaml_rts/sail_lib.ml
index 3cf4505d..dfdd1db9 100644
--- a/lib/ocaml_rts/sail_lib.ml
+++ b/lib/ocaml_rts/sail_lib.ml
@@ -413,6 +413,8 @@ let real_power (x, y) = Num.power_num x (Num.num_of_big_int y)
 let add_real (x, y) = Num.add_num x y
 let sub_real (x, y) = Num.sub_num x y
 
+let abs_real x = Num.abs_num x
+
 let lt (x, y) = lt_big_int x y
 let gt (x, y) = gt_big_int x y
 let lteq (x, y) = le_big_int x y
@@ -422,6 +424,7 @@ let pow2 x = power_big_int_positive_int x 2
 
 let max_int (x, y) = max_big_int x y
 let min_int (x, y) = min_big_int x y
+let abs_int x = abs_big_int x
 
 let undefined_real () = Num.num_of_int 0
 
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 363761f5..13d811e4 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -167,6 +167,13 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp =
     let var = E_aux (E_id id, (l, Some (env, typ, no_effect))) in
     match destruct_atom_nexp env typ with
     | Some size when prove env (nc_eq size nexp) -> Some var
+    (* AA: This next case is a bit of a hack... is there a more
+       general way to deal with trivial nexps that are offset by
+       constants? This will resolve a 'n - 1 sizeof when 'n is in
+       scope. *)
+    | Some size when prove env (nc_eq (nsum size (nint 1)) nexp) ->
+       let one_exp = infer_exp env (mk_lit_exp (L_num unit_big_int)) in
+       Some (E_aux (E_app (mk_id "add_range", [var; one_exp]), (gen_loc l, Some (env, atom_typ (nsum size (nint 1)), no_effect))))
     | _ ->
        begin
          match destruct_vector env typ with