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
|
open import Interp_ast
open import Interp_utilities
open import Pervasives
type instr_parm_typ =
| IBit
| IBitvector of maybe nat
| IRange of maybe nat
| IEnum of string * nat
| IOther
type instruction_form =
| Instr_form of string * list (string * instr_parm_typ) * list base_effect
| Skipped
val extract_instructions : string -> defs tannot -> list instruction_form
let rec extract_ityp t tag = match (t,tag) with
| (T_abbrev _ t,_) -> extract_ityp t tag
| (T_id "bit",_) -> IBit
| (T_id "bool",_) -> IBit
| (T_app "vector" (T_args [_; T_arg_nexp (Ne_const len); _; T_arg_typ (T_id "bit")]),_) ->
IBitvector (Just (natFromInteger len))
| (T_app "vector" (T_args [_;_;_;T_arg_typ (T_id "bit")]),_) -> IBitvector (Just 64)
| (T_app "atom" (T_args [T_arg_nexp (Ne_const num)]),_) ->
IRange (Just (natFromInteger num))
| (T_app "atom" _,_) -> IRange Nothing
| (T_app "range" (T_args [_;T_arg_nexp (Ne_const max)]),_) ->
IRange (Just (natFromInteger max))
| (T_app "range" _,_) -> IRange Nothing
| (T_app i (T_args []),Tag_enum max) ->
IEnum i (natFromInteger max)
| (T_id i,Tag_enum max) ->
IEnum i (natFromInteger max)
| _ -> IOther
end
let extract_parm (E_aux e (_,tannot)) =
match e with
| E_id (Id_aux (Id i) _) ->
match tannot with
| Just(t,tag,_,_,_) -> (i,(extract_ityp t tag))
| _ -> (i,IOther) end
| _ ->
let i = "Unnamed" in
match tannot with
| Just(t,tag,_,_,_) -> (i,(extract_ityp t tag))
| _ -> (i,IOther) end
end
let rec extract_from_decode decoder =
match decoder with
| [] -> []
| (FCL_aux (FCL_Funcl _ pat exp) _)::decoder ->
(match exp with
| E_aux (E_app (Id_aux(Id id) _) parms) (_,(Just (_,Tag_ctor,_,_,_))) ->
Instr_form id (List.map extract_parm parms) []
| _ -> Skipped end)::(extract_from_decode decoder)
end
let rec extract_effects_of_fcl id execute = match execute with
| [] -> []
| FCL_aux (FCL_Funcl _ (P_aux (P_app (Id_aux (Id i) _) _) _) _) (_,(Just(_,_,_,Effect_aux(Effect_set efs) _,_))) :: executes ->
if i = id
then efs
else extract_effects_of_fcl id executes
| _::executes -> extract_effects_of_fcl id executes
end
let rec extract_patt_parm (P_aux p (_,tannot)) =
let t = match tannot with
| Just(t,tag,_,_,_) -> extract_ityp t tag
| _ -> IOther end in
match p with
| P_lit lit -> ("",t)
| P_wild -> ("Unnamed",t)
| P_as _ (Id_aux (Id id) _) -> (id,t)
| P_typ typ p -> extract_patt_parm p
| P_id (Id_aux (Id id) _) -> (id,t)
| P_app (Id_aux (Id id) _) [] -> (id,t)
| _ -> ("",t) end
let rec extract_from_execute fcls = match fcls with
| [] -> []
| FCL_aux (FCL_Funcl _ (P_aux (P_app (Id_aux (Id i) _) parms) _) _) (_,Just(_,_,_,Effect_aux(Effect_set efs) _,_))::fcls ->
(Instr_form i (List.map extract_patt_parm parms) efs)::extract_from_execute fcls
end
let rec extract_effects instrs execute =
match instrs with
| [] -> []
| Skipped::instrs -> Skipped::(extract_effects instrs execute)
| (Instr_form id parms [])::instrs ->
(Instr_form id parms (extract_effects_of_fcl id execute))::(extract_effects instrs execute)
end
let extract_instructions_old decode_name execute_name defs =
let (Just decoder) = find_function defs (Id_aux (Id decode_name) Unknown) in
let (Just executer) = find_function defs (Id_aux (Id execute_name) Unknown) in
let instr_no_effects = extract_from_decode decoder in
let instructions = extract_effects instr_no_effects executer in
instructions
let extract_instructions execute_name defs =
let (Just executer) = find_function defs (Id_aux (Id execute_name) Unknown) in
let instructions = extract_from_execute executer in
instructions
|
