From 0952ebb7800fe1c396f6916c33bbc19a3b895308 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 28 Nov 2017 18:48:19 +0000
Subject: 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.
---
 src/rewrites.ml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'src')

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
-- 
cgit v1.2.3