diff options
| -rw-r--r-- | src/common/Coquplib.v | 2 | ||||
| -rw-r--r-- | src/common/IntegerExtra.v | 36 | ||||
| -rw-r--r-- | src/common/Monad.v | 4 | ||||
| -rw-r--r-- | src/extraction/Extraction.v | 4 | ||||
| -rw-r--r-- | src/translation/HTLgen.v | 92 | ||||
| -rw-r--r-- | src/translation/HTLgenspec.v | 35 | ||||
| -rw-r--r-- | src/verilog/PrintHTL.ml | 2 | ||||
| -rw-r--r-- | src/verilog/PrintVerilog.ml | 10 | ||||
| -rw-r--r-- | src/verilog/PrintVerilog.mli | 4 | ||||
| -rw-r--r-- | src/verilog/Verilog.v | 33 |
10 files changed, 131 insertions, 91 deletions
diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v index 2295ff6..469eddc 100644 --- a/src/common/Coquplib.v +++ b/src/common/Coquplib.v @@ -235,3 +235,5 @@ Definition debug_show {A B : Type} `{Show A} (a : A) (b : B) : B := Definition debug_show_msg {A B : Type} `{Show A} (s : string) (a : A) (b : B) : B := let unused := debug_print (s ++ show a) in b. + +Notation "f $ x" := (f x) (at level 60, right associativity, only parsing). diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v index fe7d94f..8e32c2c 100644 --- a/src/common/IntegerExtra.v +++ b/src/common/IntegerExtra.v @@ -298,44 +298,48 @@ Module IntExtra. (or (shl (repr (Byte.unsigned c)) (repr Byte.zwordsize)) (repr (Byte.unsigned d)))). - Definition byte1 (n: int) : byte := Byte.repr (unsigned n). + Definition byte0 (n: int) : byte := Byte.repr $ unsigned n. + Definition ibyte0 (n: int) : int := Int.repr $ Byte.unsigned $ byte0 n. - Definition byte2 (n: int) : byte := Byte.repr (unsigned (shru n (repr Byte.zwordsize))). + Definition byte1 (n: int) : byte := Byte.repr $ unsigned $ shru n $ repr Byte.zwordsize. + Definition ibyte1 (n: int) : int := Int.repr $ Byte.unsigned $ byte1 n. - Definition byte3 (n: int) : byte := Byte.repr (unsigned (shru n (repr (2 * Byte.zwordsize)))). + Definition byte2 (n: int) : byte := Byte.repr $ unsigned $ shru n $ repr (2 * Byte.zwordsize). + Definition ibyte2 (n: int) : int := Int.repr $ Byte.unsigned $ byte2 n. - Definition byte4 (n: int) : byte := Byte.repr (unsigned (shru n (repr (3 * Byte.zwordsize)))). + Definition byte3 (n: int) : byte := Byte.repr $ unsigned $ shru n $ repr (3 * Byte.zwordsize). + Definition ibyte3 (n: int) : int := Int.repr $ Byte.unsigned $ byte3 n. - Lemma bits_byte1: - forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte1 n) i = testbit n i. + Lemma bits_byte0: + forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte0 n) i = testbit n i. Proof. - intros. unfold byte1. rewrite Byte.testbit_repr; auto. + intros. unfold byte0. rewrite Byte.testbit_repr; auto. Qed. - Lemma bits_byte2: - forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte2 n) i = testbit n (i + Byte.zwordsize). + Lemma bits_byte1: + forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte1 n) i = testbit n (i + Byte.zwordsize). Proof. - intros. unfold byte2. rewrite Byte.testbit_repr; auto. + intros. unfold byte1. rewrite Byte.testbit_repr; auto. assert (zwordsize = 4 * Byte.zwordsize) by reflexivity. fold (testbit (shru n (repr Byte.zwordsize)) i). rewrite bits_shru. change (unsigned (repr Byte.zwordsize)) with Byte.zwordsize. apply zlt_true. omega. omega. Qed. - Lemma bits_byte3: - forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte3 n) i = testbit n (i + (2 * Byte.zwordsize)). + Lemma bits_byte2: + forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte2 n) i = testbit n (i + (2 * Byte.zwordsize)). Proof. - intros. unfold byte3. rewrite Byte.testbit_repr; auto. + intros. unfold byte2. rewrite Byte.testbit_repr; auto. assert (zwordsize = 4 * Byte.zwordsize) by reflexivity. fold (testbit (shru n (repr (2 * Byte.zwordsize))) i). rewrite bits_shru. change (unsigned (repr (2 * Byte.zwordsize))) with (2 * Byte.zwordsize). apply zlt_true. omega. omega. Qed. - Lemma bits_byte4: - forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte4 n) i = testbit n (i + (3 * Byte.zwordsize)). + Lemma bits_byte3: + forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte3 n) i = testbit n (i + (3 * Byte.zwordsize)). Proof. - intros. unfold byte4. rewrite Byte.testbit_repr; auto. + intros. unfold byte3. rewrite Byte.testbit_repr; auto. assert (zwordsize = 4 * Byte.zwordsize) by reflexivity. fold (testbit (shru n (repr (3 * Byte.zwordsize))) i). rewrite bits_shru. change (unsigned (repr (3 * Byte.zwordsize))) with (3 * Byte.zwordsize). diff --git a/src/common/Monad.v b/src/common/Monad.v index 8517186..628963e 100644 --- a/src/common/Monad.v +++ b/src/common/Monad.v @@ -20,6 +20,10 @@ Module MonadExtra(M : Monad). Module MonadNotation. + Notation "A ; B" := + (bind A (fun _ => B)) + (at level 200, B at level 200). + Notation "'do' X <- A ; B" := (bind A (fun X => B)) (at level 200, X ident, A at level 100, B at level 200). diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index df21dc4..5d10cd7 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -16,7 +16,7 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From coqup Require Verilog Value Compiler. +From coqup Require Verilog ValueInt Compiler. From Coq Require DecidableClass. @@ -167,7 +167,7 @@ Set Extraction AccessOpaque. Cd "src/extraction". Separate Extraction - Verilog.module Value.uvalueToZ coqup.Compiler.transf_hls + Verilog.module ValueInt.uvalueToZ coqup.Compiler.transf_hls Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index b4f6b51..65b6627 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -292,26 +292,16 @@ Definition check_address_parameter_unsigned (p : Z) : bool := Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr := match a, args with (* TODO: We should be more methodical here; what are the possibilities?*) | Op.Aindexed off, r1::nil => - if (check_address_parameter_signed off) - then ret (boplitz Vadd r1 off) - else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed): address misaligned") + ret (boplitz Vadd r1 off) | Op.Ascaled scale offset, r1::nil => - if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) - then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue offset))) - else error (Errors.msg "Veriloggen: translate_eff_addressing (Ascaled): address misaligned") + ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue offset))) | Op.Aindexed2 offset, r1::r2::nil => - if (check_address_parameter_signed offset) - then ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 offset)) - else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2): address misaligned") + ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 offset)) | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) - if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) - then ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) - else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2scaled): address misaligned") + ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) let a := Integers.Ptrofs.unsigned a in - if (check_address_parameter_unsigned a) - then ret (Vlit (ZToValue a)) - else error (Errors.msg "Veriloggen: translate_eff_addressing (Ainstack): address misaligned") + ret (Vlit (ZToValue a)) | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing") end. @@ -390,27 +380,27 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := | _, _ => Error (Errors.msg "Htlgen: add_branch_instr") end. -Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) - (args : list reg) (stack : reg) : mon expr := - match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*) - | Mint32, Op.Aindexed off, r1::nil => - if (check_address_parameter_signed off) - then ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 4)))) - else error (Errors.msg "HTLgen: translate_arr_access address misaligned") - | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) - if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) - then ret (Vvari stack - (Vbinop Vdivu - (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) - (Vlit (ZToValue 4)))) - else error (Errors.msg "HTLgen: translate_arr_access address misaligned") - | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) - let a := Integers.Ptrofs.unsigned a in - if (check_address_parameter_unsigned a) - then ret (Vvari stack (Vlit (ZToValue (a / 4)))) - else error (Errors.msg "HTLgen: eff_addressing misaligned stack offset") - | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing") - end. +(* Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) *) +(* (args : list reg) (stack : reg) : mon expr := *) +(* match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*) *) +(* | Mint32, Op.Aindexed off, r1::nil => *) +(* if (check_address_parameter_signed off) *) +(* then ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 4)))) *) +(* else error (Errors.msg "HTLgen: translate_arr_access address misaligned") *) +(* | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) *) +(* if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) *) +(* then ret (Vvari stack *) +(* (Vbinop Vdivu *) +(* (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) *) +(* (Vlit (ZToValue 4)))) *) +(* else error (Errors.msg "HTLgen: translate_arr_access address misaligned") *) +(* | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) *) +(* let a := Integers.Ptrofs.unsigned a in *) +(* if (check_address_parameter_unsigned a) *) +(* then ret (Vvari stack (Vlit (ZToValue (a / 4)))) *) +(* else error (Errors.msg "HTLgen: eff_addressing misaligned stack offset") *) +(* | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing") *) +(* end. *) Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) := match ns with @@ -424,6 +414,20 @@ Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) := end) (enumerate 0 ns). +Definition create_single_cycle_load (stack : reg) (addr : expr) (dst : reg) : stmnt := + let l0 := Vnonblock (Vvarb0 dst) (Vvari stack addr) in + let l1 := Vnonblock (Vvarb1 dst) (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 1)) in + let l2 := Vnonblock (Vvarb2 dst) (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) in + let l3 := Vnonblock (Vvarb3 dst) (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) + in Vseq l0 $ Vseq l1 $ Vseq l2 $ l3. + +Definition create_single_cycle_store (stack : reg) (addr : expr) (src : reg) : stmnt := + let l0 := Vnonblock (Vvari stack addr) (Vvarb0 src) in + let l1 := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 1)) (Vvarb1 src) in + let l2 := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) (Vvarb2 src) in + let l3 := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) (Vvarb3 src) + in Vseq l0 $ Vseq l1 $ Vseq l2 $ l3. + Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit := match ni with (n, i) => @@ -439,15 +443,15 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni add_instr n n' (nonblock dst instr) else error (Errors.msg "State is larger than 2^32.") | Iload mem addr args dst n' => - if Z.leb (Z.pos n') Integers.Int.max_unsigned then - do src <- translate_arr_access mem addr args stack; - do _ <- declare_reg None dst 32; - add_instr n n' (nonblock dst src) + if Z.leb (Z.pos n') Integers.Int.max_unsigned + then do addr' <- translate_eff_addressing addr args; + do _ <- declare_reg None dst 32; + add_instr n n' $ create_single_cycle_load stack addr' dst else error (Errors.msg "State is larger than 2^32.") | Istore mem addr args src n' => - if Z.leb (Z.pos n') Integers.Int.max_unsigned then - do dst <- translate_arr_access mem addr args stack; - add_instr n n' (Vnonblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *) + if Z.leb (Z.pos n') Integers.Int.max_unsigned + then do addr' <- translate_eff_addressing addr args; + add_instr n n' $ create_single_cycle_store stack addr' src else error (Errors.msg "State is larger than 2^32.") | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.") | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.") @@ -554,7 +558,7 @@ Definition transf_module (f: function) : mon module := if stack_correct f.(fn_stacksize) then do fin <- create_reg (Some Voutput) 1; do rtrn <- create_reg (Some Voutput) 32; - do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4)); + do (stack, stack_len) <- create_arr None 8 (Z.to_nat f.(fn_stacksize)); do _ <- collectlist (transf_instr fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code)); do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(RTL.fn_params); do start <- create_reg (Some Vinput) 1; diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index f0508bd..aba5d0c 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -138,16 +138,17 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt - tr_instr fin rtrn st stk (RTL.Ireturn (Some r)) (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r))) Vskip | tr_instr_Iload : - forall mem addr args s s' i c dst n, + forall mem addr args s s' i e dst n, Z.pos n <= Int.max_unsigned -> - translate_arr_access mem addr args stk s = OK c s' i -> - tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (nonblock dst c) (state_goto st n) + translate_eff_addressing addr args s = OK e s' i -> + tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) + (create_single_cycle_load stk e dst) (state_goto st n) | tr_instr_Istore : - forall mem addr args s s' i c src n, + forall mem addr args s s' i e src n, Z.pos n <= Int.max_unsigned -> - translate_arr_access mem addr args stk s = OK c s' i -> - tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src)) - (state_goto st n) + translate_eff_addressing addr args s = OK e s' i -> + tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) + (create_single_cycle_store stk e src) (state_goto st n) | tr_instr_Ijumptable : forall cexpr tbl r, cexpr = tbl_to_case_expr st tbl -> @@ -175,7 +176,7 @@ Inductive tr_module (f : RTL.function) : module -> Prop := st stk stk_len fin rtrn start rst clk scldecls arrdecls wf) -> (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> - stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> + stk_len = Z.to_nat f.(RTL.fn_stacksize) -> Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 -> 0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus -> st = ((RTL.max_reg_function f) + 1)%positive -> @@ -377,15 +378,6 @@ Proof. Qed. Hint Resolve translate_instr_freshreg_trans : htlspec. -Lemma translate_arr_access_freshreg_trans : - forall mem addr args st s r s' i, - translate_arr_access mem addr args st s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - intros. unfold translate_arr_access in H. repeat (unfold_match H); inv H; eauto with htlspec. -Qed. -Hint Resolve translate_arr_access_freshreg_trans : htlspec. - Lemma add_instr_freshreg_trans : forall n n' st s r s' i, add_instr n n' st s = OK r s' i -> @@ -423,10 +415,13 @@ Proof. destruct i0; try (monadInv H); try (unfold_match H); eauto with htlspec. - monadInv H. apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ. apply declare_reg_freshreg_trans in EQ1. congruence. - - monadInv H. apply add_instr_freshreg_trans in EQ2. apply translate_arr_access_freshreg_trans in EQ. + - monadInv H. apply add_instr_freshreg_trans in EQ2. + apply translate_eff_addressing_freshreg_trans in EQ. apply declare_reg_freshreg_trans in EQ1. congruence. - - monadInv H. apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_freshreg_trans in EQ. congruence. - - monadInv H. apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0. + - monadInv H. apply add_instr_freshreg_trans in EQ0. + apply translate_eff_addressing_freshreg_trans in EQ. congruence. + - monadInv H. apply translate_condition_freshreg_trans in EQ. + apply add_branch_instr_freshreg_trans in EQ0. congruence. - inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence. Qed. diff --git a/src/verilog/PrintHTL.ml b/src/verilog/PrintHTL.ml index 0bdba51..36fdd3c 100644 --- a/src/verilog/PrintHTL.ml +++ b/src/verilog/PrintHTL.ml @@ -16,7 +16,7 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -open Value +open ValueInt open Datatypes open Camlcoq open AST diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml index 5265c97..db78ad5 100644 --- a/src/verilog/PrintVerilog.ml +++ b/src/verilog/PrintVerilog.ml @@ -17,7 +17,7 @@ *) open Verilog -open Value +open ValueInt open Datatypes open Camlcoq @@ -70,11 +70,17 @@ let unop = function let register a = sprintf "reg_%d" (P.to_int a) -let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (uvalueToZ l)) +let literal l = sprintf "32'd%d" (Z.to_int (uvalueToZ l)) + +let byte n s = sprintf "reg_%d[%d:%d]" (P.to_int s) (7 + n * 8) (n * 8) let rec pprint_expr = function | Vlit l -> literal l | Vvar s -> register s + | Vvarb0 s -> byte 0 s + | Vvarb1 s -> byte 1 s + | Vvarb2 s -> byte 2 s + | Vvarb3 s -> byte 3 s | Vvari (s, i) -> concat [register s; "["; pprint_expr i; "]"] | Vinputvar s -> register s | Vunop (u, e) -> concat ["("; unop u; pprint_expr e; ")"] diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli index 62bf63f..5fd8fe9 100644 --- a/src/verilog/PrintVerilog.mli +++ b/src/verilog/PrintVerilog.mli @@ -18,8 +18,8 @@ val pprint_stmnt : int -> Verilog.stmnt -> string -val print_value : out_channel -> Value.value -> unit +val print_value : out_channel -> ValueInt.value -> unit val print_program : bool -> out_channel -> Verilog.program -> unit -val print_result : out_channel -> (BinNums.positive * Value.value) list -> unit +val print_result : out_channel -> (BinNums.positive * ValueInt.value) list -> unit diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 9659189..108ac72 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -29,7 +29,7 @@ Require Import Lia. Import ListNotations. -From coqup Require Import common.Coquplib common.Show verilog.ValueInt AssocMap Array. +From coqup Require Import common.Coquplib common.Show verilog.ValueInt IntegerExtra AssocMap Array. From compcert Require Events. From compcert Require Import Integers Errors Smallstep Globalenvs. @@ -154,9 +154,13 @@ Inductive unop : Type := (** ** Expressions *) Inductive expr : Type := -| Vlit : value -> expr -| Vvar : reg -> expr -| Vvari : reg -> expr -> expr +| Vlit : value -> expr (** literal *) +| Vvar : reg -> expr (** reg *) +| Vvarb0 : reg -> expr (** 1st byte projection of reg *) +| Vvarb1 : reg -> expr +| Vvarb2 : reg -> expr +| Vvarb3 : reg -> expr +| Vvari : reg -> expr -> expr (** array *) | Vinputvar : reg -> expr | Vbinop : binop -> expr -> expr -> expr | Vunop : unop -> expr -> expr @@ -340,6 +344,22 @@ Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop forall fext reg stack v r, reg#r = v -> expr_runp fext reg stack (Vvar r) v + | erun_Vvarb0 : + forall fext reg stack v r, + reg#r = v -> + expr_runp fext reg stack (Vvarb0 r) (IntExtra.ibyte0 v) + | erun_Vvarb1 : + forall fext reg stack v r, + reg#r = v -> + expr_runp fext reg stack (Vvarb1 r) (IntExtra.ibyte1 v) + | erun_Vvarb2 : + forall fext reg stack v r, + reg#r = v -> + expr_runp fext reg stack (Vvarb2 r) (IntExtra.ibyte2 v) + | erun_Vvarb3 : + forall fext reg stack v r, + reg#r = v -> + expr_runp fext reg stack (Vvarb3 r) (IntExtra.ibyte3 v) | erun_Vvari : forall fext reg stack v iexp i r, expr_runp fext reg stack iexp i -> @@ -429,6 +449,7 @@ Definition access_fext (f : fext) (r : reg) : res value := Inductive location : Type := | LocReg (_ : reg) +| LocRegB (_ : reg) (_ : nat) | LocArray (_ : reg) (_ : nat). Inductive location_is : fext -> assocmap -> assocmap_arr -> expr -> location -> Prop := @@ -777,6 +798,10 @@ Proof. repeat (try match goal with | [ H : expr_runp _ _ _ (Vlit _) _ |- _ ] => invert H | [ H : expr_runp _ _ _ (Vvar _) _ |- _ ] => invert H + | [ H : expr_runp _ _ _ (Vvarb0 _) _ |- _ ] => invert H + | [ H : expr_runp _ _ _ (Vvarb1 _) _ |- _ ] => invert H + | [ H : expr_runp _ _ _ (Vvarb2 _) _ |- _ ] => invert H + | [ H : expr_runp _ _ _ (Vvarb3 _) _ |- _ ] => invert H | [ H : expr_runp _ _ _ (Vvari _ _) _ |- _ ] => invert H | [ H : expr_runp _ _ _ (Vinputvar _) _ |- _ ] => invert H | [ H : expr_runp _ _ _ (Vbinop _ _ _) _ |- _ ] => invert H |