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
|
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 = Interp.to_top_env defs
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 l with
| [] -> []
| (a::b::c::d::e::f::g::h::rest) ->
(natFromInteger(integerFromBoolList (true,[a;b;c;d;e;f;g;h])))::(to_bytes rest)
end
let intern_value v = match v with
| Bitvector bs -> Interp.V_vector 0 true (to_bits bs)
| Bytevector bys -> Interp.V_vector 0 true (to_bits (List.concat (List.map (fun n -> boolListFrombitSeq 8 (bitSeqFromInteger (Just 8) (integerFromNat n))) bys)))
| 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 _ true bits ->
if for_mem
then (Bytevector (to_bytes (from_bits bits)), Nothing)
else (Bitvector (from_bits bits), Nothing)
| Interp.V_track (Interp.V_vector _ true bits) regs ->
if for_mem
then (Bytevector (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), Nothing)
| _ -> (Unknown,Nothing)
end
let initial_instruction_state top_level main arg =
let (e_arg,env) = Interp.to_exp <| Interp.eager_eval = true; Interp.track_values = false |> Interp.eenv (intern_value arg) in
Interp.Thunk_frame (E_aux (E_app (Id_aux (Id main) Interp_ast.Unknown) [e_arg]) (Interp_ast.Unknown, Nothing)) top_level Interp.eenv Interp.emem
(*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 =
[ ("MEM", (Just(Interp.Read_plain), Just(Interp.Write_plain), (fun mode v -> extern_value mode true v)));
]
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, tracking) = (f mode value) in
Read_mem read_k location tracking (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, tracking) = (f mode loc_val) in
let (value, val_tracking) = (extern_value mode true write_val) in
Write_mem write_k location tracking 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 Interp.Plain 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 -> interp_to_outcome mode (fun _ -> Interp.resume mode next_state (Just (f value))) end
| Interp.Step l _ _ -> Internal (fun _ -> "Function state to string not implemented yet") 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 i_state_fun ->
(E_read_mem read_k loc tracking)::(ie_loop mode (i_state_fun Unknown))
| Write_mem write_k loc l_track value v_track i_state_fun ->
(E_write_mem write_k loc 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 = <| Interp.eager_eval = true; Interp.track_values = false; |> in
ie_loop mode i_state
|
