diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-31 11:49:21 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-31 11:49:21 +0200 |
| commit | 7de591569308917c9ffcd4626c94872e390811a2 (patch) | |
| tree | 0c9f226d5d82e52fff7d2c3b1f655962e6f93a7e | |
| parent | 764b167efe9edb3d0d20e8ea37263320c42f3036 (diff) | |
| download | compcert-kvx-7de591569308917c9ffcd4626c94872e390811a2.tar.gz compcert-kvx-7de591569308917c9ffcd4626c94872e390811a2.zip | |
INJnop
| -rw-r--r-- | backend/Inject.v | 3 | ||||
| -rw-r--r-- | backend/Injectproof.v | 6 |
2 files changed, 8 insertions, 1 deletions
diff --git a/backend/Inject.v b/backend/Inject.v index 6ef32ccb..57aa343b 100644 --- a/backend/Inject.v +++ b/backend/Inject.v @@ -5,11 +5,13 @@ Require Import Memory Registers Op RTL. Local Open Scope positive. Inductive inj_instr : Type := + | INJnop | INJop: operation -> list reg -> reg -> inj_instr | INJload: memory_chunk -> addressing -> list reg -> reg -> inj_instr. Definition inject_instr (i : inj_instr) (pc' : node) : instruction := match i with + | INJnop => Inop pc' | INJop op args dst => Iop op args dst pc' | INJload chunk addr args dst => Iload NOTRAP chunk addr args dst pc' end. @@ -83,6 +85,7 @@ Section INJECTOR. Definition valid_injection_instr (max_reg : reg) (i : inj_instr) := match i with + | INJnop => true | INJop op args res => (max_reg <? res) && (negb (is_trapping_op op) && (Datatypes.length args =? args_of_operation op)%nat) | INJload _ _ _ res => max_reg <? res diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 51d049b1..7ce401cb 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -742,7 +742,11 @@ Section INJECTOR. (State ts tf sp (Pos.succ pc) trs' m) /\ match_regs (f : function) trs trs'. Proof. - destruct ii as [op args res | chunk addr args res]; simpl; intros. + destruct ii as [ |op args res | chunk addr args res]; simpl; intros. + - exists trs. + split. + * apply exec_Inop; assumption. + * apply match_regs_refl. - repeat rewrite andb_true_iff in VALID. rewrite negb_true_iff in VALID. destruct VALID as (MAX_REG & NOTRAP & LENGTH). |