diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 88 | ||||
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 7 | ||||
| -rw-r--r-- | src/lem_interp/run_interp_model.ml | 3 | ||||
| -rw-r--r-- | src/lem_interp/run_with_elf.ml | 4 | ||||
| -rw-r--r-- | src/lem_interp/run_with_elf_cheri.ml | 6 | ||||
| -rw-r--r-- | src/parser.mly | 6 |
6 files changed, 66 insertions, 48 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 9ed4efed..df17fffd 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -251,6 +251,32 @@ let update_reg_value_slice reg_name v start stop v2 = else (Interp.fupdate_vector_slice v_internal v2_internal start stop)) +(*TODO: Only find some sub piece matches, need to look for field/slice sub pieces*) +(*TODO immediate: this will be impacted by need to change slicing *) +let rec find_reg_name reg = function + | [] -> Nothing + | (reg_name,v)::registers -> + match (reg,reg_name) with + | (Reg i start size dir, Reg n start2 size2 dir2) -> + if i = n && size = size2 then (Just v) else find_reg_name reg registers + | (Reg_slice i _ _ (p1,p2), Reg n _ _ _) -> + if i = n then (Just (slice_reg_value v p1 p2)) else find_reg_name reg registers + | (Reg_field i _ _ f (p1,p2), Reg n _ _ _) -> + if i = n then (Just (slice_reg_value v p1 p2)) else find_reg_name reg registers + | (Reg_slice i _ _ (p1,p2), Reg_slice n _ _ (p3,p4)) -> + if i=n + then if p1=p3 && p2 = p4 then (Just v) + else if p1>=p3 && p2<= p4 then (Just (slice_reg_value v p1 p2)) + else find_reg_name reg registers + else find_reg_name reg registers + | (Reg_field i _ _ f _,Reg_field n _ _ fn _) -> + if i=n && f = fn then (Just v) else find_reg_name reg registers + | (Reg_f_slice i _ _ f _ (p1,p2), Reg_f_slice n _ _ fn _ (p3,p4)) -> + if i=n && f=fn && p1=p3 && p2=p3 then (Just v) else find_reg_name reg registers + | _ -> find_reg_name reg registers +end end + + 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)] @@ -262,7 +288,7 @@ let initial_instruction_state top_level main args = type interp_value_helper_mode = Ivh_translate | Ivh_decode | Ivh_unsupported | Ivh_illegal -let rec interp_to_value_helper arg ivh_mode err_str instr direction thunk = +let rec interp_to_value_helper arg ivh_mode err_str instr direction registers thunk = let errk_str = match ivh_mode with | Ivh_translate -> "translate" | Ivh_decode -> "decode" @@ -291,7 +317,7 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction thunk = match List.lookup i (Interp_lib.library_functions direction) with | Nothing -> (Nothing, Just (Internal_error ("External function not available " ^ i))) | Just f -> - interp_to_value_helper arg ivh_mode err_str instr direction + interp_to_value_helper arg ivh_mode err_str instr direction registers (fun _ -> Interp.resume (make_interpreter_mode true false) stack (Just (f value))) end | (Interp.Action (Interp.Exit ((E_aux e _) as exp)) stack,_,_) -> @@ -304,12 +330,24 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction thunk = | _ -> (Nothing, Just (Internal_error ("Exit called with unrecognized expression bound to an id " ^ i))) end) | _ -> (Nothing, Just (Internal_error "Exit called with unrecognized expression")) end - | (Interp.Action (Interp.Read_reg r _) _,_,_) -> + | (Interp.Action (Interp.Read_reg r slice) stack,_,_) -> let rname = match r with | Interp.Reg (Id_aux (Id i) _) _ _ -> i | Interp.SubReg (Id_aux (Id i) _) (Interp.Reg (Id_aux (Id i2) _) _ _) _ -> i2 ^ "." ^ i | _ -> Assert_extra.failwith "Reg not following expected structure" end in - (Nothing, Just (Internal_error ("Register read of "^ rname^" request in a " ^ errk_str ^ " of " ^ err_str))) + let err_value = + (Nothing, Just (Internal_error ("Register read of "^ rname^" request in a " ^ errk_str ^ " of " ^ err_str))) + in + (match registers with + | Nothing -> err_value + | Just(regs) -> + let reg = extern_reg r slice in + match find_reg_name reg regs with + | Nothing -> err_value + | Just v -> + let value = intern_reg_value v in + interp_to_value_helper arg ivh_mode err_str instr direction registers + (fun _ -> Interp.resume (make_interpreter_mode true false) stack (Just value)) end end) | (Interp.Action (Interp.Write_reg _ _ _) _,_,_) -> (Nothing, Just (Internal_error ("Register write request in a " ^ errk_str))) | (Interp.Action (Interp.Read_mem _ _ _) _,_,_) -> @@ -338,7 +376,7 @@ let build_context defs reads writes write_eas write_vals barriers externs = Context context (if Interp.is_inc(dir) then D_increasing else D_decreasing) reads writes write_eas write_vals barriers externs end -let translate_address top_level end_flag thunk_name address = +let translate_address top_level end_flag thunk_name registers address = let (Address bytes i) = address in let mode = make_mode true false end_flag in let int_mode = mode.internal_mode in @@ -348,9 +386,10 @@ let translate_address top_level end_flag thunk_name address = let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in let (address,error) = interp_to_value_helper (Opcode bytes) Ivh_translate val_str ("",[],[]) internal_direction - (fun _ -> Interp.resume - int_mode - (Interp.Thunk_frame + registers + (fun _ -> Interp.resume + int_mode + (Interp.Thunk_frame (E_aux (E_app (Id_aux (Id thunk_name) Interp_ast.Unknown) [arg;E_aux (E_lit (L_aux (L_num 0) Interp_ast.Unknown)) (Interp_ast.Unknown,Nothing)]) (Interp_ast.Unknown, Nothing)) @@ -395,14 +434,14 @@ let migrate_typ = function end -let decode_to_istate top_level value = +let decode_to_istate top_level registers value = let mode = make_interpreter_mode true false in let (Context ((Interp.Env _ instructions _ _ _ _ _ _) as top_env) direction _ _ _ _ _ _) = top_level in let intern_val = intern_opcode direction value in let val_str = Interp.string_of_value intern_val in let (arg,_) = Interp.to_exp mode Interp.eenv intern_val in let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in - let (instr_decoded,error) = interp_to_value_helper value Ivh_decode val_str ("",[],[]) internal_direction + let (instr_decoded,error) = interp_to_value_helper value Ivh_decode val_str ("",[],[]) internal_direction registers (fun _ -> Interp.resume mode (Interp.Thunk_frame @@ -431,6 +470,7 @@ let decode_to_istate top_level value = let (arg,_) = Interp.to_exp mode Interp.eenv instr in let (instr_decoded,error) = interp_to_value_helper value Ivh_unsupported val_str instr_external internal_direction + registers (fun _ -> Interp.resume mode (Interp.Thunk_frame @@ -453,8 +493,8 @@ let decode_to_istate top_level value = end -let decode_to_instruction (top_level:context) (value:opcode) : instruction_or_decode_error = - match decode_to_istate top_level value with +let decode_to_instruction (top_level:context) registers (value:opcode) : instruction_or_decode_error = + match decode_to_istate top_level registers value with | Instr inst is -> IDE_instr inst | Decode_error de -> IDE_decode_error de end @@ -609,30 +649,6 @@ let interp mode (IState interp_state context) = | (o,_) -> o end -(*TODO: Only find some sub piece matches, need to look for field/slice sub pieces*) -(*TODO immediate: this will be impacted by need to change slicing *) -let rec find_reg_name reg = function - | [] -> Nothing - | (reg_name,v)::registers -> - match (reg,reg_name) with - | (Reg i start size dir, Reg n start2 size2 dir2) -> - if i = n && size = size2 then (Just v) else find_reg_name reg registers - | (Reg_slice i _ _ (p1,p2), Reg n _ _ _) -> - if i = n then (Just (slice_reg_value v p1 p2)) else find_reg_name reg registers - | (Reg_field i _ _ f (p1,p2), Reg n _ _ _) -> - if i = n then (Just (slice_reg_value v p1 p2)) else find_reg_name reg registers - | (Reg_slice i _ _ (p1,p2), Reg_slice n _ _ (p3,p4)) -> - if i=n - then if p1=p3 && p2 = p4 then (Just v) - else if p1>=p3 && p2<= p4 then (Just (slice_reg_value v p1 p2)) - else find_reg_name reg registers - else find_reg_name reg registers - | (Reg_field i _ _ f _,Reg_field n _ _ fn _) -> - if i=n && f = fn then (Just v) else find_reg_name reg registers - | (Reg_f_slice i _ _ f _ (p1,p2), Reg_f_slice n _ _ fn _ (p3,p4)) -> - if i=n && f=fn && p1=p3 && p2=p3 then (Just v) else find_reg_name reg registers - | _ -> find_reg_name reg registers -end end (*Update slice potentially here*) let reg_size = function diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index 61074ca0..90b22fd5 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -880,11 +880,11 @@ type i_state_or_error = (** PS:I agree. propose to remove this: Function to decode an instruction and build the state to run it*) -val decode_to_istate : context -> opcode -> i_state_or_error +val decode_to_istate : context -> maybe (list (reg_name * register_value)) -> opcode -> i_state_or_error (** propose to add this, and then use instruction_to_istate on the result: Function to decode an instruction and build the state to run it*) (** PS made a placeholder in interp_inter_imp.lem, but it just uses decode_to_istate and throws away the istate; surely it's easy to just do what's necessary to get the instruction. This sort-of works, but it crashes on ioid 10 after 167 steps - maybe instruction_to_istate (which I wasn't using directly before) isn't quite right? *) -val decode_to_instruction : context -> opcode -> instruction_or_decode_error +val decode_to_instruction : context -> maybe (list (reg_name * register_value))-> opcode -> instruction_or_decode_error (*Function to generate the state to run from an instruction form; is always an Instr*) val instruction_to_istate : context -> instruction -> instruction_state (*i_state_or_error*) @@ -1149,7 +1149,8 @@ let clear_low_order_bits_of_address a = | _ -> failwith "Address does not contain 8 bytes" end -val translate_address : context -> end_flag -> string -> address -> maybe address * maybe nat +val translate_address : + context -> end_flag -> string -> maybe (list (reg_name * register_value)) -> address -> maybe address * maybe nat val byte_list_of_memory_value : end_flag -> memory_value -> maybe (list byte) let byte_list_of_memory_value endian mv = diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml index e40dfe9f..9abf0442 100644 --- a/src/lem_interp/run_interp_model.ml +++ b/src/lem_interp/run_interp_model.ml @@ -340,7 +340,8 @@ let run show "exiting current evaluation" "" "" ""; step e,env', e | Escape _ -> assert false - | Error0 _ -> assert false + | Error0 _ -> failwith "Internal error" + | Fail0 _ -> failwith "Assertion in program failed" | Done -> show "done evalution" "" "" ""; assert false diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml index 75ed3b33..5ceff43a 100644 --- a/src/lem_interp/run_with_elf.ml +++ b/src/lem_interp/run_with_elf.ml @@ -906,7 +906,7 @@ let fetch_instruction_opcode_and_update_ia model addr_trans = let pc_addr = address_of_register_value nextPC in (match pc_addr with | Some pc_addr -> - let pc_a = match addr_trans pc_addr with + let pc_a = match addr_trans None pc_addr with | Some a, _ -> integer_of_address a | None, Some i -> failwith ("Address translation failed with error code " ^ (Nat_big_num.to_string i)) | _ -> failwith "Neither an address or a code on translate address" in @@ -990,7 +990,7 @@ let run () = endian mode, and translate function name *) let addr_trans = translate_address context E_big_endian "TranslateAddress" in - let startaddr = match addr_trans startaddr_internal with + let startaddr = match addr_trans None startaddr_internal with | Some a, _ -> integer_of_address a | None, Some i -> failwith ("Address translation failed with error code " ^ (Nat_big_num.to_string i)) | _ -> failwith "Neither an address or a code on translate address" diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml index ff4e5caa..05150f47 100644 --- a/src/lem_interp/run_with_elf_cheri.ml +++ b/src/lem_interp/run_with_elf_cheri.ml @@ -989,7 +989,7 @@ let fetch_instruction_opcode_and_update_ia model addr_trans = let pc_addr = address_of_register_value nextPC in (match pc_addr with | Some pc_addr -> - let pc_a = match addr_trans pc_addr with + let pc_a = match addr_trans None pc_addr with | Some a, _ -> integer_of_address a | None, Some i -> failwith ("Address translation failed with error code " ^ (Nat_big_num.to_string i)) | _ -> failwith "Neither an address or a code on translate address" in @@ -1021,7 +1021,7 @@ let rec fde_loop count context model mode track_dependencies opcode addr_trans = interactf "\n**** instruction %d from address %s ****\n" count (Printing_functions.register_value_to_string (get_pc_address model)); if !break_point && count = !break_instr then begin break_point := false; eager_eval := false end; - let (instruction,istate) = match Interp_inter_imp.decode_to_istate context opcode with + let (instruction,istate) = match Interp_inter_imp.decode_to_istate context None opcode with | Instr(instruction,istate) -> interactf "\n**** Running: %s ****\n" (Printing_functions.instruction_to_string instruction); (instruction,istate) @@ -1073,7 +1073,7 @@ let run () = endian mode, and translate function name *) let addr_trans = translate_address context E_big_endian "TranslateAddress" in - let startaddr = match addr_trans startaddr_internal with + let startaddr = match addr_trans None startaddr_internal with | Some a, _ -> integer_of_address a | None, Some i -> failwith ("Address translation failed with error code " ^ (Nat_big_num.to_string i)) | _ -> failwith "Neither an address or a code on translate address" diff --git a/src/parser.mly b/src/parser.mly index 8868340d..00bcb465 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -962,7 +962,7 @@ patsexp: { peloc (Pat_exp($1,$3)) } letbind: - | Let_ atomic_pat Eq atomic_exp + | Let_ atomic_pat Eq exp { lbloc (LB_val_implicit($2,$4)) } | Let_ typquant atomic_typ atomic_pat Eq exp { lbloc (LB_val_explicit((mk_typschm $2 $3 2 3),$4,$6)) } @@ -1256,11 +1256,11 @@ def: { dloc (DEF_spec($1)) } | default_typ { dloc (DEF_default($1)) } - | Register atomic_typ id + | Register typ id { dloc (DEF_reg_dec(DEC_aux(DEC_reg($2,$3),loc ()))) } | Register Alias id Eq exp { dloc (DEF_reg_dec(DEC_aux(DEC_alias($3,$5),loc ()))) } - | Register Alias atomic_typ id Eq exp + | Register Alias typ id Eq exp { dloc (DEF_reg_dec(DEC_aux(DEC_typ_alias($3,$4,$6), loc ()))) } | Scattered scattered_def { dloc (DEF_scattered $2) } |