diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-05 11:19:22 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-05 11:19:22 +0200 |
| commit | c4cc75dc6abcb0eee6f3288e96fea4aec540fd68 (patch) | |
| tree | e63d0437c3f3cb43eb26cced8ad94acc62e82dad /backend/LTL.v | |
| parent | 7042070a3668ae149ec6a490b8e7c1a6aa82d6fe (diff) | |
| download | compcert-kvx-c4cc75dc6abcb0eee6f3288e96fea4aec540fd68.tar.gz compcert-kvx-c4cc75dc6abcb0eee6f3288e96fea4aec540fd68.zip | |
more proofs going through
Diffstat (limited to 'backend/LTL.v')
| -rw-r--r-- | backend/LTL.v | 19 |
1 files changed, 16 insertions, 3 deletions
diff --git a/backend/LTL.v b/backend/LTL.v index 5e7eec8c..ee8b4826 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -29,7 +29,7 @@ Definition node := positive. Inductive instruction: Type := | Lop (op: operation) (args: list mreg) (res: mreg) - | Lload (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dst: mreg) + | Lload (trap : trapping_mode) (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dst: mreg) | Lgetstack (sl: slot) (ofs: Z) (ty: typ) (dst: mreg) | Lsetstack (src: mreg) (sl: slot) (ofs: Z) (ty: typ) | Lstore (chunk: memory_chunk) (addr: addressing) (args: list mreg) (src: mreg) @@ -209,11 +209,24 @@ Inductive step: state -> trace -> state -> Prop := rs' = Locmap.set (R res) v (undef_regs (destroyed_by_op op) rs) -> step (Block s f sp (Lop op args res :: bb) rs m) E0 (Block s f sp bb rs' m) - | exec_Lload: forall s f sp chunk addr args dst bb rs m a v rs', + | exec_Lload: forall s f sp trap chunk addr args dst bb rs m a v rs', eval_addressing ge sp addr (reglist rs args) = Some a -> Mem.loadv chunk m a = Some v -> rs' = Locmap.set (R dst) v (undef_regs (destroyed_by_load chunk addr) rs) -> - step (Block s f sp (Lload chunk addr args dst :: bb) rs m) + step (Block s f sp (Lload trap chunk addr args dst :: bb) rs m) + E0 (Block s f sp bb rs' m) + | exec_Lload_notrap1: forall s f sp chunk addr args dst bb rs m rs', + eval_addressing ge sp addr (reglist rs args) = None -> + rs' = Locmap.set (R dst) (default_notrap_load_value chunk) + (undef_regs (destroyed_by_load chunk addr) rs) -> + step (Block s f sp (Lload NOTRAP chunk addr args dst :: bb) rs m) + E0 (Block s f sp bb rs' m) + | exec_Lload_notrap2: forall s f sp chunk addr args dst bb rs m a rs', + eval_addressing ge sp addr (reglist rs args) = Some a -> + Mem.loadv chunk m a = None -> + rs' = Locmap.set (R dst) (default_notrap_load_value chunk) + (undef_regs (destroyed_by_load chunk addr) rs) -> + step (Block s f sp (Lload NOTRAP chunk addr args dst :: bb) rs m) E0 (Block s f sp bb rs' m) | exec_Lgetstack: forall s f sp sl ofs ty dst bb rs m rs', rs' = Locmap.set (R dst) (rs (S sl ofs ty)) (undef_regs (destroyed_by_getstack sl) rs) -> |