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
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
|
import Interp
import Interp_lib
open import Interp_ast
open import Interp_interface
open import Pervasives
val intern_value : value -> Interp.value
val extern_value : interp_mode -> bool -> Interp.value -> (value * maybe (list reg_name))
val extern_reg : Interp.reg_form -> maybe (integer * integer) -> reg_name
let build_context defs = match Interp.to_top_env defs with (_,context) -> context end
let make_mode eager_eval tracking_values = <| Interp.eager_eval = eager_eval; Interp.track_values = tracking_values |>;;
let tracking_dependencies mode = mode.Interp.track_values
let to_bits l = (List.map (fun b -> match b with
| false -> (Interp.V_lit (L_aux L_zero Interp_ast.Unknown))
| true -> (Interp.V_lit (L_aux L_one Interp_ast.Unknown)) end) l)
let from_bits l = (List.map (fun b -> match b with
| Interp.V_lit (L_aux L_zero _) -> false
| _ -> true end) l)
let rec to_bytes l = match (List.reverse l) with
| [] -> []
| (a::b::c::d::e::f::g::h::rest) ->
(natFromInteger(integerFromBoolList (false,[a;b;c;d;e;f;g;h])))::(to_bytes rest)
end
let intern_value v = match v with
| Bitvector bs inc fst -> Interp.V_vector fst inc (to_bits bs)
| Bytevector bys -> Interp.V_vector 0 true
(to_bits (List.reverse
(List.concat (List.map (fun n -> boolListFrombitSeq 8 (bitSeqFromInteger (Just 8) (integerFromNat n))) bys))))
| Unknown -> Interp.V_unknown
| _ -> Interp.V_unknown
end
let extern_reg r slice = match (r,slice) with
| (Interp.Reg (Id_aux (Id x) _) _,Nothing) -> Reg x
| (Interp.Reg (Id_aux (Id x) _) _,Just(i1,i2)) -> Reg_slice x (i1,i2)
| (Interp.SubReg (Id_aux (Id x) _) (Interp.Reg (Id_aux (Id y) _) _) (BF_aux(BF_single i) _),Nothing) -> Reg_field x y (i,i)
end
let extern_value mode for_mem v = match v with
| Interp.V_vector fst inc bits ->
if for_mem
then (Bytevector (List.reverse (to_bytes (from_bits bits))), Nothing)
else (Bitvector (from_bits bits) inc fst, Nothing)
| Interp.V_track (Interp.V_vector fst inc bits) regs ->
if for_mem
then (Bytevector (List.reverse (to_bytes (from_bits bits))),
if (mode.Interp.track_values)
then (Just (List.map (fun r -> extern_reg r Nothing) regs))
else Nothing)
else (Bitvector (from_bits bits) inc fst, Nothing)
| _ -> (Unknown,Nothing)
end
let initial_instruction_state top_level main args =
let e_args = match args with
| [] -> [E_aux (E_lit (L_aux L_unit Interp_ast.Unknown)) (Interp_ast.Unknown,Nothing)]
| [arg] -> let (e,_) = Interp.to_exp (make_mode true false) Interp.eenv (intern_value arg) in [e]
| args -> List.map fst (List.map (Interp.to_exp (make_mode true false) Interp.eenv)
(List.map intern_value args)) end in
Interp.Thunk_frame (E_aux (E_app (Id_aux (Id main) Interp_ast.Unknown) e_args) (Interp_ast.Unknown, Nothing))
top_level Interp.eenv Interp.emem Interp.Top
(*For now, append to this list to add more external functions; should add to the mode record for more perhaps *)
let external_functions =
Interp_lib.function_map
type mem_function = (string *
(maybe read_kind * maybe write_kind * (interp_mode -> Interp.value -> (value * (maybe (list reg_name))))))
(*List of memory functions; needs to be expanded with all of the memory functions needed for PPCMem.
Should probably be expanded into a parameter to mode as with above
*)
let memory_functions =
[ ("MEMr", (Just(Read_plain), Nothing,
(fun mode v -> match v with
| Interp.V_tuple [location;length] ->
match length with
| Interp.V_lit (L_aux (L_num len) _) ->
let (v,regs) = extern_value mode true location in
(v,len,regs) end end)));
("MEMw", (Nothing, Just(Write_plain),
(fun mode v -> match v with
| Interp.V_tuple [location;length] ->
match length with
| Interp.V_lit (L_aux (L_num len) _) ->
let (v,regs) = extern_value mode true location in
(v,len,regs) end end)));
]
let rec interp_to_value_helper thunk =
match thunk() with
| Interp.Value value -> (Just value,Nothing)
| Interp.Error l msg -> (Nothing, Just (Internal_error msg))
| Interp.Action (Interp.Call_extern i value) stack ->
match List.lookup i external_functions with
| Nothing -> (Nothing, Just (Internal_error ("External function not available " ^ i)))
| Just f ->
interp_to_value_helper (fun _ -> Interp.resume (make_mode true false) stack (Just (f value)))
end
| Interp.Action (Interp.Exit (E_aux e _)) _ ->
match e with
| E_id (Id_aux (Id "unsupported_instruction") _) -> (Nothing,Just (Unsupported_instruction_error ("",[],[])))
| E_id (Id_aux (Id "no_matching_pattern") _) -> (Nothing,Just Not_an_instruction_error)
end
| _ -> (Nothing, Just (Internal_error "Memory or register requested in decode"))
end
let decode_to_istate top_level value =
let mode = make_mode true false in
let (arg,_) = Interp.to_exp mode Interp.eenv (intern_value value) in
let (instr_decoded,error) = interp_to_value_helper
(fun _ -> Interp.resume
(make_mode true false)
(Interp.Thunk_frame
(E_aux (E_app (Id_aux (Id "decode") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown, Nothing))
top_level Interp.eenv Interp.emem Interp.Top) Nothing) in
match (instr_decoded,error) with
| (Just instr, _) ->
let (arg,_) = Interp.to_exp mode Interp.eenv instr in
let (instr_decoded,error) = interp_to_value_helper
(fun _ -> Interp.resume
(make_mode true false)
(Interp.Thunk_frame
(E_aux (E_app (Id_aux (Id "supported_instructions") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown, Nothing))
top_level Interp.eenv Interp.emem Interp.Top) Nothing) in
match (instr_decoded,error) with
| (Just instr,_) ->
let (arg,_) = Interp.to_exp mode Interp.eenv instr in
Instr (Interp.Thunk_frame
(E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown,Nothing))
top_level Interp.eenv Interp.emem Interp.Top)
("",[],[])
| (Nothing, Just err) -> err
end
| (Nothing, Just err) -> err
end
let rec interp_to_outcome mode thunk =
match thunk () with
| Interp.Value _ -> Done
| Interp.Error l msg -> Error msg (*Todo, add the l information the string format*)
| Interp.Action a next_state ->
match a with
| Interp.Read_reg reg_form slice ->
Read_reg (extern_reg reg_form slice)
(fun v ->
let v = (intern_value v) in
let v = if mode.Interp.track_values then (Interp.V_track v [reg_form]) else v in
Interp.add_answer_to_stack next_state v)
| Interp.Write_reg reg_form slice value ->
let (v,_) = extern_value mode false value in Write_reg (extern_reg reg_form slice) v next_state
| Interp.Read_mem (Id_aux (Id i) _) value slice ->
match List.lookup i memory_functions with
| (Just (Just read_k,_,f)) ->
let (location, length, tracking) = (f mode value) in
Read_mem read_k location tracking length Nothing (fun v -> Interp.add_answer_to_stack next_state (intern_value v))
| _ -> Error ("Memory " ^ i ^ " function with read kind not found")
end
| Interp.Write_mem (Id_aux (Id i) _) loc_val slice write_val ->
match List.lookup i memory_functions with
| (Just (_,Just write_k,f)) ->
let (location, length, tracking) = (f mode loc_val) in
let (value, val_tracking) = (extern_value mode true write_val) in
Write_mem write_k location tracking length Nothing value val_tracking (fun b -> next_state)
| _ -> Error ("Memory " ^ i ^ " function with write kind not found")
end
| Interp.Barrier (Id_aux (Id i) _) lval ->
Barrier Sync next_state (* TODO set up some barrier functions and see if the value would be anything needed *)
| Interp.Nondet exps ->
let nondet_states = List.map (Interp.set_in_context next_state) exps in
Nondet_choice nondet_states next_state
| Interp.Call_extern i value ->
match List.lookup i external_functions with
| Nothing -> Error ("External function not available " ^ i)
| Just f ->
if (mode.Interp.eager_eval)
then interp_to_outcome mode (fun _ -> Interp.resume mode next_state (Just (f value)))
else let new_v = f value in
Internal (Just i)
(Just (fun _ -> Interp.string_of_value value))
(Interp.add_answer_to_stack next_state new_v)
end
| Interp.Step l Nothing Nothing -> Internal Nothing Nothing next_state
| Interp.Step l (Just name) Nothing -> Internal (Just name) Nothing next_state
| Interp.Step l (Just name) (Just value) ->
Internal (Just name) (Just (fun _ -> Interp.string_of_value value)) next_state
end
end
let interp mode i_state = interp_to_outcome mode (fun _ -> Interp.resume mode i_state Nothing)
let rec ie_loop mode i_state =
match (interp mode i_state) with
| Done -> []
| Error msg -> [E_error msg]
| Read_reg reg i_state_fun ->
(E_read_reg reg)::(ie_loop mode (i_state_fun Unknown))
| Write_reg reg value i_state->
(E_write_reg reg value)::(ie_loop mode i_state)
| Read_mem read_k loc tracking length ltracking i_state_fun ->
(E_read_mem read_k loc tracking length ltracking)::(ie_loop mode (i_state_fun Unknown))
| Write_mem write_k loc track length l_track value v_track i_state_fun ->
(E_write_mem write_k loc track length l_track value v_track)::(ie_loop mode (i_state_fun true))
| Internal _ _ next -> (ie_loop mode next)
end ;;
let interp_exhaustive i_state =
let mode = make_mode true false in
ie_loop mode i_state
let rec rr_ie_loop mode i_state =
match (interp mode i_state) with
| Done -> ([],Done)
| Error msg -> ([E_error msg], Error msg)
| Read_reg reg i_state_fun -> ([], Read_reg reg i_state_fun)
| Write_reg reg value i_state->
let (events,outcome) = (rr_ie_loop mode i_state) in
(((E_write_reg reg value)::events), outcome)
| Read_mem read_k loc tracking length ltracking i_state_fun ->
let (events,outcome) = (rr_ie_loop mode (i_state_fun Unknown)) in
(((E_read_mem read_k loc tracking length ltracking)::events),outcome)
| Write_mem write_k loc track length l_track value v_track i_state_fun ->
let (events,outcome) = (rr_ie_loop mode (i_state_fun true)) in
(((E_write_mem write_k loc track length l_track value v_track)::events),outcome)
| Internal _ _ next -> (rr_ie_loop mode next)
end ;;
let rr_interp_exhaustive mode i_state events =
let (events',outcome) = rr_ie_loop mode i_state in ((events ++ events'),outcome)
|
