diff options
Diffstat (limited to 'src/lem_interp/0.11/interp_inter_imp.lem')
| -rw-r--r-- | src/lem_interp/0.11/interp_inter_imp.lem | 1338 |
1 files changed, 1338 insertions, 0 deletions
diff --git a/src/lem_interp/0.11/interp_inter_imp.lem b/src/lem_interp/0.11/interp_inter_imp.lem new file mode 100644 index 00000000..3413494e --- /dev/null +++ b/src/lem_interp/0.11/interp_inter_imp.lem @@ -0,0 +1,1338 @@ +(*========================================================================*) +(* 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) + + |