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
134
135
136
137
138
139
140
141
142
143
open Types
module Raw (State : RAW_STATE) = struct
let uop e (o : Dba.Unary_op.t) : Term.unary Term.operator =
match o with
| Not -> Not
| UMinus -> Minus
| Sext n -> Sext (n - Dba.Expr.size_of e)
| Uext n -> Uext (n - Dba.Expr.size_of e)
| Restrict interval -> Restrict interval
let bop (op : Dba.Binary_op.t) : Term.binary Term.operator =
match op with
| Plus -> Plus
| Minus -> Minus
| Mult -> Mul
| DivU -> Udiv
| DivS -> Sdiv
| ModU -> Umod
| ModS -> Smod
| Eq -> Eq
| Diff -> Diff
| LeqU -> Ule
| LtU -> Ult
| GeqU -> Uge
| GtU -> Ugt
| LeqS -> Sle
| LtS -> Slt
| GeqS -> Sge
| GtS -> Sgt
| Xor -> Xor
| And -> And
| Or -> Or
| Concat -> Concat
| LShift -> Lsl
| RShiftU -> Lsr
| RShiftS -> Asr
| LeftRotate -> Rol
| RightRotate -> Ror
let rec eval (e : Types.Expr.t) state =
match e with
| Cst bv | Var { info = Symbol (_, (lazy bv)); _ } ->
State.Value.constant bv
| Var var -> State.lookup var state
| Load (len, dir, addr, None) ->
fst (State.read ~addr:(eval addr state) len dir state)
| Load (len, dir, addr, Some name) ->
fst (State.select name ~addr:(eval addr state) len dir state)
| Unary (f, x) -> State.Value.unary (uop x f) (eval x state)
| Binary (f, x, y) ->
State.Value.binary (bop f) (eval x state) (eval y state)
| Ite (c, r, e) ->
State.Value.ite (eval c state) (eval r state) (eval e state)
end
module Make (Path : Path.S) (State : STATE) = struct
include Raw (State)
let fresh (var : Dba.Var.t) state path =
let id = Path.get State.id path in
Path.set State.id (State.Uid.succ id) path;
let value = State.Value.var id var.name var.size in
let symbols = Path.get State.symbols path in
let stream = try S.Map.find var.name symbols with Not_found -> [] in
Path.set State.symbols (S.Map.add var.name (value :: stream) symbols) path;
State.assign var value state
let rec safe_eval e state path =
try (eval e state, state) with
| Undef var -> safe_eval e (fresh var state path) path
| Uninterp array -> safe_eval e (State.alloc ~array state) path
let rec get_value e state path =
try State.get_value (eval e state) state with
| Undef var -> get_value e (fresh var state path) path
| Uninterp array -> get_value e (State.alloc ~array state) path
let rec assume e state path =
try State.assume (eval e state) state with
| Undef var -> assume e (fresh var state path) path
| Uninterp array -> assume e (State.alloc ~array state) path
let rec test e state path =
try State.test (eval e state) state with
| Undef var -> test e (fresh var state path) path
| Uninterp array -> test e (State.alloc ~array state) path
let rec split_on e ?n ?except state path =
try State.enumerate (eval e state) ?n ?except state with
| Undef var -> split_on e ?n ?except (fresh var state path) path
| Uninterp array -> split_on e ?n ?except (State.alloc ~array state) path
let rec assign name e state path =
try State.assign name (eval e state) state with
| Undef var -> assign name e (fresh var state path) path
| Uninterp array -> assign name e (State.alloc ~array state) path
let rec read ~addr bytes dir state path =
try State.read ~addr:(eval addr state) bytes dir state with
| Undef var -> read ~addr bytes dir (fresh var state path) path
| Uninterp array -> read ~addr bytes dir (State.alloc ~array state) path
let rec write ~addr value dir state path =
try State.write ~addr:(eval addr state) (eval value state) dir state with
| Undef var -> write ~addr value dir (fresh var state path) path
| Uninterp array -> write ~addr value dir (State.alloc ~array state) path
let rec select name ~addr bytes dir state path =
try State.select name ~addr:(eval addr state) bytes dir state with
| Undef var -> select name ~addr bytes dir (fresh var state path) path
| Uninterp array ->
select name ~addr bytes dir (State.alloc ~array state) path
let rec store name ~addr value dir state path =
try
State.store name ~addr:(eval addr state) (eval value state) dir state
with
| Undef var -> store name ~addr value dir (fresh var state path) path
| Uninterp array ->
store name ~addr value dir (State.alloc ~array state) path
end