blob: f30d10e947f372053f71ed3db6e1514c836a62e5 (
plain)
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
98
99
100
101
102
|
Require Import String.
Inductive Const32 : Set = | const32: word 32 -> Const32.
Inductive Reg (len: nat) : Set =
| reg32: string -> Reg 32
| reg3232: string -> Reg 64
| reg6464: string -> Reg 128
| float80: string -> Reg 80.
Inductive Stack (len: nat) : Set =
| stack32: string -> Stack 32.
| stack64: string -> Stack 64.
| stack128: string -> Stack 128.
Definition Index (limit: nat) := {x: nat | x < limit}.
Inductive Assignment : Set :=
| Assign32Stack32: Reg 32 -> Stack32 -> Assignment
| Assign32Stack16: Reg 32 -> Stack32 -> Index 2 -> Assignment
| Assign32Stack8: Reg 32 -> Stack32 -> Index 4 -> Assignment
| Assign32Stack64: Reg 32 -> Stack64 -> Index 2 -> Assignment
| Assign32Stack128: Reg 32 -> Stack128 -> Index 2 -> Assignment
| Assign32Reg32: Reg 32 -> Reg 32 -> Assignment
| Assign32Reg16: Reg 32 -> Reg 32 -> Index 2 -> Assignment
| Assign32Reg8: Reg 32 -> Reg 32 -> Index 4 -> Assignment
| Assign32Reg64: Reg 32 -> Reg64 -> Index 2 -> Assignment
| Assign32Reg128: Reg 32 -> Reg 128 -> Index 4 -> Assignment
| Assign3232Stack32: Reg 64 -> Index 2 -> Stack32 -> Assignment
| Assign3232Stack64: Reg 64 -> Stack64 -> Assignment
| Assign3232Stack128: Reg 64 -> Stack128 -> Index 2 -> Assignment
| Assign3232Reg32: Reg 64 -> Index 2 -> Reg 32 -> Assignment
| Assign3232Reg64: Reg 64 -> Reg64 -> Assignment
| Assign3232Reg128: Reg 64 -> Reg 128 -> M 2 -> Assignment
| AssignConstant: Reg 32 -> Const32 -> Assignment
| AssignPtr: Reg 32 -> Stack64.
Hint Constructors Assignment.
Inductive BinOp :=
| Plus: BinOp | Minus: BinOp | Mult: BinOp
| Div: BinOp | Xor: BinOp | And: BinOp.
Inductive RotOp :=
| Shl: NatOp | Shr: NatOp | Rotl: NatOp | Rotr: NatOp.
Inductive Operation :=
| OpReg32Constant: BinOp -> Reg 32 -> Const32 -> Operation
| OpReg32Reg32: BinOp -> Reg 32 -> Reg 32 -> Operation
| RotReg32: RotOp -> Reg 32 -> Index 32 -> Operation
| OpReg64Constant: BinOp -> Reg 32 -> Const32 -> Operation
| OpReg64Reg64: BinOp -> Reg 64 -> Reg 64 -> Operation
| OpReg128Constant: BinOp -> Reg 128 -> Const32 -> Operation
| OpReg128Reg128: BinOp -> Reg 128 -> Reg 128 -> Operation.
Hint Constructors Operation.
Inductive TestOp :=
| Eq: TestOp
| Lt: TestOp
| UnsignedLt: TestOp
| Gt: TestOp
| UnsignedGt: TestOp.
Definition Invert := bool.
Definition Conditional :=
| TestReg32Reg32: TestOp -> Invert -> Reg 32 -> Reg 32 -> Conditional
| TestReg32Const: TestOp -> Invert -> Reg 32 -> W -> Conditional.
Hint Constructors Conditional.
Definition Label := nat.
Inductive AlmostQhasm :=
| QSeq: AlmostQhasm -> AlmostQhasm -> AlmostQhasm
| QAssign: Assignment -> AlmostQhasm
| QOp: Operation -> AlmostQhasm
| QCond: Conditional -> AlmostQhasm -> AlmostQhasm -> AlmostQhasm
| QWhile: Conditional -> AlmostQhasm -> AlmostQhasm
Hint Constructors AlmostQhasm.
Inductive Qhasm :=
| QSeq: Qhasm -> Qhasm -> Qhasm
| QAssign: Assignment -> Qhasm
| QOp: Operation -> Qhasm
| QCond: Conditional -> Qhasm -> Qhasm -> Qhasm
| QWhile: Conditional -> Qhasm -> Qhasm
Hint Constructors Qhasm.
(* evalReg: Qhasm -> Reg 32 -> Reg 32
evalStack: Qhasm -> Stack32 -> Stack32 *)
|
