(*========================================================================*) (* Sail *) (* *) (* Copyright (c) 2013-2017 *) (* Kathyrn Gray *) (* Shaked Flur *) (* Stephen Kell *) (* Gabriel Kerneis *) (* Robert Norton-Wright *) (* Christopher Pulte *) (* Peter Sewell *) (* *) (* 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 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) | _ -> (Ivh_error (Interp_interface.Internal_error ("Non expected action in a " ^ errk_str)), 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 ("",[]) 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) (T_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 = 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_instruction direction instruction 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 (analysis_or_error,events) = interp_to_value_helper debug Nothing Ivh_analysis val_str ("",[]) 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_LR") _) _ _ _ -> NIA_LR | Interp_ast.V_ctor (Id_aux (Id "NIAFP_CTR") _) _ _ _ -> NIA_CTR | Interp_ast.V_ctor (Id_aux (Id "NIAFP_register") _) _ _ reg -> NIA_register (reg_to_reg_name reg) | _ -> failwith "Register footprint analysis did not return nia of expected type" end in let ik_to_ik = function | Interp_ast.V_ctor (Id_aux (Id "IK_barrier") _) _ _ (Interp_ast.V_ctor (Id_aux (Id b) _) _ _ _) -> IK_barrier (match b with | "Barrier_Sync" -> Barrier_Sync | "Barrier_LwSync" -> Barrier_LwSync | "Barrier_Eieio" -> Barrier_Eieio | "Barrier_Isync" -> Barrier_Isync | "Barrier_DMB" -> Barrier_DMB | "Barrier_DMB_ST" -> Barrier_DMB_ST | "Barrier_DMB_LD" -> Barrier_DMB_LD | "Barrier_DSB" -> Barrier_DSB | "Barrier_DSB_ST" -> Barrier_DSB_ST | "Barrier_DSB_LD" -> Barrier_DSB_LD | "Barrier_ISB" -> Barrier_ISB | "Barrier_MIPS_SYNC" -> Barrier_MIPS_SYNC end) | Interp_ast.V_ctor (Id_aux (Id "IK_mem_read") _) _ _ (Interp_ast.V_ctor (Id_aux (Id r) _) _ _ _) -> IK_mem_read (match r with | "Read_plain" -> Read_plain | "Read_reserve" -> Read_reserve | "Read_acquire" -> Read_acquire | "Read_exclusive" -> Read_exclusive | "Read_exclusive_acquire" -> Read_exclusive_acquire | "Read_stream" -> Read_stream end) | Interp_ast.V_ctor (Id_aux (Id "IK_mem_write") _) _ _ (Interp_ast.V_ctor (Id_aux (Id w) _) _ _ _) -> IK_mem_write (match w with | "Write_plain" -> Write_plain | "Write_conditional" -> Write_conditional | "Write_release" -> Write_release | "Write_exclusive" -> Write_exclusive | "Write_exclusive_release" -> Write_exclusive_release end) | Interp_ast.V_ctor (Id_aux (Id "IK_cond_branch") _) _ _ _ -> IK_cond_branch | Interp_ast.V_ctor (Id_aux (Id "IK_simple") _) _ _ _ -> IK_simple | _ -> failwith "Analysis returned unexpected instruction kind" 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, ik_to_ik 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 ("",[]) 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_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_external instr | 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 instrv -> let mode = make_interpreter_mode true false in let (arg,_) = Interp.to_exp mode Interp.eenv instrv 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) (T_id "ast") Interp_ast.C_Union parmsV val instruction_to_istate : context -> instruction -> instruction_state let instruction_to_istate (top_level:context) (((name, parms) as instr):instruction) : 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_external_to_interp_value top_level 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 -> instruction -> 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 : 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 _ _ -> 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 nias_of_instruction thread_ism (nia_address: list (maybe address)) (* Nothing for unknown/undef*) (regs_in: list reg_name) (instruction: instruction) : list nia = let (instruction_name, instruction_fields) = instruction in let unknown_nia_address = List.elem Nothing nia_address in let nias = [NIA_concrete_address addr | forall (addr MEM (List.mapMaybe id nia_address)) | true] in (* it's a fact of the Power2.06B instruction pseudocode that in the B and Bc cases there should be no Unknown values in nia_values, while in the Bclr and Bcctr cases nia_values will just be Unknown and the semantics should match the comments in the machineDefTypes definition of nia *) (* All our other analysis is on the pseudocode directly, which is arguably pleasingly robust. We could replace the nias pattern match on instruction_name with something in that style if the exhaustive interpreter announced register dependencies to register writes (easy) and if it could check the form of the register writes to LR and CTR matches the machineDefTypes nia definition *) match (thread_ism, instruction_name) with | ("PPCGEN_ism", "B") -> let () = ensure (not unknown_nia_address) "unexpected unknown/undefined address in nia_values 1" in nias | ("PPCGEN_ism", "Bc") -> let () = ensure (not unknown_nia_address) "unexpected unknown/undefined address in nia_values 2" in NIA_successor :: nias | ("PPCGEN_ism", "Bclr") -> [ NIA_successor; NIA_LR ] | ("PPCGEN_ism", "Bcctr") -> [ NIA_successor; NIA_CTR ] | ("PPCGEN_ism", "Sc") -> let () = ensure (not unknown_nia_address) "unexpected unknown/undefined address in nia_values 3" in match instruction_fields with | [(_, _, lev)] -> (* LEV field is 7 bits long, pad it with false at beginning *) if lev = [Bitc_zero;Bitc_one;Bitc_one;Bitc_one;Bitc_one;Bitc_one;Bitc_one] (* (Interp_inter_imp.integer_of_byte_list (Interp_inter_imp.to_bytes (false :: bl))) = 63 *) then [] else [NIA_successor] | _ -> [ NIA_successor ] end (* AARch64 label branch (i.e. address must be known) although these instructions take the address as an offset from PC, in here we see the absolute address as it was extracted from the micro ops just before write to PC *) | ("AArch64HandSail", "BranchImmediate") -> nias | ("AArch64HandSail", "BranchConditional") -> NIA_successor :: nias | ("AArch64HandSail", "CompareAndBranch") -> NIA_successor :: nias | ("AArch64HandSail", "TestBitAndBranch") -> NIA_successor :: nias (* AArch64 calculated address branch *) | ("AArch64HandSail", "BranchRegister") -> (* do some parsing of the ast fields to figure out which register holds the branching address i.e. find n in "BR ". The ast constructor from armV8.sail: (reg_index,BranchType) BranchRegister; *) let n_integer = match instruction_fields with | [(_, _, n); _] -> integer_of_bit_list n | _ -> fail end in let () = ensure (0 <= n_integer && n_integer <= 31) "expected register number from 0 to 31" in if n_integer = 31 then nias (* BR XZR *) else (* look for Xn (which we actually call Rn) in regs_in *) let n_reg = "R" ^ (String_extra.stringFromInteger n_integer) in [NIA_register r | forall (r MEM regs_in) | match r with | (Reg name _ _ _) -> name = n_reg | _ -> false end] (** hacky cut-and-paste for AArch64Gen, duplicating code just to see if this suffices *) | ("AArch64GenSail", "BranchImmediate") -> nias | ("AArch64GenSail", "BranchConditional") -> NIA_successor :: nias | ("AArch64GenSail", "CompareAndBranch") -> NIA_successor :: nias | ("AArch64GenSail", "TestBitAndBranch") -> NIA_successor :: nias (* AArch64 calculated address branch *) | ("AArch64GenSail", "branch_unconditional_register") -> (* do some parsing of the ast fields to figure out which register holds the branching address i.e. find n in "BR ". The ast constructor from armV8.sail: (reg_index,BranchType) BranchRegister; *) let n_integer = match instruction_fields with | [(_, _, n); _] -> integer_of_bit_list n | _ -> fail end in let () = ensure (0 <= n_integer && n_integer <= 31) "expected register number from 0 to 31" in if n_integer = 31 then nias (* BR XZR *) else (* look for Xn (which we actually call Rn) in regs_in *) let n_reg = "R" ^ (String_extra.stringFromInteger n_integer) in [NIA_register r | forall (r MEM regs_in) | match r with | (Reg name _ _ _) -> name = n_reg | _ -> false end] (** end of hacky *) | ("AArch64LitmusSail", "CtrlDep") -> NIA_successor :: nias | ("MIPS_ism", "B") -> fail | (s1,s2) -> let () = ensure (not unknown_nia_address) ("unexpected unknown/undefined address in nia_values 4 (\""^s1^"\", \""^s2^"\")") in [ NIA_successor ] end let interp_instruction_analysis (interp_exhaustive : ((list (reg_name * register_value)) -> list event)) instruction nia_reg 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_of_instruction ism nia_address regs_in instruction in let dia = DIA_none in (* FIX THIS! *) let inst_kind = match List.mapMaybe instruction_kind_of_event es with | [] -> if List.length nias > 1 then IK_cond_branch else IK_simple | inst_kind :: inst_kinds -> let () = ensure (List.length nias > 1 --> inst_kind = IK_cond_branch) "multiple NIAs must be IK_cond_branch" in if forall (inst_kind' MEM inst_kinds). inst_kind' = inst_kind then inst_kind (* 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,pp_instruction,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 " ^ pp_instruction instruction) let interp_compare_analyses print_endline pp_instruction (non_pseudo_registers : set reg_name -> set reg_name) context endianness interp_exhaustive instruction nia_reg ism environment analysis_function reg_info = let (regs_in1,regs_out1,regs_feeding_address1,nias1,dia1,inst_kind1) = interp_instruction_analysis interp_exhaustive instruction nia_reg 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,pp_instruction,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)