summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/lem_interp/instruction_extractor.lem27
-rw-r--r--src/lem_interp/interp.lem31
-rw-r--r--src/lem_interp/interp_inter_imp.lem39
3 files changed, 69 insertions, 28 deletions
diff --git a/src/lem_interp/instruction_extractor.lem b/src/lem_interp/instruction_extractor.lem
index d4a52890..d2597740 100644
--- a/src/lem_interp/instruction_extractor.lem
+++ b/src/lem_interp/instruction_extractor.lem
@@ -2,13 +2,13 @@ open import Interp_ast
open import Interp_utilities
open import Pervasives
-type typ =
-| Bit
-| Bitvector of maybe integer
-| Other
+type instr_parm_typ =
+| IBit
+| IBitvector of maybe integer
+| IOther
type instruction_form =
-| Instr of string * list (string * typ) * list base_effect
+| Instr_form of string * list (string * instr_parm_typ) * list base_effect
| Skipped
val extract_instructions : string -> string -> defs tannot -> list instruction_form
@@ -17,13 +17,14 @@ let extract_parm (E_aux e (_,tannot)) =
match e with
| E_id (Id_aux (Id i) _) ->
match tannot with
- | Just(T_id "bit",_,_,_) -> (i,Bit)
+ | 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,Bitvector (Just len))
+ (i,IBitvector (Just len))
| Just(T_app "vector" (T_args [T_arg_nexp _; T_arg_nexp _; _; T_arg_typ (T_id "bit")]),_,_,_) ->
- (i,Bitvector Nothing)
- | _ -> (i,Other) end
- | _ -> ("UNKNOWN_PARM",Other)
+ (i,IBitvector Nothing)
+ | _ -> (i,IOther) end
+ | _ -> ("UNKNOWN_PARM",IOther)
end
let rec extract_from_decode decoder =
@@ -32,7 +33,7 @@ let rec extract_from_decode decoder =
| (FCL_aux (FCL_Funcl _ pat exp) _)::decoder ->
(match exp with
| E_aux (E_app (Id_aux(Id id) _) parms) (_,(Just (_,Tag_ctor,_,_))) ->
- Instr id (List.map extract_parm parms) []
+ Instr_form id (List.map extract_parm parms) []
| _ -> Skipped end)::(extract_from_decode decoder)
end
@@ -49,8 +50,8 @@ let rec extract_effects instrs execute =
match instrs with
| [] -> []
| Skipped::instrs -> Skipped::(extract_effects instrs execute)
- | (Instr id parms [])::instrs ->
- (Instr id parms (extract_effects_of_fcl id execute))::(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 =
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index a436d652..6febc709 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -7,6 +7,8 @@ open import String_extra (* for 'show' to convert nat to string) *)
open import Interp_ast
open import Interp_utilities
+open import Instruction_extractor
+
type tannot = Interp_utilities.tannot
val intern_annot : tannot -> tannot
@@ -112,9 +114,17 @@ type lenv = LEnv of nat * env
let emem = LMem 1 Map.empty
let eenv = LEnv 1 []
+type sub_reg_map = list (id * index_range)
+
(*top_level is a tuple of
- (all definitions, letbound and enum values, register values, Typedef union constructors, sub register mappings, and register aliases) *)
-type top_level = Env of (defs tannot) * env * env * list (id * typ) * list (id * list (id * index_range)) * list (id * (alias_spec tannot))
+ (all definitions,
+ all extracted instructions (where possible),
+ letbound and enum values,
+ register values,
+ Typedef union constructors,
+ sub register mappings, and register aliases) *)
+type top_level =
+ | Env of (defs tannot) * list instruction_form * env * env * list (id * typ) * list (id * sub_reg_map) * list (id * (alias_spec tannot))
type action =
| Read_reg of reg_form * maybe (integer * integer)
@@ -982,7 +992,7 @@ let rec exp_list mode t_level build_e build_v l_env l_mem vals exps =
end
and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
- let (Env defs lets regs ctors subregs aliases) = t_level in
+ let (Env defs instrs lets regs ctors subregs aliases) = t_level in
let (typ,tag,ncs,effect) = match annot with
| Nothing -> (T_var "fresh_v", Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
| Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in
@@ -1757,7 +1767,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
end
and create_write_message_or_update mode t_level value l_env l_mem is_top_level ((LEXP_aux lexp (l,annot)):lexp tannot) : ((outcome * lmem * lenv) * maybe ((exp tannot) -> lenv -> ((lexp tannot) * lenv))) =
- let (Env defs lets regs ctors subregs aliases) = t_level in
+ let (Env defs instrs lets regs ctors subregs aliases) = t_level in
let (typ,tag,ncs,ef) = match annot with
| Nothing -> (T_var "fresh_v", Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
| Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in
@@ -2068,7 +2078,7 @@ and interp_letbind mode t_level l_env l_mem (LB_aux lbind (l,annot)) =
end
and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
- let (Env defs lets regs ctors subregs aliases) = t_level in
+ let (Env defs instrs lets regs ctors subregs aliases) = t_level in
let stack = Hole_frame (Id_aux (Id "0") Unknown)
(E_aux (E_id (Id_aux (Id "0") l)) (l,(intern_annot annot)))
t_level l_env l_mem Top in
@@ -2113,14 +2123,14 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
(l,(intern_annot annot))) t_level l_env l_mem Top), l_mem,l_env) end
let rec to_global_letbinds (Defs defs) t_level =
- let (Env defs' lets regs ctors subregs aliases) = t_level in
+ let (Env defs' instrs lets regs ctors subregs aliases) = t_level in
match defs with
| [] -> ((Value (V_lit (L_aux L_unit Unknown)), emem, eenv),t_level)
| def::defs ->
match def with
| DEF_val lbind ->
match interp_letbind <|eager_eval=true; track_values=false;|> t_level eenv emem lbind with
- | ((Value v,lm,(LEnv _ le)),_) -> to_global_letbinds (Defs defs) (Env defs' (lets++le) regs ctors subregs aliases)
+ | ((Value v,lm,(LEnv _ le)),_) -> to_global_letbinds (Defs defs) (Env defs' instrs (lets++le) regs ctors subregs aliases)
| ((Action a s,lm,le),_) ->
((Error Unknown "Top level let may not access memory, registers or (for now) external functions", lm,le),t_level)
| (e,_) -> (e,t_level) end
@@ -2128,14 +2138,17 @@ let rec to_global_letbinds (Defs defs) t_level =
match tdef with
| TD_enum id ns ids _ ->
let enum_vals = map (fun eid -> (eid,V_ctor eid (T_id (get_id id)) unitv)) ids in
- to_global_letbinds (Defs defs) (Env defs' (lets++enum_vals) regs ctors subregs aliases)
+ to_global_letbinds (Defs defs) (Env defs' instrs (lets++enum_vals) regs ctors subregs aliases)
| _ -> to_global_letbinds (Defs defs) t_level end
| _ -> to_global_letbinds (Defs defs) t_level
end
end
+(*TODO Contemplate making decode and execute environment variables instead of these constants*)
let to_top_env defs =
- let t_level = Env defs [] (to_registers defs) (to_data_constructors defs) (to_register_fields defs) (to_aliases defs) in
+ let t_level = Env defs (extract_instructions "decode" "execute" defs)
+ [] (* empty letbind and enum values, call below will fill in any *)
+ (to_registers defs) (to_data_constructors defs) (to_register_fields defs) (to_aliases defs) in
let (o,t_level) = to_global_letbinds defs t_level in
match o with
| (Value _,_,_) -> (Nothing,t_level)
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index c18f07f7..b930e8ec 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -1,5 +1,6 @@
import Interp
import Interp_lib
+import Instruction_extractor
open import Interp_ast
open import Interp_interface
open import Pervasives
@@ -129,7 +130,7 @@ let memory_functions =
end end end)));
]
-let rec interp_to_value_helper arg thunk =
+let rec interp_to_value_helper arg instr thunk =
match thunk() with
| Interp.Value value -> (Just value,Nothing)
| Interp.Error l msg -> (Nothing, Just (Internal_error msg))
@@ -137,20 +138,36 @@ let rec interp_to_value_helper arg thunk =
match List.lookup i external_functions with
| Nothing -> (Nothing, Just (Internal_error ("External function not available " ^ i)))
| Just f ->
- interp_to_value_helper arg (fun _ -> Interp.resume (make_mode true false) stack (Just (f value)))
+ interp_to_value_helper arg instr (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 "unsupported_instruction") _) -> (Nothing,Just (Unsupported_instruction_error instr))
| E_id (Id_aux (Id "no_matching_pattern") _) -> (Nothing,Just (Not_an_instruction_error arg))
end
| _ -> (Nothing, Just (Internal_error "Memory or register requested in decode"))
end
+let rec find_instruction i = function
+ | [] -> Nothing
+ | Skipped::instrs -> find_instruction i instrs
+ | ((Instruction_extractor.Instr_form name parms effects) as instr)::instrs ->
+ if i = name
+ then Just instr
+ else find_instruction i instrs
+end
+
+let migrate_typ = function
+ | Instruction_extractor.IBit -> Bit
+ | Instruction_extractor.IBitvector len -> Bvector len
+ | Instruction_extractor.IOther -> Other
+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 value
+ let (Interp.Env _ instructions _ _ _ _ _) = top_level in
+ let (instr_decoded,error) = interp_to_value_helper value ("",[],[])
(fun _ -> Interp.resume
(make_mode true false)
(Interp.Thunk_frame
@@ -158,8 +175,18 @@ let decode_to_istate top_level value =
top_level Interp.eenv Interp.emem Interp.Top) Nothing) in
match (instr_decoded,error) with
| (Just instr, _) ->
+ let instr_external = match instr with
+ | Interp.V_ctor (Id_aux (Id i) _) _ parm ->
+ match (find_instruction i instructions) with
+ | Just(Instruction_extractor.Instr_form name parms effects) ->
+ match (parm,parms) with
+ | (Interp.V_lit (L_aux L_unit _),[]) -> (name, [], effects)
+ | (value,[(p_name,ie_typ)]) -> (name, [(p_name,(migrate_typ ie_typ),fst(extern_value mode false value))], effects)
+ | (Interp.V_tuple vals,parms) ->
+ (name, (Interp.map2 (fun value (p_name,ie_typ) -> (p_name,(migrate_typ ie_typ),fst(extern_value mode false value))) vals parms), effects)
+ end end end in
let (arg,_) = Interp.to_exp mode Interp.eenv instr in
- let (instr_decoded,error) = interp_to_value_helper value
+ let (instr_decoded,error) = interp_to_value_helper value instr_external
(fun _ -> Interp.resume
(make_mode true false)
(Interp.Thunk_frame
@@ -168,7 +195,7 @@ let decode_to_istate top_level value =
match (instr_decoded,error) with
| (Just instr,_) ->
let (arg,_) = Interp.to_exp mode Interp.eenv instr in
- Instr ("",[],[])
+ Instr instr_external
(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)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 11:20:44 +0000