-
Notifications
You must be signed in to change notification settings - Fork 0
/
RelationExtraction.v
97 lines (88 loc) · 3.47 KB
/
RelationExtraction.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
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
Require Import ZArith List.
Require Export Labels.
Require Export Instructions.
Require Import Rules.
Context{T : Type}.
Context{Latt : JoinSemiLattice T}.
Definition none := bot.
Record MVec := MkMVec {
mop : OpCode;
ml1 : T;
ml2 : T;
ml3 : T;
mpc : T
}.
Record RVec := MkRVec {
rlab : T;
rpc : T
}.
Inductive table : MVec -> RVec -> Prop :=
| TLab : forall pc l1 l2 l3,
table (MkMVec OpLab l1 l2 l3 pc) (MkRVec bot pc)
| TMLab : forall pc l1 l2 l3,
table (MkMVec OpMLab l1 l2 l3 pc) (MkRVec l1 pc)
| TPcLab : forall pc l1 l2 l3,
table (MkMVec OpPcLab l1 l2 l3 pc) (MkRVec bot pc)
| TBCall : forall pc l1 l2 l3,
table (MkMVec OpBCall l1 l2 l3 pc) (MkRVec (join l2 pc) (join l1 pc))
| TBRet : forall pc l1 l2 l3,
flows (join l1 pc) (join l2 l3) = true ->
table (MkMVec OpBRet l1 l2 l3 pc) (MkRVec l2 l3)
| TPutBot : forall pc l1 l2 l3,
table (MkMVec OpPutLab l1 l2 l3 pc) (MkRVec bot pc)
| TNop : forall pc l1 l2 l3,
table (MkMVec OpNop l1 l2 l3 pc) (MkRVec none pc)
| TPut : forall pc l1 l2 l3,
table (MkMVec OpPut l1 l2 l3 pc) (MkRVec bot pc)
| TBinOp : forall pc l1 l2 l3,
table (MkMVec OpBinOp l1 l2 l3 pc) (MkRVec (join l1 l2) pc)
| TJump : forall pc l1 l2 l3,
table (MkMVec OpJump l1 l2 l3 pc) (MkRVec none (join pc l1))
| TBNZ : forall pc l1 l2 l3,
table (MkMVec OpBNZ l1 l2 l3 pc) (MkRVec none (join pc l1))
| TLoad : forall pc l1 l2 l3,
table (MkMVec OpLoad l1 l2 l3 pc) (MkRVec l3 (join pc (join l1 l2)))
| TStore : forall pc l1 l2 l3,
flows (join l1 pc) l2 = true ->
table (MkMVec OpStore l1 l2 l3 pc) (MkRVec l3 pc)
| TAlloc : forall pc l1 l2 l3,
table (MkMVec OpAlloc l1 l2 l3 pc) (MkRVec (join l1 l2) pc)
| TPSetOff : forall pc l1 l2 l3,
table (MkMVec OpPSetOff l1 l2 l3 pc) (MkRVec (join l1 l2) pc)
| TPGetOff : forall pc l1 l2 l3,
table (MkMVec OpPGetOff l1 l2 l3 pc) (MkRVec l1 pc)
| TMSize : forall pc l1 l2 l3,
table (MkMVec OpMSize l1 l2 l3 pc) (MkRVec l2 (join pc l1)).
Declare ML Module "relation_extraction_plugin".
Extraction Relation table [1].
(* This produces:
let rec table1 p1 =
match p1 with
| MkMVec (OpLab, l1, l2, l3, pc) -> MkRVec (bot, pc)
| MkMVec (OpMLab, l1, l2, l3, pc) -> MkRVec (l1, pc)
| MkMVec (OpPcLab, l1, l2, l3, pc) -> MkRVec (bot, pc)
| MkMVec (OpBCall, l1, l2, l3, pc) -> MkRVec ((join l2 pc), (join l1 pc))
| MkMVec (OpBRet, l1, l2, l3, pc) ->
(match flows (join l1 pc) (join l2 l3) with
| true -> MkRVec (l2, l3)
| _ -> assert false (* *))
| MkMVec (OpFlowsTo, l1, l2, l3, pc) -> MkRVec ((join l1 l2), pc)
| MkMVec (OpLJoin, l1, l2, l3, pc) -> MkRVec ((join l1 l2), pc)
| MkMVec (OpPutBot, l1, l2, l3, pc) -> MkRVec (bot, pc)
| MkMVec (OpNop, l1, l2, l3, pc) -> MkRVec (none, pc)
| MkMVec (OpPut, l1, l2, l3, pc) -> MkRVec (bot, pc)
| MkMVec (OpBinOp, l1, l2, l3, pc) -> MkRVec ((join l1 l2), pc)
| MkMVec (OpJump, l1, l2, l3, pc) -> MkRVec (none, (join pc l1))
| MkMVec (OpBNZ, l1, l2, l3, pc) -> MkRVec (none, (join pc l1))
| MkMVec (OpLoad, l1, l2, l3, pc) -> MkRVec (l3, (join pc (join l1 l2)))
| MkMVec (OpStore, l1, l2, l3, pc) ->
(match flows (join l1 pc) l2 with
| true -> MkRVec (l3, pc)
| _ -> assert false (* *))
| MkMVec (OpAlloc, l1, l2, l3, pc) -> MkRVec ((join l1 l2), pc)
| MkMVec (OpPSetOff, l1, l2, l3, pc) -> MkRVec ((join l1 l2), pc)
| MkMVec (OpPGetOff, l1, l2, l3, pc) -> MkRVec (l1, pc)
| MkMVec (OpMSize, l1, l2, l3, pc) -> MkRVec (l2, (join pc l1))
| MkMVec (OpOutput, l1, l2, l3, pc) -> MkRVec ((join l1 pc), pc)
| _ -> assert false (* *)
*)