From a1694d39fd1a704a903307afb89f789190f6c959 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 7 Mar 2025 11:33:04 -0800 Subject: [PATCH] WIP --- rewriter | 2 +- src/Assembly/Equivalence.v | 18 +++++++++--------- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/rewriter b/rewriter index 869b054883..1e17dcd210 160000 --- a/rewriter +++ b/rewriter @@ -1 +1 @@ -Subproject commit 869b05488312360d947f393fd33491d4c9478147 +Subproject commit 1e17dcd2101af6683ee4566d58f543e97a5d6b22 diff --git a/src/Assembly/Equivalence.v b/src/Assembly/Equivalence.v index 2006770e83..be60e7505a 100644 --- 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.