diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-02 18:30:25 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-02 18:30:25 +0200 |
commit | 71c58a8d494eafd847776446b0c246229b2bc9cf (patch) | |
tree | 7570087588f24b3b340baeed5871b398bf7fc390 /backend | |
parent | dc8b24fa2dd7ede561dd75458899cf42e9be09d2 (diff) | |
download | compcert-kvx-71c58a8d494eafd847776446b0c246229b2bc9cf.tar.gz compcert-kvx-71c58a8d494eafd847776446b0c246229b2bc9cf.zip |
avancement (il faut utiliser Vundef visiblement)
Diffstat (limited to 'backend')
-rw-r--r-- | backend/Allocation.v | 2 | ||||
-rw-r--r-- | backend/Allocproof.v | 8 | ||||
-rw-r--r-- | backend/CSE.v | 6 | ||||
-rw-r--r-- | backend/Constprop.v | 4 | ||||
-rw-r--r-- | backend/Deadcode.v | 4 | ||||
-rw-r--r-- | backend/Inlining.v | 4 | ||||
-rw-r--r-- | backend/Inliningspec.v | 6 | ||||
-rw-r--r-- | backend/Liveness.v | 2 | ||||
-rw-r--r-- | backend/RTL.v | 40 | ||||
-rw-r--r-- | backend/RTLgen.v | 2 | ||||
-rw-r--r-- | backend/RTLgenspec.v | 2 | ||||
-rw-r--r-- | backend/RTLtyping.v | 12 | ||||
-rw-r--r-- | backend/Renumber.v | 2 | ||||
-rw-r--r-- | backend/Renumberproof.v | 12 | ||||
-rw-r--r-- | backend/Tailcallproof.v | 13 | ||||
-rw-r--r-- | backend/Unusedglob.v | 2 | ||||
-rw-r--r-- | backend/Unusedglobproof.v | 32 | ||||
-rw-r--r-- | backend/ValueAnalysis.v | 2 |
18 files changed, 114 insertions, 41 deletions
diff --git a/backend/Allocation.v b/backend/Allocation.v index 13e14530..c2e80f1c 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -226,7 +226,7 @@ Definition pair_instr_block | operation_other _ _ => pair_Iop_block op args res s b end - | Iload chunk addr args dst s => + | Iload trap chunk addr args dst s => let (mv1, b1) := extract_moves nil b in match b1 with | Lload chunk' addr' args' dst' :: b2 => diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 1804f46b..ac4122bc 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -96,10 +96,10 @@ Inductive expand_block_shape: block_shape -> RTL.instruction -> LTL.bblock -> Pr expand_block_shape (BSopdead op args res mv s) (Iop op args res s) (expand_moves mv (Lbranch s :: k)) - | ebs_load: forall chunk addr args dst mv1 args' dst' mv2 s k, + | ebs_load: forall trap chunk addr args dst mv1 args' dst' mv2 s k, wf_moves mv1 -> wf_moves mv2 -> expand_block_shape (BSload chunk addr args dst mv1 args' dst' mv2 s) - (Iload chunk addr args dst s) + (Iload trap chunk addr args dst s) (expand_moves mv1 (Lload chunk addr args' dst' :: expand_moves mv2 (Lbranch s :: k))) | ebs_load2: forall addr addr2 args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s k, @@ -130,10 +130,10 @@ Inductive expand_block_shape: block_shape -> RTL.instruction -> LTL.bblock -> Pr (expand_moves mv1 (Lload Mint32 addr2 args' dst' :: expand_moves mv2 (Lbranch s :: k))) - | ebs_load_dead: forall chunk addr args dst mv s k, + | ebs_load_dead: forall trap chunk addr args dst mv s k, wf_moves mv -> expand_block_shape (BSloaddead chunk addr args dst mv s) - (Iload chunk addr args dst s) + (Iload trap chunk addr args dst s) (expand_moves mv (Lbranch s :: k)) | ebs_store: forall chunk addr args src mv1 args' src' s k, wf_moves mv1 -> diff --git a/backend/CSE.v b/backend/CSE.v index 6d3f6f33..aaaf492c 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -459,7 +459,7 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb before | Iop op args res s => add_op before res op args - | Iload chunk addr args dst s => + | Iload trap chunk addr args dst s => add_load before dst chunk addr args | Istore chunk addr args src s => let app := approx!!pc in @@ -529,14 +529,14 @@ Definition transf_instr (n: numbering) (instr: instruction) := let (op', args') := reduce _ combine_op n1 op args vl in Iop op' args' res s end - | Iload chunk addr args dst s => + | Iload trap chunk addr args dst s => let (n1, vl) := valnum_regs n args in match find_rhs n1 (Load chunk addr vl) with | Some r => Iop Omove (r :: nil) dst s | None => let (addr', args') := reduce _ combine_addr n1 addr args vl in - Iload chunk addr' args' dst s + Iload trap chunk addr' args' dst s end | Istore chunk addr args src s => let (n1, vl) := valnum_regs n args in diff --git a/backend/Constprop.v b/backend/Constprop.v index d8211ffe..b68f4cae 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -157,7 +157,7 @@ Definition transf_instr (f: function) (an: PMap.t VA.t) (rm: romem) let (op', args') := op_strength_reduction op args aargs in Iop op' args' res s' end - | Iload chunk addr args dst s => + | Iload trap chunk addr args dst s => let aargs := aregs ae args in let a := ValueDomain.loadv chunk rm am (eval_static_addressing addr aargs) in match const_for_result a with @@ -165,7 +165,7 @@ Definition transf_instr (f: function) (an: PMap.t VA.t) (rm: romem) Iop cop nil dst s | None => let (addr', args') := addr_strength_reduction addr args aargs in - Iload chunk addr' args' dst s + Iload trap chunk addr' args' dst s end | Istore chunk addr args src s => let aargs := aregs ae args in diff --git a/backend/Deadcode.v b/backend/Deadcode.v index 2286876e..1f208a91 100644 --- a/backend/Deadcode.v +++ b/backend/Deadcode.v @@ -123,7 +123,7 @@ Definition transfer (f: function) (approx: PMap.t VA.t) if is_dead nres then after else if is_int_zero nres then (kill res ne, nm) else (add_needs args (needs_of_operation op nres) (kill res ne), nm) - | Some (Iload chunk addr args dst s) => + | Some (Iload trap chunk addr args dst s) => let ndst := nreg ne dst in if is_dead ndst then after else if is_int_zero ndst then (kill dst ne, nm) @@ -175,7 +175,7 @@ Definition transf_instr (approx: PMap.t VA.t) (an: PMap.t NA.t) end else instr - | Iload chunk addr args dst s => + | Iload trap chunk addr args dst s => let ndst := nreg (fst an!!pc) dst in if is_dead ndst then Inop s diff --git a/backend/Inlining.v b/backend/Inlining.v index f7ee4166..9cf535b9 100644 --- a/backend/Inlining.v +++ b/backend/Inlining.v @@ -364,9 +364,9 @@ Definition expand_instr (ctx: context) (pc: node) (i: instruction): mon unit := | Iop op args res s => set_instr (spc ctx pc) (Iop (sop ctx op) (sregs ctx args) (sreg ctx res) (spc ctx s)) - | Iload chunk addr args dst s => + | Iload trap chunk addr args dst s => set_instr (spc ctx pc) - (Iload chunk (saddr ctx addr) (sregs ctx args) (sreg ctx dst) (spc ctx s)) + (Iload trap chunk (saddr ctx addr) (sregs ctx args) (sreg ctx dst) (spc ctx s)) | Istore chunk addr args src s => set_instr (spc ctx pc) (Istore chunk (saddr ctx addr) (sregs ctx args) (sreg ctx src) (spc ctx s)) diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index c345c942..e20fb373 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -270,10 +270,10 @@ Inductive tr_instr: context -> node -> instruction -> code -> Prop := Ple res ctx.(mreg) -> c!(spc ctx pc) = Some (Iop (sop ctx op) (sregs ctx args) (sreg ctx res) (spc ctx s)) -> tr_instr ctx pc (Iop op args res s) c - | tr_load: forall ctx pc c chunk addr args res s, + | tr_load: forall ctx pc c trap chunk addr args res s, Ple res ctx.(mreg) -> - c!(spc ctx pc) = Some (Iload chunk (saddr ctx addr) (sregs ctx args) (sreg ctx res) (spc ctx s)) -> - tr_instr ctx pc (Iload chunk addr args res s) c + c!(spc ctx pc) = Some (Iload trap chunk (saddr ctx addr) (sregs ctx args) (sreg ctx res) (spc ctx s)) -> + tr_instr ctx pc (Iload trap chunk addr args res s) c | tr_store: forall ctx pc c chunk addr args src s, c!(spc ctx pc) = Some (Istore chunk (saddr ctx addr) (sregs ctx args) (sreg ctx src) (spc ctx s)) -> tr_instr ctx pc (Istore chunk addr args src s) c diff --git a/backend/Liveness.v b/backend/Liveness.v index 16533158..afe11ae6 100644 --- a/backend/Liveness.v +++ b/backend/Liveness.v @@ -79,7 +79,7 @@ Definition transfer reg_list_live args (reg_dead res after) else after - | Iload chunk addr args dst s => + | Iload trap chunk addr args dst s => if Regset.mem dst after then reg_list_live args (reg_dead dst after) else diff --git a/backend/RTL.v b/backend/RTL.v index 9599a24a..d09cca77 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -36,6 +36,8 @@ Require Import Op Registers. Definition node := positive. +Inductive trapping_mode : Type := TRAP | NOTRAP. + Inductive instruction: Type := | Inop: node -> instruction (** No operation -- just branch to the successor. *) @@ -43,11 +45,12 @@ Inductive instruction: Type := (** [Iop op args dest succ] performs the arithmetic operation [op] over the values of registers [args], stores the result in [dest], and branches to [succ]. *) - | Iload: memory_chunk -> addressing -> list reg -> reg -> node -> instruction - (** [Iload chunk addr args dest succ] loads a [chunk] quantity from + | Iload: trapping_mode -> memory_chunk -> addressing -> list reg -> reg -> node -> instruction + (** [Iload trap chunk addr args dest succ] loads a [chunk] quantity from the address determined by the addressing mode [addr] and the values of the [args] registers, stores the quantity just read - into [dest], and branches to [succ]. *) + into [dest], and branches to [succ]. + If trap=NOTRAP, then failures lead to a default value written to [dest]. *) | Istore: memory_chunk -> addressing -> list reg -> reg -> node -> instruction (** [Istore chunk addr args src succ] stores the value of register [src] in the [chunk] quantity at the @@ -194,6 +197,8 @@ Definition find_function end end. +Definition default_notrap_load_value (chunk : memory_chunk) := Vundef. + (** The transitions are presented as an inductive predicate [step ge st1 t st2], where [ge] is the global environment, [st1] the initial state, [st2] the final state, and [t] the trace @@ -212,12 +217,25 @@ Inductive step: state -> trace -> state -> Prop := step (State s f sp pc rs m) E0 (State s f sp pc' (rs#res <- v) m) | exec_Iload: - forall s f sp pc rs m chunk addr args dst pc' a v, - (fn_code f)!pc = Some(Iload chunk addr args dst pc') -> + forall s f sp pc rs m trap chunk addr args dst pc' a v, + (fn_code f)!pc = Some(Iload trap chunk addr args dst pc') -> eval_addressing ge sp addr rs##args = Some a -> Mem.loadv chunk m a = Some v -> step (State s f sp pc rs m) E0 (State s f sp pc' (rs#dst <- v) m) + | exec_Iload_notrap1: + forall s f sp pc rs m chunk addr args dst pc', + (fn_code f)!pc = Some(Iload NOTRAP chunk addr args dst pc') -> + eval_addressing ge sp addr rs##args = None -> + step (State s f sp pc rs m) + E0 (State s f sp pc' (rs#dst <- (default_notrap_load_value chunk)) m) + | exec_Iload_notrap2: + forall s f sp pc rs m chunk addr args dst pc' a, + (fn_code f)!pc = Some(Iload NOTRAP chunk addr args dst pc') -> + eval_addressing ge sp addr rs##args = Some a -> + Mem.loadv chunk m a = None-> + step (State s f sp pc rs m) + E0 (State s f sp pc' (rs#dst <- (default_notrap_load_value chunk)) m) | exec_Istore: forall s f sp pc rs m chunk addr args src pc' a m', (fn_code f)!pc = Some(Istore chunk addr args src pc') -> @@ -299,8 +317,8 @@ Proof. Qed. Lemma exec_Iload': - forall s f sp pc rs m chunk addr args dst pc' rs' a v, - (fn_code f)!pc = Some(Iload chunk addr args dst pc') -> + forall s f sp pc rs m trap chunk addr args dst pc' rs' a v, + (fn_code f)!pc = Some(Iload trap chunk addr args dst pc') -> eval_addressing ge sp addr rs##args = Some a -> Mem.loadv chunk m a = Some v -> rs' = (rs#dst <- v) -> @@ -384,7 +402,7 @@ Definition successors_instr (i: instruction) : list node := match i with | Inop s => s :: nil | Iop op args res s => s :: nil - | Iload chunk addr args dst s => s :: nil + | Iload trap chunk addr args dst s => s :: nil | Istore chunk addr args src s => s :: nil | Icall sig ros args res s => s :: nil | Itailcall sig ros args => nil @@ -403,7 +421,7 @@ Definition instr_uses (i: instruction) : list reg := match i with | Inop s => nil | Iop op args res s => args - | Iload chunk addr args dst s => args + | Iload trap chunk addr args dst s => args | Istore chunk addr args src s => src :: args | Icall sig (inl r) args res s => r :: args | Icall sig (inr id) args res s => args @@ -422,7 +440,7 @@ Definition instr_defs (i: instruction) : option reg := match i with | Inop s => None | Iop op args res s => Some res - | Iload chunk addr args dst s => Some dst + | Iload trap chunk addr args dst s => Some dst | Istore chunk addr args src s => None | Icall sig ros args res s => Some res | Itailcall sig ros args => None @@ -462,7 +480,7 @@ Definition max_reg_instr (m: positive) (pc: node) (i: instruction) := match i with | Inop s => m | Iop op args res s => fold_left Pos.max args (Pos.max res m) - | Iload chunk addr args dst s => fold_left Pos.max args (Pos.max dst m) + | Iload trap chunk addr args dst s => fold_left Pos.max args (Pos.max dst m) | Istore chunk addr args src s => fold_left Pos.max args (Pos.max src m) | Icall sig (inl r) args res s => fold_left Pos.max args (Pos.max r (Pos.max res m)) | Icall sig (inr id) args res s => fold_left Pos.max args (Pos.max res m) diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 9d7a8506..a0ca0f17 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -436,7 +436,7 @@ Fixpoint transl_expr (map: mapping) (a: expr) (rd: reg) (nd: node) transl_exprlist map al rl no | Eload chunk addr al => do rl <- alloc_regs map al; - do no <- add_instr (Iload chunk addr rl rd nd); + do no <- add_instr (Iload TRAP chunk addr rl rd nd); transl_exprlist map al rl no | Econdition a b c => do nfalse <- transl_expr map c rd nd; diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 17022a7d..aa83da6d 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -707,7 +707,7 @@ Inductive tr_expr (c: code): tr_expr c map pr (Eop op al) ns nd rd dst | tr_Eload: forall map pr chunk addr al ns nd rd n1 rl dst, tr_exprlist c map pr al ns n1 rl -> - c!n1 = Some (Iload chunk addr rl rd nd) -> + c!n1 = Some (Iload TRAP chunk addr rl rd nd) -> reg_map_ok map rd dst -> ~In rd pr -> tr_expr c map pr (Eload chunk addr al) ns nd rd dst | tr_Econdition: forall map pr a ifso ifnot ns nd rd ntrue nfalse dst, diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index 8336d1bf..6d27df28 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -104,11 +104,11 @@ Inductive wt_instr : instruction -> Prop := valid_successor s -> wt_instr (Iop op args res s) | wt_Iload: - forall chunk addr args dst s, + forall trap chunk addr args dst s, map env args = type_of_addressing addr -> env dst = type_of_chunk chunk -> valid_successor s -> - wt_instr (Iload chunk addr args dst s) + wt_instr (Iload trap chunk addr args dst s) | wt_Istore: forall chunk addr args src s, map env args = type_of_addressing addr -> @@ -282,7 +282,7 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv := else (let (targs, tres) := type_of_operation op in do e1 <- S.set_list e args targs; S.set e1 res tres) - | Iload chunk addr args dst s => + | Iload trap chunk addr args dst s => do x <- check_successor s; do e1 <- S.set_list e args (type_of_addressing addr); S.set e1 dst (type_of_chunk chunk) @@ -841,14 +841,14 @@ Proof. Qed. Lemma wt_exec_Iload: - forall env f chunk addr args dst s m a v rs, - wt_instr f env (Iload chunk addr args dst s) -> + forall env f trap chunk addr args dst s m a v rs, + wt_instr f env (Iload trap chunk addr args dst s) -> Mem.loadv chunk m a = Some v -> wt_regset env rs -> wt_regset env (rs#dst <- v). Proof. intros. destruct a; simpl in H0; try discriminate. inv H. - eapply wt_regset_assign; eauto. rewrite H8; eapply Mem.load_type; eauto. + eapply wt_regset_assign; eauto. rewrite H9; eapply Mem.load_type; eauto. Qed. Lemma wt_exec_Ibuiltin: diff --git a/backend/Renumber.v b/backend/Renumber.v index 10f58251..7ba16658 100644 --- a/backend/Renumber.v +++ b/backend/Renumber.v @@ -43,7 +43,7 @@ Definition renum_instr (i: instruction) : instruction := match i with | Inop s => Inop (renum_pc s) | Iop op args res s => Iop op args res (renum_pc s) - | Iload chunk addr args res s => Iload chunk addr args res (renum_pc s) + | Iload trap chunk addr args res s => Iload trap chunk addr args res (renum_pc s) | Istore chunk addr args src s => Istore chunk addr args src (renum_pc s) | Icall sg ros args res s => Icall sg ros args res (renum_pc s) | Itailcall sg ros args => i diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v index 7cda9425..2e161965 100644 --- a/backend/Renumberproof.v +++ b/backend/Renumberproof.v @@ -175,6 +175,18 @@ Proof. rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. eapply exec_Iload; eauto. constructor; auto. eapply reach_succ; eauto. simpl; auto. + (* load notrap1 *) + econstructor; split. + assert (eval_addressing tge sp addr rs ## args = None). + rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload_notrap1; eauto. + constructor; auto. eapply reach_succ; eauto. simpl; auto. + (* load notrap2 *) + econstructor; split. + assert (eval_addressing tge sp addr rs ## args = Some a). + rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload_notrap2; eauto. + constructor; auto. eapply reach_succ; eauto. simpl; auto. (* store *) econstructor; split. assert (eval_addressing tge sp addr rs ## args = Some a). diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 06e314f3..4a5e83a1 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -438,6 +438,19 @@ Proof. apply eval_addressing_preserved. exact symbols_preserved. eauto. econstructor; eauto. apply set_reg_lessdef; auto. + (* TODO *) +- (* load notrap1 *) + TransfInstr. + assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto. + + intros [a' [ADDR' ALD]]. + exploit Mem.loadv_extends; eauto. + intros [v' [LOAD' VLD]]. + left. exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- v') m'); split. + eapply exec_Iload with (a := a'). eauto. rewrite <- ADDR'. + apply eval_addressing_preserved. exact symbols_preserved. eauto. + econstructor; eauto. apply set_reg_lessdef; auto. + - (* store *) TransfInstr. assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto. diff --git a/backend/Unusedglob.v b/backend/Unusedglob.v index 8ac7c4ce..1b5f2547 100644 --- a/backend/Unusedglob.v +++ b/backend/Unusedglob.v @@ -46,7 +46,7 @@ Definition ref_instruction (i: instruction) : list ident := match i with | Inop _ => nil | Iop op _ _ _ => globals_operation op - | Iload _ addr _ _ _ => globals_addressing addr + | Iload _ _ addr _ _ _ => globals_addressing addr | Istore _ addr _ _ _ => globals_addressing addr | Icall _ (inl r) _ _ _ => nil | Icall _ (inr id) _ _ _ => id :: nil diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index 680daba7..fa120b6d 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -915,7 +915,7 @@ Proof. /\ Val.inject j a ta). { apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Ptrofs.zero) (vl1 := rs##args). intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto. - apply KEPT. red. exists pc, (Iload chunk addr args dst pc'); auto. + apply KEPT. red. exists pc, (Iload trap chunk addr args dst pc'); auto. econstructor; eauto. apply regs_inject; auto. assumption. } @@ -924,6 +924,36 @@ Proof. econstructor; split. eapply exec_Iload; eauto. econstructor; eauto. apply set_reg_inject; auto. +- (* load notrap1 *) + assert (eval_addressing tge (Vptr tsp Ptrofs.zero) addr trs##args = None). + { eapply eval_addressing_inj_none. + intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto. + apply KEPT. red. exists pc, (Iload NOTRAP chunk addr args dst pc'); auto. + econstructor; eauto. + rewrite Ptrofs.add_zero; reflexivity. + apply regs_inject; auto. + eassumption. + assumption. } + + econstructor; split. eapply exec_Iload_notrap1; eauto. + econstructor; eauto. apply set_reg_inject; auto. + +- (* load notrap2 *) + assert (A: exists ta, + eval_addressing tge (Vptr tsp Ptrofs.zero) addr trs##args = Some ta + /\ Val.inject j a ta). + { apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Ptrofs.zero) (vl1 := rs##args). + intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto. + apply KEPT. red. exists pc, (Iload NOTRAP chunk addr args dst pc'); auto. + econstructor; eauto. + apply regs_inject; auto. + assumption. } + destruct A as (ta & B & C). + destruct (Mem.loadv chunk tm ta) eqn:Echunk2. + + econstructor; split. eapply exec_Iload; eauto. + econstructor; eauto. apply set_reg_inject; auto. + + econstructor; split. eapply exec_Iload_notrap2; eauto. + econstructor; eauto. apply set_reg_inject; auto. - (* store *) assert (A: exists ta, eval_addressing tge (Vptr tsp Ptrofs.zero) addr trs##args = Some ta diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 1f80c293..605d7e90 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -121,7 +121,7 @@ Definition transfer (f: function) (rm: romem) (pc: node) (ae: aenv) (am: amem) : | Some(Iop op args res s) => let a := eval_static_operation op (aregs ae args) in VA.State (AE.set res a ae) am - | Some(Iload chunk addr args dst s) => + | Some(Iload trap chunk addr args dst s) => let a := loadv chunk rm am (eval_static_addressing addr (aregs ae args)) in VA.State (AE.set dst a ae) am | Some(Istore chunk addr args src s) => |