blob: 0767ea79037d9673b3f5ea43bb9f2b65ca8cf3eb (
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
|
import Interp
type read_kind = Interp.read_kind
type write_kind = Interp.write_kind
type barrier_kind = Interp.barrier_kind
type value =
| Bitvector of list nat (*Always 0 or 1; should this be a Word.bitSequence? *)
| Bytevector of list (list nat) (* Should this be a list of Word.bitSequence? *)
| Unknown
type instruction_state = Interp.stack
type context = Interp.top_level
type reg_name = Interp.reg_form (*for now...*)
type outcome =
| Read_mem of read_kind * value * (value -> instruction_state)
| Write_mem of write_kind * value * value * (bool -> instruction_state)
| Barrier of barrier_kind * instruction_state
| Read_reg of reg_name * (value -> instruction_state) (*What about slicing?*)
| Write_reg of reg_name * value * instruction_state
| Nondet_choice of list instruction_state
| Internal of instruction_state
| Done
| Error of string
val build_context : Interp.defs Interp.tannot -> context
val initial_instruction_state : context -> string -> value -> instruction_state
type interp_mode = <| eager_eval : bool |>
val interp : instruction_state -> interp_mode -> outcome
val interp_exhaustive : instruction_state -> list outcome (*not sure what event was ment to be*)
val intern_value : value -> Interp.value
val extern_value : Interp.value -> value
let build_context defs = Interp.to_top_env defs
let intern_value v = match v with
| Bitvector bs -> Interp.V_vector 0 true (List.map (fun | 0 -> (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_zero Interp_ast.Unknown))
| _ -> (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_one Interp_ast.Unknown))) bs)
| Unknown -> Interp.V_unknown
let extern_value v = match v with
| Interp.V_vector _ true bits -> Bitvector (List.map (fun | Interp.V_lit (Interp_ast.L_aux Interp_ast.L_zero _) -> 0
| _ -> 1) bits)
| _ -> Unknown
let initial_instruction_state top_level main arg =
Interp.Frame Nothing (E_aux (E_app (Id_aux (Id main) Interp_ast.Unknown) [ intern_value arg ]) (Interp_ast.Unknown, Nothing)) top_level [] Interp.emem
|
