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
|
open import Interp_ast
open import Interp_utilities
open import Pervasives
type instr_parm_typ =
| IBit
| IBitvector of maybe integer
| IOther
type instruction_form =
| Instr_form of string * list (string * instr_parm_typ) * list base_effect
| Skipped
val extract_instructions : string -> string -> defs tannot -> list instruction_form
let extract_parm (E_aux e (_,tannot)) =
match e with
| E_id (Id_aux (Id i) _) ->
match tannot with
| Just(T_id "bit",_,_,_) -> (i,IBit)
| Just(T_id "bool",_,_,_) -> (i,IBit)
| Just(T_app "vector" (T_args [T_arg_nexp _; T_arg_nexp (Ne_const len); _; T_arg_typ (T_id "bit")]),_,_,_) ->
(i,IBitvector (Just len))
| Just(T_app "vector" (T_args [T_arg_nexp _; T_arg_nexp _; _; T_arg_typ (T_id "bit")]),_,_,_) ->
(i,IBitvector Nothing)
| _ -> (i,IOther) end
| _ ->
let i = "Unnamed" in
match tannot with
| Just(T_id "bit",_,_,_) -> (i,IBit)
| Just(T_id "bool",_,_,_) -> (i,IBit)
| Just(T_app "vector" (T_args [T_arg_nexp _; T_arg_nexp (Ne_const len); _; T_arg_typ (T_id "bit")]),_,_,_) ->
(i,IBitvector (Just len))
| Just(T_app "vector" (T_args [T_arg_nexp _; T_arg_nexp _; _; T_arg_typ (T_id "bit")]),_,_,_) ->
(i,IBitvector Nothing)
| _ -> (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_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 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
|
