summaryrefslogtreecommitdiff
path: root/src/lem_interp/interp_inter_imp.lem
diff options
context:
space:
mode:
Diffstat (limited to 'src/lem_interp/interp_inter_imp.lem')
-rw-r--r--src/lem_interp/interp_inter_imp.lem133
1 files changed, 107 insertions, 26 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 14a286cb..19d41f8c 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
@@ -27,7 +28,7 @@ end
let intern_value v = match v with
| Bitvector bs inc fst -> Interp.V_vector fst inc (to_bits bs)
- | Bytevector bys inc fst -> Interp.V_vector fst inc
+ | Bytevector bys -> Interp.V_vector 0 true
(to_bits (List.reverse
(List.concat (List.map (fun n -> boolListFrombitSeq 8 (bitSeqFromInteger (Just 8) (integerFromNat n))) bys))))
| Unknown -> Interp.V_unknown
@@ -40,18 +41,33 @@ let extern_reg r slice = match (r,slice) with
| (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
+let rec extern_value mode for_mem v = match v with
+ | Interp.V_track v regs ->
+ let (external_v,_) = extern_value mode for_mem v in
+ (external_v,
+ if (for_mem && mode.Interp.track_values)
+ then (Just (List.map (fun r -> extern_reg r Nothing) regs))
+ else Nothing)
| Interp.V_vector fst inc bits ->
if for_mem
- then (Bytevector (List.reverse (to_bytes (from_bits bits))) inc fst, Nothing)
+ then (Bytevector (List.reverse (to_bytes (from_bits bits))), Nothing)
else (Bitvector (from_bits bits) inc fst, Nothing)
- | Interp.V_track (Interp.V_vector fst inc bits) regs ->
+ | Interp.V_lit (L_aux L_zero _) ->
if for_mem
- then (Bytevector (List.reverse (to_bytes (from_bits bits))) inc fst,
- if (mode.Interp.track_values)
- then (Just (List.map (fun r -> extern_reg r Nothing) regs))
- else Nothing)
- else (Bitvector (from_bits bits) inc fst, Nothing)
+ then (Bytevector [0],Nothing)
+ else (Bitvector [false] true 0, Nothing)
+ | Interp.V_lit (L_aux L_false _) ->
+ if for_mem
+ then (Bytevector [0],Nothing)
+ else (Bitvector [false] true 0, Nothing)
+ | Interp.V_lit (L_aux L_one _) ->
+ if for_mem
+ then (Bytevector [1],Nothing)
+ else (Bitvector [true] true 0, Nothing)
+ | Interp.V_lit (L_aux L_true _) ->
+ if for_mem
+ then (Bytevector [1],Nothing)
+ else (Bitvector [true] true 0, Nothing)
| _ -> (Unknown,Nothing)
end
@@ -81,17 +97,55 @@ let memory_functions =
match length with
| Interp.V_lit (L_aux (L_num len) _) ->
let (v,regs) = extern_value mode true location in
- (v,len,regs) end end)));
+ (v,len,regs)
+ | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
+ let (v,loc_regs) = extern_value mode true location in
+ match loc_regs with
+ | Nothing -> (v,len,Just (List.map (fun r -> extern_reg r Nothing) size_regs))
+ | Just loc_regs -> (v,len,Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) size_regs)))
+ end end end)));
+ ("MEMr_reserve", (Just(Read_reserve),Nothing,
+ (fun mode v -> match v with
+ | Interp.V_tuple [location;length] ->
+ match length with
+ | Interp.V_lit (L_aux (L_num len) _) ->
+ let (v,regs) = extern_value mode true location in
+ (v,len,regs)
+ | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
+ let (v,loc_regs) = extern_value mode true location in
+ match loc_regs with
+ | Nothing -> (v,len,Just (List.map (fun r -> extern_reg r Nothing) size_regs))
+ | Just loc_regs -> (v,len,Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) size_regs)))
+ end end end)));
("MEMw", (Nothing, Just(Write_plain),
(fun mode v -> match v with
| Interp.V_tuple [location;length] ->
match length with
| Interp.V_lit (L_aux (L_num len) _) ->
let (v,regs) = extern_value mode true location in
- (v,len,regs) end end)));
+ (v,len,regs)
+ | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
+ let (v,loc_regs) = extern_value mode true location in
+ match loc_regs with
+ | Nothing -> (v,len,Just (List.map (fun r -> extern_reg r Nothing) size_regs))
+ | Just loc_regs -> (v,len,Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) size_regs)))
+ end end end)));
+ ("MEMw_conditional", (Nothing, Just(Write_conditional),
+ (fun mode v -> match v with
+ | Interp.V_tuple [location;length] ->
+ match length with
+ | Interp.V_lit (L_aux (L_num len) _) ->
+ let (v,regs) = extern_value mode true location in
+ (v,len,regs)
+ | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
+ let (v,loc_regs) = extern_value mode true location in
+ match loc_regs with
+ | Nothing -> (v,len,Just (List.map (fun r -> extern_reg r Nothing) size_regs))
+ | Just loc_regs -> (v,len,Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) size_regs)))
+ end end end)));
]
-let rec interp_to_value_helper 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))
@@ -99,20 +153,36 @@ let rec interp_to_value_helper thunk =
match List.lookup i external_functions with
| Nothing -> (Nothing, Just (Internal_error ("External function not available " ^ i)))
| Just f ->
- interp_to_value_helper (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 "no_matching_pattern") _) -> (Nothing,Just Not_an_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
+ 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
@@ -120,8 +190,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
+ let (instr_decoded,error) = interp_to_value_helper value instr_external
(fun _ -> Interp.resume
(make_mode true false)
(Interp.Thunk_frame
@@ -130,12 +210,13 @@ 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 (Interp.Thunk_frame
+ 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)
- | (Nothing, Just err) -> err
+ | (Nothing, Just err) -> Decode_error err
end
- | (Nothing, Just err) -> err
+ | (Nothing, Just err) -> Decode_error err
end
let rec interp_to_outcome mode thunk =
@@ -163,8 +244,8 @@ let rec interp_to_outcome mode thunk =
match List.lookup i memory_functions with
| (Just (_,Just write_k,f)) ->
let (location, length, tracking) = (f mode loc_val) in
- let (value, val_tracking) = (extern_value mode true write_val) in
- Write_mem write_k location length tracking value val_tracking (fun b -> next_state)
+ let (value, v_tracking) = (extern_value mode true write_val) in
+ Write_mem write_k location length tracking value v_tracking (fun b -> next_state)
| _ -> Error ("Memory " ^ i ^ " function with write kind not found")
end
| Interp.Barrier (Id_aux (Id i) _) lval ->
@@ -202,8 +283,8 @@ let rec ie_loop mode i_state =
(E_write_reg reg value)::(ie_loop mode i_state)
| Read_mem read_k loc length tracking i_state_fun ->
(E_read_mem read_k loc length tracking)::(ie_loop mode (i_state_fun Unknown))
- | Write_mem write_k loc length l_track value v_track i_state_fun ->
- (E_write_mem write_k loc length l_track value v_track)::(ie_loop mode (i_state_fun true))
+ | Write_mem write_k loc length tracking value v_tracking i_state_fun ->
+ (E_write_mem write_k loc length tracking value v_tracking)::(ie_loop mode (i_state_fun true))
| Internal _ _ next -> (ie_loop mode next)
end ;;
@@ -222,9 +303,9 @@ let rec rr_ie_loop mode i_state =
| Read_mem read_k loc length tracking i_state_fun ->
let (events,outcome) = (rr_ie_loop mode (i_state_fun Unknown)) in
(((E_read_mem read_k loc length tracking)::events),outcome)
- | Write_mem write_k loc length l_track value v_track i_state_fun ->
+ | Write_mem write_k loc length tracking value v_tracking i_state_fun ->
let (events,outcome) = (rr_ie_loop mode (i_state_fun true)) in
- (((E_write_mem write_k loc length l_track value v_track)::events),outcome)
+ (((E_write_mem write_k loc length tracking value v_tracking)::events),outcome)
| Internal _ _ next -> (rr_ie_loop mode next)
end ;;
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 18:37:12 +0000