blob: b6261d1c62cf6cc36e32bbb59e113a55201bdd5e (
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
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
|
Require Export QhasmCommon QhasmUtil State.
Require Export ZArith Sumbool.
Require Export Bedrock.Word.
Import State.
Import Util.
Definition evalTest {n} (o: TestOp) (a b: word n): bool :=
let c := (N.compare (wordToN a) (wordToN b)) in
let eqBit := match c with | Eq => true | _ => false end in
let ltBit := match c with | Lt => true | _ => false end in
let gtBit := match c with | Gt => true | _ => false end in
match o with
| TEq => eqBit
| TLt => ltBit
| TLe => orb (eqBit) (ltBit)
| TGt => gtBit
| TGe => orb (eqBit) (gtBit)
end.
Definition evalCond (c: Conditional) (state: State): option bool :=
match c with
| TestTrue => Some true
| TestFalse => Some false
| TestInt n t a b =>
match (getIntReg a state) with
| Some va =>
match (getIntReg b state) with
| Some vb => Some (evalTest t va vb)
| _ => None
end
| _ => None
end
end.
Definition evalIOp {b} (io: IntOp) (x y: word b) :=
match io with
| IPlus => wplus x y
| IMinus => wminus x y
| IXor => wxor x y
| IAnd => wand x y
| IOr => wor x y
end.
Definition evalRotOp {b} (ro: RotOp) (x: word b) (n: nat) :=
match ro with
| Shl => NToWord b (N.shiftl_nat (wordToN x) n)
| Shr => NToWord b (N.shiftr_nat (wordToN x) n)
end.
Definition evalDualOp {b} (duo: DualOp) (x y: word b) :=
match duo with
| IMult =>
let wres := natToWord (b + b) (N.to_nat ((wordToN x) * (wordToN y))) in
(split1 b b wres, split2 b b wres)
end.
Definition evalOperation (o: Operation) (state: State): option State :=
let liftOpt := fun {A B C} (f: A -> B -> option C) (xo: option A) (yo: option B) =>
match (xo, yo) with
| (Some x, Some y) => f x y
| _ => None
end in
match o with
| IOpConst n o r c =>
liftOpt (fun x y => setIntReg r (evalIOp o x y) state)
(getIntReg r state)
(match c with | constInt32 v => Some v | constInt64 v => Some v end)
| IOpReg n o a b =>
liftOpt (fun x y => setIntReg a (evalIOp o x y) state)
(getIntReg a state) (getIntReg b state)
| DOpReg n o a b h =>
liftOpt (fun x y =>
match (evalDualOp o x y) with
| (lw, hw) =>
match (setIntReg a lw state) with
| Some st' =>
match h with
| Some hr => setIntReg hr hw st'
| _ => Some st'
end
| None => None
end
end)
(getIntReg a state) (getIntReg b state)
| OpRot n o r i =>
match (getIntReg r state) with
| Some va => setIntReg r (evalRotOp o va i) state
| None => None
end
end.
Definition getIConst {n} (c: IConst n): word n :=
match c with
| constInt32 v => v
| constInt64 v => v
end.
Definition evalAssignment (a: Assignment) (state: State): option State :=
let liftOpt := fun {A B} (f: A -> option B) (xo: option A) =>
match xo with
| (Some x') => f x'
| _ => None
end in
match a with
| ARegStackInt n r s =>
liftOpt (fun x => setIntReg r x state) (getStack s state)
| AStackRegInt n s r =>
liftOpt (fun x => setStack s x state) (getIntReg r state)
| ARegRegInt n a b =>
liftOpt (fun x => setIntReg a x state) (getIntReg b state)
| AConstInt n r c => setIntReg r (getIConst c) state
| AIndex n m a b i =>
match (getStack b state) with
| Some v => setIntReg a (trunc n (getIndex v m i)) state
| _ => None
end
| APtr n r s =>
setIntReg r (NToWord 32 (N.of_nat (getStackIndex s))) state
end.
|
