-
Notifications
You must be signed in to change notification settings - Fork 1
/
OpsemAux.v
77 lines (66 loc) · 2.11 KB
/
OpsemAux.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
Require Import syntax.
Require Import alist.
Require Import FMapWeakList.
Require Import Classical.
Require Import Coqlib.
Require Import infrastructure.
Require Import Metatheory.
Import LLVMsyntax.
Import LLVMinfra.
Require Import opsem.
Require Import sflib.
Require Import paco.
Import Opsem.
Require Import TODO.
Require Import Decs.
Require Import Hints.
Require Import Validator.
Require Import GenericValues.
Require Import Inject.
Set Implicit Arguments.
Lemma sInsn_non_call
conf fdef bb cmd cmds term locals1 allocas1 ecs mem1
st2 event
(NONCALL: ~ Instruction.isCallInst cmd)
(STEP: sInsn
conf
(mkState (mkEC fdef bb (cmd::cmds) term locals1 allocas1) ecs mem1)
st2
event):
exists locals2 allocas2 mem2,
st2 = mkState (mkEC fdef bb cmds term locals2 allocas2) ecs mem2.
Proof.
inv STEP; eauto. ss. congruence.
Qed.
Lemma inject_decide_nonzero
TD inv
val_src decision_src
val_tgt decision_tgt
(INJECT: genericvalues_inject.gv_inject inv val_src val_tgt)
(SRC: decide_nonzero TD val_src decision_src)
(TGT: decide_nonzero TD val_tgt decision_tgt):
decision_src = decision_tgt.
Proof.
inv SRC. inv TGT. unfold GV2int in *. des_ifs.
inv INJECT. ss. inv H1.
apply inj_pair2 in H2. apply inj_pair2 in H. clarify.
Qed.
Coercion module_of_conf (conf: Config): module.
Proof.
destruct conf.
destruct CurTargetData0.
econs; eauto.
Defined.
Coercion get_cmds_from_stmts (s: stmts): cmds :=
let '(stmts_intro _ cs _) := s in cs
.
Coercion get_cmds_from_block (b: block): cmds := b.(snd).
Inductive wf_EC (ec: ExecutionContext): Prop :=
| wf_EC_intro
(BLOCK: blockInFdefB ec.(CurBB) ec.(CurFunction))
(* (CMDS: forall c (IN: In c ec.(CurCmds)), insnInBlockB (insn_cmd c) ec.(CurBB)) *)
(* Instead of above definition, I intentionally choose below definition. It was easier. *)
(* FYI: wf_fdef lemmas, such as "typings_props.wf_fdef__wf_cmd", doesn't use insnInBlockB *)
(CMDS: sublist ec.(CurCmds) (ec.(CurBB): cmds))
(TERM: insnInBlockB (insn_terminator ec.(Terminator)) ec.(CurBB))
.