(*========================================================================*) (* Sail *) (* *) (* Copyright (c) 2013-2017 *) (* Kathyrn Gray *) (* Shaked Flur *) (* Stephen Kell *) (* Gabriel Kerneis *) (* Robert Norton-Wright *) (* Christopher Pulte *) (* Peter Sewell *) (* Alasdair Armstrong *) (* Brian Campbell *) (* Thomas Bauereiss *) (* Anthony Fox *) (* Jon French *) (* Dominic Mulligan *) (* Stephen Kell *) (* Mark Wassell *) (* *) (* All rights reserved. *) (* *) (* This software was developed by the University of Cambridge Computer *) (* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) (* (REMS) project, funded by EPSRC grant EP/K008528/1. *) (* *) (* Redistribution and use in source and binary forms, with or without *) (* modification, are permitted provided that the following conditions *) (* are met: *) (* 1. Redistributions of source code must retain the above copyright *) (* notice, this list of conditions and the following disclaimer. *) (* 2. Redistributions in binary form must reproduce the above copyright *) (* notice, this list of conditions and the following disclaimer in *) (* the documentation and/or other materials provided with the *) (* distribution. *) (* *) (* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) (* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) (* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) (* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) (* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) (* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) (* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) (* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) (* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) (* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) (* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) (* SUCH DAMAGE. *) (*========================================================================*) open import Interp_ast import Interp import Interp_lib import Instruction_extractor import Set_extra open import Pervasives open import Assert_extra open import Interp_ast open import Interp_utilities open import Sail_impl_base open import Interp_interface val intern_reg_value : register_value -> Interp_ast.value val intern_mem_value : interp_mode -> direction -> memory_value -> Interp_ast.value val extern_reg_value : reg_name -> Interp_ast.value -> register_value val extern_with_track: forall 'a. interp_mode -> (Interp_ast.value -> 'a) -> Interp_ast.value -> ('a * maybe (list reg_name)) val extern_vector_value: Interp_ast.value -> list byte_lifted val extern_mem_value : Interp_ast.value -> memory_value val extern_reg : Interp_ast.reg_form -> maybe (nat * nat) -> reg_name let make_interpreter_mode eager_eval tracking_values debug = <| Interp.eager_eval = eager_eval; Interp.track_values = tracking_values; Interp.track_lmem = false; Interp.debug = debug; Interp.debug_indent = "" |>;; let make_mode eager_eval tracking_values debug = <| internal_mode = make_interpreter_mode eager_eval tracking_values debug |>;; let make_mode_exhaustive debug = <| internal_mode = <| Interp.eager_eval = true; Interp.track_values = true; Interp.track_lmem = true; Interp.debug = debug; Interp.debug_indent = "" |> |>;; let tracking_dependencies mode = mode.internal_mode.Interp.track_values let make_eager_mode mode = <| internal_mode = <| mode.internal_mode with Interp.eager_eval = true |> |>;; let make_default_mode = fun () -> <| internal_mode = make_interpreter_mode false false false |>;; let bitl_to_ibit = function | Bitl_zero -> (Interp_ast.V_lit (L_aux L_zero Interp_ast.Unknown)) | Bitl_one -> (Interp_ast.V_lit (L_aux L_one Interp_ast.Unknown)) | Bitl_undef -> (Interp_ast.V_lit (L_aux L_undef Interp_ast.Unknown)) | Bitl_unknown -> Interp_ast.V_unknown end let bit_to_ibit = function | Bitc_zero -> (Interp_ast.V_lit (L_aux L_zero Interp_ast.Unknown)) | Bitc_one -> (Interp_ast.V_lit (L_aux L_one Interp_ast.Unknown)) end let to_bool = function | Bitl_zero -> false | Bitl_one -> true | Bitl_undef -> Assert_extra.failwith "to_bool given undef" | Bitl_unknown -> Assert_extra.failwith "to_bool given unknown" end let is_bool = function | Bitl_zero -> true | Bitl_one -> true | Bitl_undef -> false | Bitl_unknown -> false end let bitl_from_ibit b = let b = Interp.detaint b in match b with | Interp_ast.V_lit (L_aux L_zero _) -> Bitl_zero | Interp_ast.V_vector _ _ [Interp_ast.V_lit (L_aux L_zero _)] -> Bitl_zero | Interp_ast.V_lit (L_aux L_one _) -> Bitl_one | Interp_ast.V_vector _ _ [Interp_ast.V_lit (L_aux L_one _)] -> Bitl_one | Interp_ast.V_lit (L_aux L_undef _) -> Bitl_undef | Interp_ast.V_vector _ _ [Interp_ast.V_lit (L_aux L_undef _)] -> Bitl_undef | Interp_ast.V_unknown -> Bitl_unknown | _ -> Assert_extra.failwith ("bit_from_ibit given unexpected " ^ (Interp.string_of_value b)) end let bits_to_ibits l = List.map bit_to_ibit l let bitls_to_ibits l = List.map bitl_to_ibit l let bitls_from_ibits l = List.map bitl_from_ibit l let bits_from_ibits l = List.map (fun b -> let b = Interp.detaint b in match b with | Interp_ast.V_lit (L_aux L_zero _) -> Bitc_zero | Interp_ast.V_vector _ _ [Interp_ast.V_lit (L_aux L_zero _)] -> Bitc_zero | Interp_ast.V_lit (L_aux L_one _) -> Bitc_one | Interp_ast.V_vector _ _ [Interp_ast.V_lit (L_aux L_one _)] -> Bitc_one | _ -> Assert_extra.failwith ("bits_from_ibits given unexpected " ^ (Interp.string_of_value b)) end) l let rec to_bytes l = match l with | [] -> [] | (a::b::c::d::e::f::g::h::rest) -> (Byte_lifted[a;b;c;d;e;f;g;h])::(to_bytes rest) | _ -> Assert_extra.failwith "to_bytes given list of bits not divisible by 8" end let all_known l = List.all is_bool l let all_known_bytes l = List.all (fun (Byte_lifted bs) -> List.all is_bool bs) l let bits_to_word8 b = if ((List.length b) = 8) && (all_known b) then natFromInteger (integerFromBoolList (false,(List.reverse (List.map to_bool b)))) else Assert_extra.failwith "bits_to_word8 given a non-8 list or one containing ? and u" let intern_direction = function | D_increasing -> Interp_ast.IInc | D_decreasing -> Interp_ast.IDec end let extern_direction = function | Interp_ast.IInc -> D_increasing | Interp_ast.IDec -> D_decreasing end let intern_opcode direction (Opcode v) = let bits = List.concatMap (fun (Byte(bits)) -> (List.map bit_to_ibit bits)) v in let direction = intern_direction direction in Interp_ast.V_vector (if Interp.is_inc(direction) then 0 else (List.length(bits) - 1)) direction bits let intern_reg_value v = match v with | <| rv_bits=[b] |> -> bitl_to_ibit b | _ -> Interp_ast.V_vector v.rv_start_internal (intern_direction v.rv_dir) (bitls_to_ibits v.rv_bits) end let intern_mem_value mode direction v = List.reverse v (* match little endian representation *) $> List.concatMap (fun (Byte_lifted bits) -> bitls_to_ibits bits) $> fun bits -> let direction = intern_direction direction in Interp_ast.V_vector (if Interp.is_inc direction then 0 else (List.length bits) -1) direction bits let intern_ifield_value direction v = let bits = bits_to_ibits v in let direction = intern_direction direction in Interp_ast.V_vector (if Interp.is_inc direction then 0 else (List.length(bits) -1)) direction bits let extern_slice (d:direction) (start:nat) ((i,j):(nat*nat)) = match d with | D_increasing -> (i,j) (*This is the case the thread/concurrecny model expects, so no change needed*) | D_decreasing -> let slice_i = start - i in let slice_j = (i - j) + slice_i in (slice_i,slice_j) end let extern_reg r slice = match (r,slice) with | (Interp_ast.Form_Reg (Id_aux (Id x) _) (Just(t,_,_,_,_)) dir,Nothing) -> Reg x (Interp.reg_start_pos r) (Interp.reg_size r) (extern_direction dir) | (Interp_ast.Form_Reg (Id_aux (Id x) _) (Just(t,_,_,_,_)) dir,Just(i1,i2)) -> let start = Interp.reg_start_pos r in let edir = extern_direction dir in Reg_slice x start edir (extern_slice edir start (i1, i2)) | (Interp_ast.Form_SubReg (Id_aux (Id x) _) ((Interp_ast.Form_Reg (Id_aux (Id y) _) _ dir) as main_r) (BF_aux(BF_single i) _), Nothing) -> let i = natFromInteger i in let start = Interp.reg_start_pos main_r in let edir = extern_direction dir in Reg_field y start edir x (extern_slice edir start (i,i)) | (Interp_ast.Form_SubReg (Id_aux (Id x) _) ((Interp_ast.Form_Reg (Id_aux (Id y) _) _ dir) as main_r) (BF_aux(BF_range i j) _), Nothing) -> let start = Interp.reg_start_pos main_r in let edir = extern_direction dir in Reg_field y start edir x (extern_slice edir start (natFromInteger i,natFromInteger j)) | (Interp_ast.Form_SubReg (Id_aux (Id x) _) ((Interp_ast.Form_Reg (Id_aux (Id y) _) _ dir) as main_r) (BF_aux(BF_range i j) _), Just(i1,j1)) -> let start = Interp.reg_start_pos main_r in let edir = extern_direction dir in Reg_f_slice y start edir x (extern_slice edir start (natFromInteger i,natFromInteger j)) (extern_slice edir start (i1, j1)) | _ -> Assert_extra.failwith "extern_reg given non-externable reg" end let rec extern_reg_value reg_name v = match v with | Interp_ast.V_track v regs -> extern_reg_value reg_name v | Interp_ast.V_vector_sparse fst stop inc bits default -> extern_reg_value reg_name (Interp_lib.fill_in_sparse v) | _ -> let (internal_start, external_start, direction) = (match reg_name with | Reg _ start size dir -> (start, (if dir = D_increasing then start else (start - (size +1))), dir) | Reg_slice _ reg_start dir (slice_start, slice_end) -> ((if dir = D_increasing then slice_start else (reg_start - slice_start)), slice_start, dir) | Reg_field _ reg_start dir _ (slice_start, slice_end) -> ((if dir = D_increasing then slice_start else (reg_start - slice_start)), slice_start, dir) | Reg_f_slice _ reg_start dir _ _ (slice_start, slice_end) -> ((if dir = D_increasing then slice_start else (reg_start - slice_start)), slice_start, dir) end) in let bit_list = (match v with | Interp_ast.V_vector fst dir bits -> bitls_from_ibits bits | Interp_ast.V_lit (L_aux L_zero _) -> [Bitl_zero] | Interp_ast.V_lit (L_aux L_false _) -> [Bitl_zero] | Interp_ast.V_lit (L_aux L_one _) -> [Bitl_one] | Interp_ast.V_lit (L_aux L_true _) -> [Bitl_one] | Interp_ast.V_lit (L_aux L_undef _) -> [Bitl_undef] | Interp_ast.V_unknown -> [Bitl_unknown] | _ -> Assert_extra.failwith ("extern_reg_val given non externable value " ^ (Interp.string_of_value v)) end) in <| rv_bits=bit_list; rv_dir=direction; rv_start=external_start; rv_start_internal = internal_start |> end let extern_with_track mode f = function | Interp_ast.V_track v regs -> (f v, if mode.internal_mode.Interp.track_values then (Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList regs))) else Nothing) | v -> (f v, Nothing) end let rec extern_vector_value v = match v with | Interp_ast.V_vector _fst _inc bits -> bitls_from_ibits bits $> to_bytes | Interp_ast.V_vector_sparse _fst _stop _inc _bits _default -> Interp_lib.fill_in_sparse v $> extern_vector_value | Interp_ast.V_track v _ -> extern_vector_value v | _ -> Assert_extra.failwith ("extern_vector_value received non-externable value " ^ (Interp.string_of_value v)) end let rec extern_mem_value v = List.reverse (extern_vector_value v) let rec extern_ifield_value i_name field_name v ftyp = match (v,ftyp) with | (Interp_ast.V_track v regs,_) -> extern_ifield_value i_name field_name v ftyp | (Interp_ast.V_vector fst inc bits,_) -> bits_from_ibits bits | (Interp_ast.V_vector_sparse fst stop inc bits default,_) -> extern_ifield_value i_name field_name (Interp_lib.fill_in_sparse v) ftyp | (Interp_ast.V_lit (L_aux L_zero _),_) -> [Bitc_zero] | (Interp_ast.V_lit (L_aux L_false _),_) -> [Bitc_zero] | (Interp_ast.V_lit (L_aux L_one _),_) -> [Bitc_one] | (Interp_ast.V_lit (L_aux L_true _),_) -> [Bitc_one] | (Interp_ast.V_lit (L_aux (L_num i) _),Range (Just n)) -> bit_list_of_integer n i | (Interp_ast.V_lit (L_aux (L_num i) _),Enum _ n) -> bit_list_of_integer n i | (Interp_ast.V_lit (L_aux (L_num i) _),_) -> bit_list_of_integer 64 i | (Interp_ast.V_ctor _ _ (Interp_ast.C_Enum i) _,Enum _ n) -> bit_list_of_integer n (integerFromNat i) | (Interp_ast.V_ctor _ _ (Interp_ast.C_Enum i) _,_) -> bit_list_of_integer 64 (integerFromNat i) | _ -> Assert_extra.failwith ("extern_ifield_value of " ^ i_name ^ " for field " ^ field_name ^ " given non-externable " ^ (Interp.string_of_value v) ^ " ftyp is " ^ show ftyp) end let rec slice_reg_value v start stop = (* let _ = Interp.debug_print ("slice_reg_value " ^ show v.rv_start_internal ^ " " ^ show v.rv_start ^ " " ^ show start ^ " " ^ show stop) in*) let inc = v.rv_dir = D_increasing in let r_internal_start = if inc then start else (stop - start) + 1 in let r_start = if inc then r_internal_start else start in (* let _ = Interp.debug_print (" " ^ " " ^ if inc then "Inc " else "dec " ^ show (List.length (Interp.from_n_to_n (if inc then (start - v.rv_start_internal) else (v.rv_start_internal - start)) (if inc then (stop - v.rv_start_internal) else (v.rv_start_internal - stop)) v.rv_bits)) ^ " " ^ show (List.length v.rv_bits) ^ " " ^ show (v.rv_start_internal - start) ^ " " ^ show (v.rv_start_internal - stop) ^ "\n") in*) <| v with rv_bits = (Interp.from_n_to_n (start - v.rv_start) (stop - v.rv_start) v.rv_bits); rv_start = r_start; rv_start_internal = r_internal_start |> let lift_reg_name_to_whole reg_name size = match reg_name with | Reg _ _ _ _ -> reg_name | Reg_slice name start dir _ -> Reg name start size dir | Reg_field name start dir _ _ -> Reg name start size dir | Reg_f_slice name start dir _ _ _ -> Reg name start size dir end let update_reg_value_slice reg_name v start stop v2 = let v_internal = intern_reg_value v in let v2_internal = intern_reg_value v2 in <| (extern_reg_value (lift_reg_name_to_whole reg_name 0) (if start = stop then (Interp.fupdate_vec v_internal start v2_internal) else (Interp.fupdate_vector_slice v_internal v2_internal start stop))) with rv_start = v.rv_start; rv_start_internal = v.rv_start_internal |> (*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 _ _ _) -> (* let _ = Interp.debug_print ("find_reg_name " ^ i ^ " field case " ^ show p1 ^ " " ^ show p2 ^ "\n") in*) 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)] | [arg] -> let (e,_) = Interp.to_exp (make_interpreter_mode true false) Interp.eenv (intern_reg_value arg) in [e] | args -> List.map fst (List.map (Interp.to_exp (make_interpreter_mode true false) Interp.eenv) (List.map intern_reg_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 "istate top level") Interp.Top type interp_value_helper_mode = Ivh_translate | Ivh_decode | Ivh_unsupported | Ivh_illegal | Ivh_analysis type interp_value_return = | Ivh_value of Interp_ast.value | Ivh_value_after_exn of Interp_ast.value | Ivh_error of decode_error let rec interp_to_value_helper debug arg ivh_mode err_str instr direction registers events exn_seen thunk = let errk_str = match ivh_mode with | Ivh_translate -> "translate" | Ivh_analysis -> "analysis" | Ivh_decode -> "decode" | Ivh_unsupported -> "supported_instructions" | Ivh_illegal -> "illegal instruction" end in let events_out = match events with [] -> Nothing | _ -> Just events end in let mode = (make_interpreter_mode true false debug) in match thunk() with | (Interp.Value value,_,_) -> if exn_seen then (Ivh_value_after_exn value, events_out) else (match ivh_mode with | Ivh_translate -> (Ivh_value value, events_out) | Ivh_analysis -> (Ivh_value value, events_out) | _ -> (match value with | Interp_ast.V_ctor (Id_aux (Id "Some") _) _ _ vinstr -> (Ivh_value vinstr,events_out) | Interp_ast.V_ctor (Id_aux (Id "None") _) _ _ _ -> (match (ivh_mode,arg) with | (Ivh_decode, (Just arg)) -> (Ivh_error (Interp_interface.Not_an_instruction_error arg), events_out) | (Ivh_illegal, (Just arg)) -> (Ivh_error (Interp_interface.Not_an_instruction_error arg), events_out) | (Ivh_unsupported, _) -> (Ivh_error (Interp_interface.Unsupported_instruction_error instr), events_out) | _ -> Assert_extra.failwith "Reached unreachable pattern" end) | _ -> (Ivh_error (Interp_interface.Internal_error ("Value not an option for " ^ errk_str)), events_out) end) end) | (Interp.Error l msg,_,_) -> (Ivh_error (Interp_interface.Internal_error msg), events_out) | (Interp.Action (Interp.Return value) stack,_,_) -> interp_to_value_helper debug arg ivh_mode err_str instr direction registers events exn_seen (fun _ -> Interp.resume mode stack (Just value)) | (Interp.Action (Interp.Call_extern i value) stack,_,_) -> match List.lookup i (Interp_lib.library_functions direction) with | Nothing -> (Ivh_error (Interp_interface.Internal_error ("External function not available " ^ i)), events_out) | Just f -> interp_to_value_helper debug arg ivh_mode err_str instr direction registers events exn_seen (fun _ -> Interp.resume mode stack (Just (f value))) end | (Interp.Action (Interp.Fail v) stack, _, _) -> match (Interp.detaint v) with | Interp_ast.V_ctor (Id_aux (Id "Some") _) _ _ (Interp_ast.V_lit (L_aux (L_string s) _)) -> (Ivh_error (Interp_interface.Internal_error ("Assert failed: " ^ s)), events_out) | _ -> (Ivh_error (Interp_interface.Internal_error "Assert failed"), events_out) end | (Interp.Action (Interp.Exit exp) stack,_,_) -> interp_to_value_helper debug arg ivh_mode err_str instr direction registers events true (fun _ -> Interp.resume mode (Interp.set_in_context stack exp) Nothing) | (Interp.Action (Interp.Read_reg r slice) stack,_,_) -> let rname = match r with | Interp_ast.Form_Reg (Id_aux (Id i) _) _ _ -> i | Interp_ast.Form_SubReg (Id_aux (Id i) _) (Interp_ast.Form_Reg (Id_aux (Id i2) _) _ _) _ -> i2 ^ "." ^ i | _ -> Assert_extra.failwith "Reg not following expected structure" end in let err_value = (Ivh_error (Interp_interface.Internal_error ("Register read of "^ rname^" request in a " ^ errk_str ^ " of " ^ err_str)), events_out) 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 (* let _ = Interp.debug_print ("Register read of " ^ rname ^ " returning value " ^ (Interp.string_of_value value) ^ "\n") in *) interp_to_value_helper debug arg ivh_mode err_str instr direction registers events exn_seen (fun _ -> Interp.resume mode stack (Just value)) end end) | (Interp.Action (Interp.Write_reg r slice value) stack,_,_) -> let ext_reg = extern_reg r slice in let reg_value = extern_reg_value ext_reg value in interp_to_value_helper debug arg ivh_mode err_str instr direction registers ((E_write_reg ext_reg reg_value)::events) exn_seen (fun _ -> Interp.resume mode stack Nothing) | (Interp.Action (Interp.Read_mem _ _ _) _,_,_) -> (Ivh_error (Interp_interface.Internal_error ("Read memory request in a " ^ errk_str)), events_out) | (Interp.Action (Interp.Read_mem_tagged _ _ _) _,_,_) -> (Ivh_error (Interp_interface.Internal_error ("Read memory tagged request in a " ^ errk_str)), events_out) | (Interp.Action (Interp.Write_mem _ _ _ _) _,_,_) -> (Ivh_error (Interp_interface.Internal_error ("Write memory request in a " ^ errk_str)), events_out) | (Interp.Action (Interp.Write_ea _ _) _,_,_) -> (Ivh_error (Interp_interface.Internal_error ("Write ea request in a " ^ errk_str)), events_out) | (Interp.Action (Interp.Excl_res _) _,_,_) -> (Ivh_error (Interp_interface.Internal_error ("Exclusive result request in a " ^ errk_str)), events_out) | (Interp.Action (Interp.Write_memv _ _ _) _,_,_) -> (Ivh_error (Interp_interface.Internal_error ("Write memory value request in a " ^ errk_str)), events_out) | (Interp.Action (Interp.Write_memv_tagged _ _ _ _) _,_,_) -> (Ivh_error (Interp_interface.Internal_error ("Write memory value tagged request in a " ^ errk_str)), events_out) | (outcome, _, _) -> (Ivh_error (Interp_interface.Internal_error ("Non expected action in a " ^ errk_str ^ " " ^ Interp.string_of_outcome outcome)), events_out) end let call_external_functions direction outcome = match outcome with | Interp.Action (Interp.Call_extern i value) stack -> match List.lookup i (Interp_lib.library_functions direction) with | Nothing -> Nothing | Just f -> Just (f value) end | _ -> Nothing end let build_context debug defs reads writes write_eas write_vals barriers excl_res externs = (*TODO add externs to to_top_env*) match Interp.to_top_env debug call_external_functions defs with | (_,((Interp.Env _ _ dir _ _ _ _ _ debug) as context)) -> Context context (if Interp.is_inc(dir) then D_increasing else D_decreasing) reads writes write_eas write_vals barriers excl_res externs end let translate_address top_level end_flag thunk_name registers address = let (Address bytes i) = address in let (Context top_env direction _ _ _ _ _ _ _ _ _) = top_level in let (Interp.Env _ _ _ _ _ _ _ _ debug) = top_env in let mode = make_mode true false debug in let int_mode = mode.internal_mode in let intern_val = intern_mem_value mode direction (memory_value_of_address end_flag address) in let val_str = Interp.string_of_value intern_val in let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in let (address_error,events) = interp_to_value_helper debug (Just (Opcode bytes)) Ivh_translate val_str (V_list []) internal_direction registers [] false (fun _ -> Interp.resume int_mode (Interp.Thunk_frame (E_aux (E_app (Id_aux (Id thunk_name) Interp_ast.Unknown) [arg]) (Interp_ast.Unknown, Nothing)) top_env Interp.eenv (Interp.emem "translate top level") Interp.Top) Nothing) in match (address_error) with | Ivh_value addr -> (address_of_byte_lifted_list (extern_vector_value addr), events) | Ivh_value_after_exn _ -> (Nothing, events) | Ivh_error err -> match err with | Interp_interface.Internal_error msg -> Assert_extra.failwith msg | _ -> Assert_extra.failwith "Not an internal error either" end end let value_of_instruction_param direction (name,typ,v) = let vec = intern_ifield_value direction v in let v = match vec with | Interp_ast.V_vector start dir bits -> match typ with | Bit -> match bits with | [b] -> b | _ -> Assert_extra.failwith "Expected a bitvector of length 1" end | Range _ -> Interp_lib.to_num Interp_lib.Unsigned vec | Enum _ _ -> Interp_lib.to_num Interp_lib.Unsigned vec | _ -> vec end | _ -> Assert_extra.failwith "intern_ifield did not return vector" end in v let intern_instruction direction (name,parms) = Interp_ast.V_ctor (Interp.id_of_string name) (mk_typ_id "ast") Interp_ast.C_Union (Interp_ast.V_tuple (List.map (value_of_instruction_param direction) parms)) let instruction_analysis top_level end_flag thunk_name regn_to_reg_details registers (instruction : Interp_ast.value) = let (Context top_env direction _ _ _ _ _ _ _ _ _) = top_level in let (Interp.Env _ _ _ _ _ _ _ _ debug) = top_env in let mode = make_mode true false debug in let int_mode = mode.internal_mode in let val_str = Interp.string_of_value instruction in let (arg,_) = Interp.to_exp int_mode Interp.eenv instruction in let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in let (analysis_or_error,events) = interp_to_value_helper debug Nothing Ivh_analysis val_str (V_list []) internal_direction registers [] false (fun _ -> Interp.resume int_mode (Interp.Thunk_frame (E_aux (E_app (Id_aux (Id thunk_name) Interp_ast.Unknown) [arg]) (Interp_ast.Unknown, Nothing)) top_env Interp.eenv (Interp.emem "instruction analysis top level") Interp.Top) Nothing) in match (analysis_or_error) with | Ivh_value analysis -> (match analysis with | Interp_ast.V_tuple [Interp_ast.V_list regs1; Interp_ast.V_list regs2; Interp_ast.V_list regs3; Interp_ast.V_list nias; dia; ik] -> let reg_to_reg_name v = match v with | Interp_ast.V_ctor (Id_aux (Id "RFull") _) _ _ (Interp_ast.V_lit (L_aux (L_string n) _)) -> let (start,length,direction,_) = regn_to_reg_details n Nothing in Reg n start length direction | Interp_ast.V_ctor (Id_aux (Id "RSlice") _) _ _ (Interp_ast.V_tuple [Interp_ast.V_lit (L_aux (L_string n) _); Interp_ast.V_lit (L_aux (L_num s1) _); Interp_ast.V_lit (L_aux (L_num s2) _);]) -> let (start,length,direction,_) = regn_to_reg_details n Nothing in Reg_slice n start direction (extern_slice direction start (natFromInteger s1, natFromInteger s2)) (*Note, this may need to change order depending on the direction*) | Interp_ast.V_ctor (Id_aux (Id "RSliceBit") _) _ _ (Interp_ast.V_tuple [Interp_ast.V_lit (L_aux (L_string n) _); Interp_ast.V_lit (L_aux (L_num s) _);]) -> let (start,length,direction,_) = regn_to_reg_details n Nothing in Reg_slice n start direction (extern_slice direction start (natFromInteger s,natFromInteger s)) | Interp_ast.V_ctor (Id_aux (Id "RField") _) _ _ (Interp_ast.V_tuple [Interp_ast.V_lit (L_aux (L_string n) _); Interp_ast.V_lit (L_aux (L_string f) _);]) -> let (start,length,direction,span) = regn_to_reg_details n (Just f) in Reg_field n start direction f (extern_slice direction start span) | _ -> Assert_extra.failwith "Register footprint analysis did not return an element of the specified type" end in let get_addr v = match address_of_byte_lifted_list (extern_vector_value v) with | Just addr -> addr | Nothing -> failwith "get_nia encountered invalid address" end in let dia_to_dia = function | Interp_ast.V_ctor (Id_aux (Id "DIAFP_none") _) _ _ _ -> DIA_none | Interp_ast.V_ctor (Id_aux (Id "DIAFP_concrete") _) _ _ address -> DIA_concrete_address (get_addr address) | Interp_ast.V_ctor (Id_aux (Id "DIAFP_reg") _) _ _ reg -> DIA_register (reg_to_reg_name reg) | _ -> failwith "Register footprint analysis did not return dia of expected type" end in let nia_to_nia = function | Interp_ast.V_ctor (Id_aux (Id "NIAFP_successor") _) _ _ _ -> NIA_successor | Interp_ast.V_ctor (Id_aux (Id "NIAFP_concrete_address") _) _ _ address -> NIA_concrete_address (get_addr address) | Interp_ast.V_ctor (Id_aux (Id "NIAFP_indirect_address") _) _ _ _ -> NIA_indirect_address | _ -> failwith "Register footprint analysis did not return nia of expected type" end in let (regs1,regs2,regs3,nias,dia,ik) = (List.map reg_to_reg_name regs1, List.map reg_to_reg_name regs2, List.map reg_to_reg_name regs3, List.map nia_to_nia nias, dia_to_dia dia, fromInterpValue ik) in ((regs1,regs2,regs3,nias,dia,ik), events) | _ -> Assert_extra.failwith "Analysis did not return a four-tuple of lists" end) | Ivh_value_after_exn _ -> Assert_extra.failwith "Instruction analysis failed" | Ivh_error err -> match err with | Interp_interface.Internal_error msg -> Assert_extra.failwith msg | _ -> Assert_extra.failwith "Not an internal error either" end end let rec find_instruction i = function | [] -> Nothing | Instruction_extractor.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.IRange len -> Range len | Instruction_extractor.IEnum s max -> Enum s max | Instruction_extractor.IOther -> Other end let interp_value_to_instr_external top_level instr = let (Context (Interp.Env _ instructions _ _ _ _ _ _ debug) _ _ _ _ _ _ _ _ _ _) = top_level in match instr with | Interp_ast.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_ast.V_lit (L_aux L_unit _),[]) -> (name, []) | (value,[(p_name,ie_typ)]) -> let t = migrate_typ ie_typ in (name, [(p_name,t, (extern_ifield_value name p_name value t))]) | (Interp_ast.V_tuple vals,parms) -> (name, (Interp_utilities.map2 (fun value (p_name,ie_typ) -> let t = migrate_typ ie_typ in (p_name,t,(extern_ifield_value name p_name value t))) vals parms)) | _ -> Assert_extra.failwith "decoded instruction doesn't match expectation" end | _ -> Assert_extra.failwith ("failed to find instruction " ^ i) end | _ -> Assert_extra.failwith "decoded instruction not a constructor" end let decode_to_instruction top_level registers value : instruction_or_decode_error = let (Context ((Interp.Env _ instructions _ _ _ _ _ _ debug) as top_env) direction _ _ _ _ _ _ _ _ _) = top_level in let mode = make_interpreter_mode true false debug 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_ast.IInc else Interp_ast.IDec in let (instr_decoded_error,events) = interp_to_value_helper debug (Just value) Ivh_decode val_str (V_list []) internal_direction registers [] false (fun _ -> Interp.resume mode (Interp.Thunk_frame (E_aux (E_app (Id_aux (Id "decode") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown, Nothing)) top_env Interp.eenv (Interp.emem "decode top level") Interp.Top) Nothing) in match (instr_decoded_error) with | Ivh_value instr -> (* let instr_external = interp_value_to_instr_external top_level instr in*) let (instr_decoded_error,events) = interp_to_value_helper debug (Just value) Ivh_unsupported val_str instr (*instr_external*) internal_direction registers [] false (fun _ -> Interp.resume mode (Interp.Thunk_frame (E_aux (E_app (Id_aux (Id "supported_instructions") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown, Nothing)) top_env Interp.eenv (Interp.emem "decode second top level") Interp.Top) Nothing) in match (instr_decoded_error) with | Ivh_value _ -> IDE_instr instr (*instr_external*) | Ivh_value_after_exn v -> Assert_extra.failwith "supported_instructions called exit, so support will be needed for that now" | Ivh_error err -> IDE_decode_error err end | Ivh_value_after_exn _ -> Assert_extra.failwith ("Decode of " ^ val_str ^ " called exit.") | Ivh_error err -> IDE_decode_error err end let decode_to_istate (top_level:context) registers (value:opcode) : i_state_or_error = let (Context top_env _ _ _ _ _ _ _ _ _ _) = top_level in match decode_to_instruction top_level registers value with | IDE_instr instr -> let mode = make_interpreter_mode true false in let (arg,_) = Interp.to_exp mode Interp.eenv instr in Instr instr (IState (Interp.Thunk_frame (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown,Nothing)) top_env Interp.eenv (Interp.emem "execute") Interp.Top) top_level) | IDE_decode_error de -> Decode_error de end let instr_external_to_interp_value top_level instr = let (Context _ direction _ _ _ _ _ _ _ _ _) = top_level in let (name,parms) = instr in let get_value (_,typ,v) = let vec = intern_ifield_value direction v in match vec with | Interp_ast.V_vector start dir bits -> match typ with | Bit -> match bits with | [b] -> b | _ -> Assert_extra.failwith "Expected a bitvector of length 1" end | Range _ -> Interp_lib.to_num Interp_lib.Unsigned vec | Enum _ _ -> Interp_lib.to_num Interp_lib.Unsigned vec | _ -> vec end | _ -> Assert_extra.failwith "intern_ifield did not return vector" end in let parmsV = match parms with | [] -> Interp_ast.V_lit (L_aux L_unit Unknown) | _ -> Interp_ast.V_tuple (List.map get_value parms) end in (*This type shouldn't be hard-coded*) Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id name) Interp_ast.Unknown) (mk_typ_id "ast") Interp_ast.C_Union parmsV val instruction_to_istate : context -> Interp_ast.value -> instruction_state let instruction_to_istate (top_level:context) (instr:Interp_ast.value) : instruction_state = let mode = make_interpreter_mode true false in let (Context top_env _ _ _ _ _ _ _ _ _ _) = top_level in let ast_node = fst (Interp.to_exp mode Interp.eenv instr) in (IState (Interp.Thunk_frame (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [ast_node]) (Interp_ast.Unknown,Nothing)) top_env Interp.eenv (Interp.emem "execute") Interp.Top) top_level) let rec interp_to_outcome mode context thunk = let (Context _ direction mem_reads mem_reads_tagged mem_writes mem_write_eas mem_write_vals mem_write_vals_tagged barriers excl_res spec_externs) = context in let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in match thunk () with | (Interp.Value _,lm,le) -> (Done,lm) | (Interp.Error l msg,lm,le) -> (Error msg,lm) | (Interp.Action a next_state,lm,le) -> (match a with | Interp.Read_reg reg_form slice -> (Read_reg (extern_reg reg_form slice) (fun v -> let v = (intern_reg_value v) in let v = if mode.internal_mode.Interp.track_values then (Interp_ast.V_track v (Set.fromList [reg_form])) else v in IState (Interp.add_answer_to_stack next_state v) context), lm) | Interp.Write_reg reg_form slice value -> let reg_name = extern_reg reg_form slice in (Write_reg reg_name (extern_reg_value reg_name value) (IState next_state context),lm) | Interp.Read_mem (Id_aux (Id i) _) value slice -> (match List.lookup i mem_reads with | (Just (MR read_k f)) -> let (location, length, tracking) = (f mode value) in if (List.length location) = 8 then let address_int = match (maybe_all (List.map byte_of_byte_lifted location)) with | Just bs -> Just (integer_of_byte_list bs) | _ -> Nothing end in Read_mem read_k (Address_lifted location address_int) length tracking (fun v -> IState (Interp.add_answer_to_stack next_state (intern_mem_value mode direction v)) context) else Error ("Memory address on read is not 64 bits") | _ -> Error ("Memory function " ^ i ^ " not found") end , lm) | Interp.Read_mem_tagged (Id_aux (Id i) _) value slice -> (match List.lookup i mem_reads_tagged with | (Just (MRT read_k f)) -> let (location, length, tracking) = (f mode value) in if (List.length location) = 8 then let address_int = match (maybe_all (List.map byte_of_byte_lifted location)) with | Just bs -> Just (integer_of_byte_list bs) | _ -> Nothing end in Read_mem_tagged read_k (Address_lifted location address_int) length tracking (fun (tag, v) -> IState (Interp.add_answer_to_stack next_state (Interp_ast.V_tuple ([(bitl_to_ibit tag);(intern_mem_value mode direction v)]))) context) else Error ("Memory address on read is not 64 bits") | _ -> Error ("Memory function " ^ i ^ " not found") end , lm) | Interp.Write_mem (Id_aux (Id i) _) loc_val slice write_val -> (match List.lookup i mem_writes with | (Just (MW write_k f return)) -> let (location, length, tracking) = (f mode loc_val) in let (value, v_tracking) = extern_with_track mode extern_mem_value write_val in if (List.length location) = 8 then let address_int = match (maybe_all (List.map byte_of_byte_lifted location)) with | Just bs -> Just (integer_of_byte_list bs) | _ -> Nothing end in Write_mem write_k (Address_lifted location address_int) length tracking value v_tracking (fun b -> match return with | Nothing -> (IState (Interp.add_answer_to_stack next_state Interp.unitv) context) | Just return_bool -> return_bool (IState next_state context) b end) else Error "Memory address on write is not 64 bits" | _ -> Error ("Memory function " ^ i ^ " not found") end , lm) | Interp.Write_ea (Id_aux (Id i) _) loc_val -> (match List.lookup i mem_write_eas with | (Just (MEA write_k f)) -> let (location, length, tracking) = (f mode loc_val) in if (List.length location) = 8 then let address_int = match (maybe_all (List.map byte_of_byte_lifted location)) with | Just bs -> Just (integer_of_byte_list bs) | _ -> Nothing end in Write_ea write_k (Address_lifted location address_int) length tracking (IState next_state context) else Error "Memory address for write is not 64 bits" | _ -> Error ("Memory function " ^ i ^ " to signal impending write, not found") end, lm) | Interp.Excl_res (Id_aux (Id i) _) -> (match excl_res with | (Just (i', ER return)) -> Excl_res (fun b -> match return with | Nothing -> (IState (Interp.add_answer_to_stack next_state Interp.unitv) context) | Just return_bool -> return_bool (IState next_state context) b end) | _ -> Error ("Exclusive result function, not provided") end, lm) | Interp.Write_memv (Id_aux (Id i) _) address_val write_val -> (match List.lookup i mem_write_vals with | (Just (MV parmf return)) -> let (value, v_tracking) = match (Interp.detaint write_val) with | Interp_ast.V_tuple[_;v] -> extern_with_track mode extern_mem_value (Interp.retaint write_val v) | _ -> extern_with_track mode extern_mem_value write_val end in let location_opt = match parmf mode address_val with | Nothing -> Nothing | Just mv -> let address_int = match (maybe_all (List.map byte_of_byte_lifted mv)) with | Just bs -> Just (integer_of_byte_list bs) | _ -> Nothing end in Just (Address_lifted mv address_int) end in Write_memv location_opt value v_tracking (fun b -> match return with | Nothing -> (IState (Interp.add_answer_to_stack next_state Interp.unitv) context) | Just return_bool -> return_bool (IState next_state context) b end) | _ -> Error ("Memory function " ^ i ^ " not found") end, lm) | Interp.Write_memv_tagged (Id_aux (Id i) _) address_val tag_val write_val -> (match List.lookup i mem_write_vals_tagged with | (Just (MVT parmf return)) -> let (value, v_tracking) = match (Interp.detaint write_val) with | Interp_ast.V_tuple[_;v] -> extern_with_track mode extern_mem_value (Interp.retaint write_val v) | _ -> extern_with_track mode extern_mem_value write_val end in let location_opt = match parmf mode address_val with | Nothing -> Nothing | Just mv -> let address_int = match (maybe_all (List.map byte_of_byte_lifted mv)) with | Just bs -> Just (integer_of_byte_list bs) | _ -> Nothing end in Just (Address_lifted mv address_int) end in Write_memv_tagged location_opt ((bitl_from_ibit tag_val), value) v_tracking (fun b -> match return with | Nothing -> (IState (Interp.add_answer_to_stack next_state Interp.unitv) context) | Just return_bool -> return_bool (IState next_state context) b end) | _ -> Error ("Memory function " ^ i ^ " not found") end, lm) | Interp.Barrier (Id_aux (Id i) _) lval -> (match List.lookup i barriers with | Just barrier -> Barrier barrier (IState next_state context) | _ -> Error ("Barrier " ^ i ^ " function not found") end, lm) | Interp.Footprint (Id_aux (Id i) _) lval -> (Footprint (IState next_state context), lm) | Interp.Nondet exps tag -> (match tag with | Tag_unknown _ -> let possible_states = List.map (Interp.set_in_context next_state) exps in let cleared_possibles = List.map Interp.clear_stack_state possible_states in Analysis_non_det (List.map (fun i -> IState i context) cleared_possibles) (IState next_state context) | _ -> let nondet_states = List.map (Interp.set_in_context next_state) exps in Nondet_choice (List.map (fun i -> IState i context) nondet_states) (IState next_state context) end, lm) | Interp.Call_extern i value -> (match List.lookup i ((Interp_lib.library_functions internal_direction) ++ spec_externs) with | Nothing -> (Error ("External function not available " ^ i), lm) | Just f -> if (mode.internal_mode.Interp.eager_eval) then interp_to_outcome mode context (fun _ -> Interp.resume mode.internal_mode next_state (Just (f value))) else let new_v = f value in (Internal (Just i) (Just (fun _ -> (Interp.string_of_value value) ^ "=>" ^ (Interp.string_of_value new_v))) (IState (Interp.add_answer_to_stack next_state new_v) context), lm) end) | Interp.Return value -> interp_to_outcome mode context (fun _ -> Interp.resume mode.internal_mode next_state (Just value)) | Interp.Step l Nothing Nothing -> (Internal Nothing Nothing (IState next_state context), lm) | Interp.Step l (Just name) Nothing -> (Internal (Just name) Nothing (IState next_state context), lm) | Interp.Step l (Just name) (Just value) -> (Internal (Just name) (Just (fun _ -> Interp.string_of_value value)) (IState next_state context), lm) | Interp.Fail value -> (match value with | Interp_ast.V_ctor (Id_aux (Id "Some") _) _ _ (Interp_ast.V_lit (L_aux (L_string s) _)) -> (Fail (Just s),lm) | _ -> (Fail Nothing,lm) end) | Interp.Exit e -> (Escape (match e with | E_aux (E_lit (L_aux L_unit _)) _ -> Nothing | _ -> Just (IState (Interp.set_in_context next_state e) context) end) (IState next_state context), (snd (Interp.get_stack_state next_state))) | _ -> Assert_extra.failwith "Action not as expected: consider if a deiid could have appeared" end ) end (*Update slice potentially here*) let reg_size = function | Reg i _ size _ -> size | Reg_slice i _ _ (p1,p2) -> if p1 < p2 then (p2-p1 +1) else (p1-p2 +1) | Reg_field i _ _ f (p1,p2) -> if p1 < p2 then (p2-p1 +1) else (p1-p2 +1) | Reg_f_slice i _ _ f _ (p1,p2) -> if p1 < p2 then p2-p1 +1 else p1-p2+1 end let interp mode (IState interp_state context) = match interp_to_outcome mode context (fun _ -> Interp.resume mode.internal_mode interp_state Nothing) with | (o,_) -> o end (*ie_loop returns a tuple of event list, and a tuple ofinternal interpreter memory, bool to indicate normal or exceptional termination*) let rec ie_loop mode register_values (IState interp_state context) = let (Context _ direction externs reads reads_tagged writes write_eas write_vals write_vals_tagged barriers excl_res) = context in let unknown_reg size = <| rv_bits = (List.replicate size Bitl_unknown); rv_start = 0; rv_start_internal = (if direction = D_increasing then 0 else (size-1)); rv_dir = direction |> in let unknown_mem size = List.replicate size (Byte_lifted (List.replicate 8 Bitl_unknown)) in match interp_to_outcome mode context (fun _ -> Interp.resume mode.internal_mode interp_state Nothing) with | (Done,lm) -> ([],(lm,true)) | (Error msg,lm) -> ([E_error msg],(lm,false)) | (Escape Nothing i_state,lm) -> ([E_escape],(lm,false)) (*Do we want to record anything about the escape expression, which may be a function call*) | (Escape _ i_state,lm) -> ([E_escape],(lm,false)) | (Fail _,lm) -> ([E_escape],(lm,false)) | (Read_reg reg i_state_fun,_) -> let v = (match register_values with | Nothing -> unknown_reg (reg_size reg) | Just(registers) -> match find_reg_name reg registers with | Nothing -> unknown_reg (reg_size reg) | Just v -> v end end) in let (events,analysis_data) = ie_loop mode register_values (i_state_fun v) in ((E_read_reg reg)::events,analysis_data) | (Write_reg reg value i_state, _)-> let (events,analysis_data) = ie_loop mode register_values i_state in ((E_write_reg reg value)::events,analysis_data) | (Read_mem read_k loc length tracking i_state_fun, _) -> let (events,analysis_data) = ie_loop mode register_values (i_state_fun (unknown_mem length)) in ((E_read_mem read_k loc length tracking)::events,analysis_data) | (Read_mem_tagged read_k loc length tracking i_state_fun, _) -> let (events,analysis_data) = ie_loop mode register_values (i_state_fun (Bitl_unknown, (unknown_mem length))) in ((E_read_memt read_k loc length tracking)::events,analysis_data) | (Write_mem write_k loc length tracking value v_tracking i_state_fun, _) -> let (events,analysis_data) = ie_loop mode register_values (i_state_fun true) in let (events',analysis_data) = ie_loop mode register_values (i_state_fun false) in (*TODO: consider if lm and lm should be distinct and merged*) ((E_write_mem write_k loc length tracking value v_tracking)::(events++events'),analysis_data) | (Write_ea write_k loc length tracking i_state, _) -> let (events,analysis_data) = ie_loop mode register_values i_state in ((E_write_ea write_k loc length tracking)::events,analysis_data) | (Excl_res i_state_fun, _) -> let (events,analysis_data) = ie_loop mode register_values (i_state_fun true) in let (events',analysis_data) = ie_loop mode register_values (i_state_fun false) in (*TODO: consider if lm and lm should be merged*) (E_excl_res :: (events ++ events'), analysis_data) | (Write_memv opt_address value tracking i_state_fun, _) -> let (events,analysis_data) = ie_loop mode register_values (i_state_fun true) in let (events',analysis_data) = ie_loop mode register_values (i_state_fun false) in (*TODO: consider if lm and lm should be merged*) ((E_write_memv opt_address value tracking)::(events++events'),analysis_data) | (Write_memv_tagged opt_address value tracking i_state_fun, _) -> let (events,analysis_data) = ie_loop mode register_values (i_state_fun true) in let (events',analysis_data) = ie_loop mode register_values (i_state_fun false) in (*TODO: consider if lm and lm should be merged*) ((E_write_memvt opt_address value tracking)::(events++events'),analysis_data) | (Barrier barrier_k i_state, _) -> let (events,analysis_data) = ie_loop mode register_values i_state in ((E_barrier barrier_k)::events,analysis_data) | (Footprint i_state, _) -> let (events,analysis_data) = ie_loop mode register_values i_state in (E_footprint::events,analysis_data) | (Internal _ _ next, _) -> (ie_loop mode register_values next) | (Analysis_non_det possible_istates i_state,_) -> if possible_istates = [] then ie_loop mode register_values i_state else let (possible_events,possible_states) = List.unzip(List.map (ie_loop mode register_values) possible_istates) in let (unified_mem,update_mem) = List.foldr (fun (lm,terminated_normally) (mem,update_mem) -> if terminated_normally && update_mem then (Interp.merge_lmems lm mem, true) else if terminated_normally then (lm, true) else (mem, false)) (List_extra.head possible_states) (List_extra.tail possible_states) in let updated_i_state = if update_mem then match i_state with | (IState interp_state context) -> IState (Interp.update_stack_state interp_state unified_mem) context end else i_state in let (events,analysis_data) = ie_loop mode register_values updated_i_state in ((List.concat possible_events)++events, analysis_data) | _ -> Assert_extra.failwith "interp_to_outcome may have produced a nondet action" end ;; val interp_exhaustive : bool -> maybe (list (reg_name * register_value)) -> instruction_state -> list event let interp_exhaustive debug register_values i_state = let mode = make_mode_exhaustive debug in match ie_loop mode register_values i_state with | (events,_) -> events end val state_to_outcome_s : (instruction_state -> unit -> (string * string)) -> interp_mode -> instruction_state -> Sail_impl_base.outcome_s unit val outcome_to_outcome : (instruction_state -> unit -> (string * string)) -> interp_mode -> Interp_interface.outcome -> Sail_impl_base.outcome unit let rec outcome_to_outcome pp_instruction_state mode = let state_to_outcome_s = state_to_outcome_s pp_instruction_state in function | Interp_interface.Read_mem rk addr size _ k -> Sail_impl_base.Read_mem (rk,addr,size) (fun v -> state_to_outcome_s mode (k v)) | Interp_interface.Write_mem rk addr size _ mv _ k -> failwith "Write_mem not supported anymore" | Interp_interface.Write_ea wk addr size _ state -> Sail_impl_base.Write_ea (wk,addr,size) (state_to_outcome_s mode state) | Interp_interface.Excl_res k -> Sail_impl_base.Excl_res (fun v -> state_to_outcome_s mode (k v)) | Interp_interface.Write_memv _ mv _ k -> Sail_impl_base.Write_memv mv (fun v -> state_to_outcome_s mode (k v)) | Interp_interface.Barrier bk state -> Sail_impl_base.Barrier bk (state_to_outcome_s mode state) | Interp_interface.Footprint state -> Sail_impl_base.Footprint (state_to_outcome_s mode state) | Interp_interface.Read_reg r k -> Sail_impl_base.Read_reg r (fun v -> state_to_outcome_s mode (k v)) | Interp_interface.Write_reg r rv state -> Sail_impl_base.Write_reg (r,rv) (state_to_outcome_s mode state) | Interp_interface.Nondet_choice _ _ -> failwith "Nondet_choice not supported yet" | Interp_interface.Escape _ _ -> Sail_impl_base.Escape Nothing | Interp_interface.Fail maybestring -> Sail_impl_base.Fail maybestring | Interp_interface.Internal maybestring maybeprint state -> Sail_impl_base.Internal (maybestring,maybeprint) (state_to_outcome_s mode state) | Interp_interface.Analysis_non_det _ _ -> failwith "Analysis_non_det outcome returned" | Interp_interface.Done -> Sail_impl_base.Done () | Interp_interface.Error message -> failwith ("Interpreter error: " ^ message) end and state_to_outcome_s pp_instruction_state mode state = let next_outcome' = interp mode state in let next_outcome = outcome_to_outcome pp_instruction_state mode next_outcome' in (next_outcome, Just ((pp_instruction_state state), (fun env -> interp_exhaustive mode.internal_mode.Interp.debug (Just env) state)) ) val initial_outcome_s_of_instruction : (instruction_state -> unit -> (string * string)) -> context -> interp_mode -> Interp_ast.value -> Sail_impl_base.outcome_s unit let initial_outcome_s_of_instruction pp_instruction_state context mode instruction = let state = instruction_to_istate context instruction in state_to_outcome_s pp_instruction_state mode state (*This code is no longer uptodate. If no one is using it, then we don't need to fix it If someone is using it, this will let me know*) (*let rec rr_ie_loop mode i_state = let (IState _ (Context _ direction _ _ _ _ _ _)) = i_state in let unknown_reg size = <| rv_bits = (List.replicate size Bitl_unknown); rv_start = 0; rv_start_internal = (if direction=D_increasing then 0 else (size-1)); rv_dir = direction |> in let unknown_mem size = List.replicate size (Byte_lifted (List.replicate 8 Bitl_unknown)) in match (interp mode i_state) with | Done -> ([],Done) | Error msg -> ([E_error msg], Error msg) | Read_reg reg i_state_fun -> ([], Read_reg reg i_state_fun) | Write_reg reg value i_state-> let (events,outcome) = (rr_ie_loop mode i_state) in (((E_write_reg reg value)::events), outcome) | Read_mem read_k loc length tracking i_state_fun -> let (events,outcome) = (rr_ie_loop mode (i_state_fun (unknown_mem length))) in (((E_read_mem read_k loc length tracking)::events),outcome) | 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 tracking value v_tracking)::events),outcome) | Barrier barrier_k i_state -> let (events,outcome) = (rr_ie_loop mode i_state) in (((E_barrier barrier_k)::events),outcome) | Internal _ _ next -> (rr_ie_loop mode next) end ;; let rr_interp_exhaustive mode i_state events = let (events',outcome) = rr_ie_loop mode i_state in ((events ++ events'),outcome) *) let instruction_kind_of_event nia_reg : event -> maybe instruction_kind = function (* this is a hack to avoid adding special events for AArch64 transactional-memory *) | E_read_reg (Reg "TMStartEffect" 63 64 D_decreasing) -> Just (IK_trans Transaction_start) | E_write_reg (Reg "TMAbortEffect" 63 64 D_decreasing) _ -> Just (IK_trans Transaction_abort) | E_barrier Barrier_TM_COMMIT -> Just (IK_trans Transaction_commit) | E_read_mem rk _ _ _ -> Just (IK_mem_read rk) | E_read_memt rk _ _ _ -> Just (IK_mem_read rk) | E_write_mem wk _ _ _ _ _ -> Just (IK_mem_write wk) | E_write_ea wk _ _ _ -> Just (IK_mem_write wk) | E_excl_res -> Nothing | E_write_memv _ _ _ -> Nothing | E_write_memvt _ _ _ -> Nothing | E_barrier bk -> Just (IK_barrier bk) | E_footprint -> Nothing | E_read_reg _ -> Nothing | E_write_reg reg _ -> if register_base_name reg = register_base_name nia_reg then Just IK_branch else Nothing | E_error s -> failwith ("instruction_kind_of_event error: "^s) | E_escape -> Nothing (*failwith ("instruction_kind_of_event escape")*) end (* TODO: how can we decide, looking only at the output of interp_exhaustive, that an instruction is a conditional branch? *) let regs_in_of_event : event -> list reg_name = function | E_read_mem _ _ _ _ -> [] | E_read_memt _ _ _ _ -> [] | E_write_mem _ _ _ _ _ _ -> [] | E_write_ea _ _ _ _ -> [] | E_excl_res -> [] | E_write_memv _ _ _ -> [] | E_write_memvt _ _ _ -> [] | E_barrier _ -> [] | E_footprint -> [] | E_read_reg r -> [r] | E_write_reg _ _ -> [] | E_error s -> failwith ("regs_in_of_event "^s) | E_escape -> [] (*failwith ("regs_in_of_event escape")*) end let regs_out_of_event : event -> list reg_name = function | E_read_mem _ _ _ _ -> [] | E_read_memt _ _ _ _ -> [] | E_write_mem _ _ _ _ _ _ -> [] | E_write_ea _ _ _ _ -> [] | E_excl_res -> [] | E_write_memv _ _ _ -> [] | E_write_memvt _ _ _ -> [] | E_barrier _ -> [] | E_footprint -> [] | E_read_reg _ -> [] | E_write_reg r _ -> [r] | E_error s -> failwith ("regs_out_of_event "^s) | E_escape -> [] (*failwith ("regs_out_of_event escape")*) end let regs_feeding_memory_access_address_of_event : event -> list reg_name = function | E_read_mem _ _ _ (Just rs) -> rs | E_read_mem _ _ _ None -> [] | E_read_memt _ _ _ (Just rs) -> rs | E_read_memt _ _ _ None -> [] | E_write_mem _ _ _ (Just rs) _ _ -> rs | E_write_mem _ _ _ None _ _ -> [] | E_write_ea wk _ _ (Just rs) -> rs | E_write_ea wk _ _ None -> [] | E_excl_res -> [] | E_write_memv _ _ _ -> [] | E_write_memvt _ _ _ -> [] | E_barrier bk -> [] | E_footprint -> [] | E_read_reg _ -> [] | E_write_reg _ _ -> [] | E_error s -> failwith ("regs_feeding_memory_access_address_of_event " ^ s) | E_escape -> [] (*failwith ("regs_feeding_memory_access_address_of_event escape")*) end let nia_address_of_event nia_reg (event: event) : maybe (maybe address) = (* return Nothing for unknown/undef *) match event with | E_write_reg reg reg_value -> if register_base_name reg = register_base_name nia_reg then let al = match address_lifted_of_register_value reg_value with | Just al -> al | Nothing -> failwith "nia_register_of_event: NIA read not 64 bits" end in Just (address_of_address_lifted al) else Nothing | _ -> Nothing end let interp_instruction_analysis top_level (interp_exhaustive : ((list (reg_name * register_value)) -> list event)) instruction nia_reg (nias_function : (list (maybe address) -> list nia)) ism environment = let es = interp_exhaustive environment in let regs_in = List.concatMap regs_in_of_event es in let regs_out = List.concatMap regs_out_of_event es in let regs_feeding_address = List.concatMap regs_feeding_memory_access_address_of_event es in let nia_address = List.mapMaybe (nia_address_of_event nia_reg) es in let nias = nias_function nia_address in let dia = DIA_none in (* FIX THIS! *) let inst_kind = match List.mapMaybe (instruction_kind_of_event nia_reg) es with | [] -> IK_simple | inst_kind :: [] -> inst_kind | inst_kind :: inst_kinds -> if forall (inst_kind' MEM inst_kinds). inst_kind' = inst_kind then inst_kind else if (forall (inst_kind' MEM (inst_kind :: inst_kinds)). match inst_kind' with | IK_mem_read _ -> true | IK_mem_write _ -> true | IK_mem_rmw _ -> false | IK_barrier _ -> false | IK_branch -> false | IK_trans _ -> false | IK_simple -> false end) then match List.partition (function IK_mem_read _ -> true | _ -> false end) (inst_kind :: inst_kinds) with | ((IK_mem_read r) :: rs, (IK_mem_write w) :: ws) -> let () = ensure (forall (r' MEM rs). r' = IK_mem_read r) "more than one kind of read" in let () = ensure (forall (w' MEM ws). w' = IK_mem_write w) "more than one kind of write" in IK_mem_rmw (r, w) | _ -> fail end (* the TSTART instruction can also be aborted so it will have two kinds of events *) else if (exists (inst_kind' MEM (inst_kind :: inst_kinds)). inst_kind' = IK_trans Transaction_start) && (forall (inst_kind' MEM (inst_kind :: inst_kinds)). inst_kind' = IK_trans Transaction_start || inst_kind' = IK_trans Transaction_abort) then IK_trans Transaction_start else failwith "multiple instruction kinds" end in (regs_in, regs_out, regs_feeding_address, nias, dia, inst_kind) let interp_handwritten_instruction_analysis context endianness instruction analysis_function reg_info environment = fst (instruction_analysis context endianness analysis_function reg_info (Just environment) instruction) val print_and_fail_of_inequal : forall 'a. Show 'a => (string -> unit) -> (instruction -> string) -> (string * 'a) -> (string * 'a) -> unit let print_and_fail_if_inequal (print_endline,instruction) (name1,xs1) (name2,xs2) = if xs1 = xs2 then () else let () = print_endline (name1^": "^show xs1) in let () = print_endline (name2^": "^show xs2) in failwith (name1^" and "^ name2^" inequal for instruction: \n" ^ Interp.string_of_value instruction) let interp_compare_analyses print_endline (non_pseudo_registers : set reg_name -> set reg_name) context endianness interp_exhaustive (instruction : Interp_ast.value) nia_reg (nias_function : (list (maybe address) -> list nia)) ism environment analysis_function reg_info = let (regs_in1,regs_out1,regs_feeding_address1,nias1,dia1,inst_kind1) = interp_instruction_analysis context interp_exhaustive instruction nia_reg nias_function ism environment in let (regs_in1S,regs_out1S,regs_feeding_address1S,nias1S) = (Set.fromList regs_in1, Set.fromList regs_out1, Set.fromList regs_feeding_address1, Set.fromList nias1) in let (regs_in1S,regs_out1S,regs_feeding_addres1S) = (non_pseudo_registers regs_in1S, non_pseudo_registers regs_out1S, non_pseudo_registers regs_feeding_address1S) in let (regs_in2,regs_out2,regs_feeding_address2,nias2,dia2,inst_kind2) = interp_handwritten_instruction_analysis context endianness instruction analysis_function reg_info environment in let (regs_in2S,regs_out2S,regs_feeding_address2S,nias2S) = (Set.fromList regs_in2, Set.fromList regs_out2, Set.fromList regs_feeding_address2, Set.fromList nias2) in let (regs_in2S,regs_out2S,regs_feeding_addres2S) = (non_pseudo_registers regs_in2S, non_pseudo_registers regs_out2S, non_pseudo_registers regs_feeding_address2S) in let aux = (print_endline,instruction) in let () = (print_and_fail_if_inequal aux) ("regs_in exhaustive",regs_in1S) ("regs_in hand",regs_in2S) in let () = (print_and_fail_if_inequal aux) ("regs_out exhaustive",regs_out1S) ("regs_out hand",regs_out2S) in let () = (print_and_fail_if_inequal aux) ("regs_feeding_address exhaustive",regs_feeding_address1S) ("regs_feeding_address hand",regs_feeding_address2S) in let () = (print_and_fail_if_inequal aux) ("nias exhaustive",nias1S) ("nias hand",nias2S) in let () = (print_and_fail_if_inequal aux) ("dia exhaustive",dia1) ("dia hand",dia2) in let () = (print_and_fail_if_inequal aux) ("inst_kind exhaustive",inst_kind1) ("inst_kind hand",inst_kind2) in (regs_in1,regs_out1,regs_feeding_address1,nias1,dia1,inst_kind1)