WIP

JasonGross · Mar 7, 2025 · a1694d3 · a1694d3
1 parent 2d55a49
commit a1694d3
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 10 deletions.
diff --git a/rewriter b/rewriter
diff --git a/src/Assembly/Equivalence.v b/src/Assembly/Equivalence.v
@@ -780,7 +780,7 @@ Definition RevealWidth (i : idx) : symexM N :=
   then symex_return w
   else symex_error (Expected_power_of_two s i).
 
-Definition type_spec := list (option nat). (* list of array lengths; None means not an array *)
+Definition type_spec := list (N * option nat). (* list of element size in bytes * length; None means not an array *)
 
 (** Convert PHOAS info about types and argument bounds into a simplified specification *)
 Fixpoint simplify_base_type
@@ -843,23 +843,23 @@ Fixpoint build_inputs {descr:description} (types : type_spec) : dag.M (list (idx
      end%dagM.
 
 (* we factor this out so that conversion is not slow when proving things about this *)
-Definition compute_array_address {opts : symbolic_options_computed_opt} {descr:description} (base : idx) (i : nat)
-  := (offset <- Symbolic.App (zconst 64%N (8 * Z.of_nat i), nil);
+Definition compute_array_address {opts : symbolic_options_computed_opt} {descr:description} (bytes_per_element : N) (base : idx) (i : nat)
+  := (offset <- Symbolic.App (zconst 64%N (Z.of_N bytes_per_element * Z.of_nat i), nil);
       Symbolic.App (add 64%N, [base; offset]))%x86symex.
 
-Definition build_merge_array_addresses {opts : symbolic_options_computed_opt} {descr:description} (base : idx) (items : list idx) : M (list idx)
+Definition build_merge_array_addresses {opts : symbolic_options_computed_opt} {descr:description} {bytes_per_element : N} (base : idx) (items : list idx) : M (list idx)
   := mapM (fun '(i, idx) =>
-             (addr <- compute_array_address base i;
+             (addr <- compute_array_address bytes_per_element base i;
               (fun s => Success (addr, update_mem_with s (cons (addr,idx)))))
           )%x86symex (List.enumerate items).
 
-Fixpoint build_merge_base_addresses {opts : symbolic_options_computed_opt} {descr:description} {dereference_scalar:bool} (items : list (idx + list idx)) (reg_available : list REG) : M (list ((REG + idx) + idx))
+Fixpoint build_merge_base_addresses {opts : symbolic_options_computed_opt} {descr:description} {dereference_scalar:bool} {bytes_per_element : N} (items : list (idx + list idx)) (reg_available : list REG) : M (list ((REG + idx) + idx))
   := match items, reg_available with
      | [], _ | _, [] => Symbolic.ret []
      | inr idxs :: xs, r :: reg_available
        => (base <- SetRegFresh r; (* note: overwrites initial value *)
-           addrs <- build_merge_array_addresses base idxs; (* note: overwrites initial value *)
-           rest <- build_merge_base_addresses (dereference_scalar:=dereference_scalar) xs reg_available;
+           addrs <- build_merge_array_addresses (bytes_per_element:=bytes_per_element) base idxs; (* note: overwrites initial value *)
+           rest <- build_merge_base_addresses (dereference_scalar:=dereference_scalar) (bytes_per_element:=bytes_per_element) xs reg_available;
            Symbolic.ret (inr base :: rest))
      | inl idx :: xs, r :: reg_available =>
           (addr <- (if dereference_scalar
@@ -869,7 +869,7 @@ Fixpoint build_merge_base_addresses {opts : symbolic_options_computed_opt} {desc
                     else
                       (_ <- SetReg r idx; (* note: overwrites initial value *)
                        ret (inl r)));
-           rest <- build_merge_base_addresses (dereference_scalar:=dereference_scalar) xs reg_available;
+           rest <- build_merge_base_addresses (dereference_scalar:=dereference_scalar) (bytes_per_element:=bytes_per_element) xs reg_available;
            Symbolic.ret (inl addr :: rest))
      end%N%x86symex.