summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/lem_interp/interp.lem4
-rw-r--r--src/lem_interp/interp_inter_imp.lem37
-rw-r--r--src/lem_interp/interp_interface.lem10
-rw-r--r--src/test/run_power.ml58
4 files changed, 61 insertions, 48 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index ea06fa5d..bbcec75b 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -118,10 +118,6 @@ type lenv = LEnv of nat * env
let emem = LMem 1 Map.empty
let eenv = LEnv 1 []
-type read_kind = Read_plain | Read_reserve | Read_acquire
-type write_kind = Write_plain | Write_conditional | Write_release
-type barrier_kind = Sync | LwSync | Eieio | Isync | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB (* PS removed "plain" and added "Isync" and "ISB" *)
-
(*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))
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 8a5bd664..95cb3f36 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -8,7 +8,7 @@ val intern_value : value -> Interp.value
val extern_value : interp_mode -> bool -> Interp.value -> (value * maybe (list reg_name))
val extern_reg : Interp.reg_form -> maybe (integer * integer) -> reg_name
-let build_context defs = Interp.to_top_env defs
+let build_context defs = match Interp.to_top_env defs with (_,context) -> context end
let make_mode eager_eval tracking_values = <| Interp.eager_eval = eager_eval; Interp.track_values = tracking_values |>;;
let tracking_dependencies mode = mode.Interp.track_values
@@ -52,9 +52,14 @@ let extern_value mode for_mem v = match v with
| _ -> (Unknown,Nothing)
end
-let initial_instruction_state top_level main arg =
- let (e_arg,env) = Interp.to_exp <| Interp.eager_eval = true; Interp.track_values = false |> Interp.eenv (intern_value arg) in
- Interp.Thunk_frame (E_aux (E_app (Id_aux (Id main) Interp_ast.Unknown) [e_arg]) (Interp_ast.Unknown, Nothing)) top_level Interp.eenv Interp.emem
+let initial_instruction_state top_level main args =
+ let e_args = match args with
+ | [] -> [E_aux (E_lit (L_aux L_unit Interp_ast.Unknown)) (Interp_ast.Unknown,Nothing)]
+ | [arg] -> let (e,_) = Interp.to_exp (make_mode true false) Interp.eenv (intern_value arg) in [e]
+ | args -> List.map fst (List.map (Interp.to_exp (make_mode true false) Interp.eenv)
+ (List.map intern_value args)) end in
+ Interp.Thunk_frame (E_aux (E_app (Id_aux (Id main) Interp_ast.Unknown) e_args) (Interp_ast.Unknown, Nothing))
+ top_level Interp.eenv Interp.emem Interp.Top
(*For now, append to this list to add more external functions; should add to the mode record for more perhaps *)
let external_functions =
@@ -67,7 +72,13 @@ type mem_function = (string *
Should probably be expanded into a parameter to mode as with above
*)
let memory_functions =
- [ ("MEM", (Just(Read_plain), Just(Write_plain), (fun mode v -> extern_value mode true v)));
+ [ ("MEM", (Just(Read_plain), 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)));
]
let rec interp_to_outcome mode thunk =
@@ -87,16 +98,16 @@ let rec interp_to_outcome mode thunk =
| Interp.Read_mem (Id_aux (Id i) _) value slice ->
match List.lookup i memory_functions with
| (Just (Just read_k,_,f)) ->
- let (location, tracking) = (f mode value) in
- Read_mem read_k location tracking (fun v -> Interp.add_answer_to_stack next_state (intern_value v))
+ let (location, length, tracking) = (f mode value) in
+ Read_mem read_k location length tracking (fun v -> Interp.add_answer_to_stack next_state (intern_value v))
| _ -> Error ("Memory " ^ i ^ " function with read kind not found")
end
| Interp.Write_mem (Id_aux (Id i) _) loc_val slice write_val ->
match List.lookup i memory_functions with
| (Just (_,Just write_k,f)) ->
- let (location, tracking) = (f mode loc_val) in
+ 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 tracking value val_tracking (fun b -> next_state)
+ Write_mem write_k location length tracking value val_tracking (fun b -> next_state)
| _ -> Error ("Memory " ^ i ^ " function with write kind not found")
end
| Interp.Barrier (Id_aux (Id i) _) lval ->
@@ -122,10 +133,10 @@ let rec ie_loop mode i_state =
(E_read_reg reg)::(ie_loop mode (i_state_fun Unknown))
| Write_reg reg value i_state->
(E_write_reg reg value)::(ie_loop mode i_state)
- | Read_mem read_k loc tracking i_state_fun ->
- (E_read_mem read_k loc tracking)::(ie_loop mode (i_state_fun Unknown))
- | Write_mem write_k loc l_track value v_track i_state_fun ->
- (E_write_mem write_k loc l_track value v_track)::(ie_loop mode (i_state_fun true))
+ | 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))
| Internal _ next -> (ie_loop mode next)
end ;;
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index a7049633..e821aae8 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -14,7 +14,7 @@ val tracking_dependencies : interp_mode -> bool
(*Concrete types*)
type read_kind = Read_plain | Read_reserve | Read_acquire
type write_kind = Write_plain | Write_conditional | Write_release
-type barrier_kind = Plain | Sync | LwSync | Eieio | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD
+type barrier_kind = Sync | LwSync | Eieio | Isync | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB (* PS removed "plain" and added "Isync" and "ISB" *)
type value =
| Bitvector of list bool (* For register accesses *)
@@ -36,9 +36,9 @@ type reg_name =
type outcome =
(* Request to read memory, value is location to read followed by registers that location depended on when mode.track_values *)
-| Read_mem of read_kind * value * maybe (list reg_name) * (value -> instruction_state)
+| Read_mem of read_kind * value * integer * maybe (list reg_name) * (value -> instruction_state)
(* Request to write memory, first value and dependent registers is location, second is the value to write *)
-| Write_mem of write_kind * value * maybe (list reg_name) * value * maybe (list reg_name) * (bool -> instruction_state)
+| Write_mem of write_kind * value * integer * maybe (list reg_name) * value * maybe (list reg_name) * (bool -> instruction_state)
(* Request a memory barrier *)
| Barrier of barrier_kind * instruction_state
(* Request to read register, will track dependency when mode.track_values *)
@@ -53,8 +53,8 @@ type outcome =
| Error of string
type event =
-| E_read_mem of read_kind * value * maybe (list reg_name)
-| E_write_mem of write_kind * value * maybe (list reg_name) * value * maybe (list reg_name)
+| E_read_mem of read_kind * value * integer * maybe (list reg_name)
+| E_write_mem of write_kind * value * integer * maybe (list reg_name) * value * maybe (list reg_name)
| E_barrier of barrier_kind
| E_read_reg of reg_name
| E_write_reg of reg_name * value
diff --git a/src/test/run_power.ml b/src/test/run_power.ml
index 4526a79d..667792c0 100644
--- a/src/test/run_power.ml
+++ b/src/test/run_power.ml
@@ -1,8 +1,10 @@
open Printf ;;
-open Interp ;;
+(*open Interp ;;*)
open Interp_ast ;;
-open Interp_lib ;;
-open Run_interp ;;
+(*open Interp_lib ;;*)
+open Interp_interface ;;
+open Interp_inter_imp ;;
+open Run_interp_model ;;
let startaddr = ref "0" ;;
let mainaddr = ref "0" ;;
@@ -18,19 +20,22 @@ let big_endian = true ;;
let hex_to_big_int s = Big_int.big_int_of_int64 (Int64.of_string s) ;;
-let big_int_to_vec b size =
- (if big_endian then to_vec_inc else to_vec_dec)
- (V_tuple [(V_lit (L_aux (L_num size, Unknown)));
- (V_lit (L_aux (L_num b, Unknown)))])
+let big_int_to_vec for_mem b size =
+ fst (extern_value
+ (make_mode true false)
+ for_mem
+ ((if big_endian then Interp_lib.to_vec_inc else Interp_lib.to_vec_dec)
+ (Interp.V_tuple [(Interp.V_lit (L_aux (L_num size, Unknown)));
+ (Interp.V_lit (L_aux (L_num b, Unknown)))])))
;;
let mem = ref Mem.empty ;;
let add_mem byte addr =
assert(byte >= 0 && byte < 256);
- let vector = big_int_to_vec (Big_int.big_int_of_int byte) (Big_int.big_int_of_int 8) in
- let key = (*Id_aux (Id "MEM", Unknown), (* memory map no longer using id, just the address, since read/write id different *)*) addr in
- mem := Mem.add key vector !mem
+ let addr = big_int_to_vec true addr (Big_int.big_int_of_int 64) in
+ match addr with
+ | Bytevector addr -> mem := Mem.add addr byte !mem
;;
let add_section s =
@@ -61,11 +66,11 @@ let lr_init_value = Big_int.zero_big_int
let init_reg () =
let init name value size =
(* fix index - this is necessary for CR, indexed from 32 *)
- let offset = function
+(* let offset = function
V_vector(_, inc, v) ->
V_vector(Big_int.big_int_of_int (64 - size), inc, v)
- | _ -> assert false in
- Id_aux(Id name, Unknown), offset (big_int_to_vec value (Big_int.big_int_of_int size)) in
+ | _ -> assert false in*)
+ name, (*offset*) (big_int_to_vec false value (Big_int.big_int_of_int size)) in
List.fold_left (fun r (k,v) -> Reg.add k v r) Reg.empty [
(* XXX execute main() directly until we can handle the init phase *)
init "CIA" (hex_to_big_int !mainaddr) 64;
@@ -74,7 +79,7 @@ let init_reg () =
init "CTR" Big_int.zero_big_int 64;
init "CR" Big_int.zero_big_int 32;
init "LR" lr_init_value 64;
- Id_aux(Id "mode64bit", Unknown), V_lit (L_aux (L_true, Unknown));
+ "mode64bit", Bitvector [true];
]
;;
@@ -98,22 +103,23 @@ let time_it action arg =
;;
let get_reg reg name =
- let reg_content = Reg.find (Id_aux(Id name, Unknown)) reg in
- match to_num true reg_content with
- | V_lit(L_aux(L_num n, Unknown)) -> n
- | _ -> assert false
+ let reg_content = Reg.find name reg in reg_content
;;
-let rec fde_loop count entry mem reg ?mode prog =
+let eq_zero = function
+ | Bitvector bools -> List.for_all (not) bools
+;;
+
+let rec fde_loop count main_func parameters mem reg ?mode prog =
debugf "\n**** instruction %d ****\n" count;
- match Run_interp.run ~entry ~mem ~reg ~eager_eval:!eager_eval ?mode prog with
+ match Run_interp_model.run ~main_func ~parameters ~mem ~reg ~eager_eval:!eager_eval ?mode prog with
| false, _, _ -> eprintf "FAILURE\n"; exit 1
| true, mode, (reg, mem) ->
- if Big_int.eq_big_int (get_reg reg "CIA") lr_init_value then
+ if eq_zero (get_reg reg "CIA") then
eprintf "\nSUCCESS: returned with value %s\n"
- (Big_int.string_of_big_int (get_reg reg "GPR3"))
+ (Run_interp_model.val_to_string (get_reg reg "GPR3"))
else
- fde_loop (count+1) entry mem reg ~mode:mode prog
+ fde_loop (count+1) main_func parameters mem reg ~mode:mode prog
;;
let run () =
@@ -134,10 +140,10 @@ let run () =
close_in ic;
let reg = init_reg () in
(* entry point: unit -> unit fde *)
- let entry = E_aux(E_app(Id_aux((Id "fde"),Unknown),
- [E_aux(E_lit (L_aux(L_unit,Unknown)),(Unknown,None))]),(Unknown,None)) in
+ let funk_name = "fde" in
+ let args = [] in
let name = Filename.basename !file in
- let t =time_it (fun () -> fde_loop 0 entry !mem reg (name, Power.defs)) () in
+ let t =time_it (fun () -> fde_loop 0 funk_name args !mem reg (name, Power.defs)) () in
eprintf "Execution time: %f seconds\n" t
;;
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 14:34:43 +0000