diff options
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 38 | ||||
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 98 | ||||
| -rw-r--r-- | src/lem_interp/sail_impl_base.lem | 102 | ||||
| -rw-r--r-- | src/pretty_print.ml | 1 | ||||
| -rw-r--r-- | src/process_file.ml | 4 |
5 files changed, 118 insertions, 125 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index a39f3f3a..6149bdea 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -1,3 +1,4 @@ +open import Interp_ast import Interp import Interp_lib import Instruction_extractor @@ -124,11 +125,6 @@ let intern_ifield_value direction v = let direction = intern_direction direction in Interp.V_vector (if Interp.is_inc direction then 0 else (List.length(bits) -1)) direction bits -let num_to_bits size kind num = -(* num_to_bits needed in src_power_get/trans_sail.gen - - rather than reengineer the generation, we include a wrapper here *) - Sail_impl_base.bit_list_of_integer size num - 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*) @@ -331,18 +327,18 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev | Interp.V_ctor (Id_aux (Id "Some") _) _ _ vinstr -> (Ivh_value vinstr,events_out) | Interp.V_ctor (Id_aux (Id "None") _) _ _ _ -> (match (ivh_mode,arg) with - | (Ivh_decode, (Just arg)) -> (Ivh_error (Sail_impl_base.Not_an_instruction_error arg), events_out) - | (Ivh_illegal, (Just arg)) -> (Ivh_error (Sail_impl_base.Not_an_instruction_error arg), events_out) - | (Ivh_unsupported, _) -> (Ivh_error (Sail_impl_base.Unsupported_instruction_error instr), events_out) + | (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 (Sail_impl_base.Internal_error ("Value not an option for " ^ errk_str)), events_out) end) end) - | (Interp.Error l msg,_,_) -> (Ivh_error (Sail_impl_base.Internal_error msg), events_out) + | _ -> (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 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 (Sail_impl_base.Internal_error ("External function not available " ^ i)), events_out) + | Nothing -> (Ivh_error (Interp_interface.Internal_error ("External function not available " ^ i)), events_out) | Just f -> interp_to_value_helper arg ivh_mode err_str instr direction registers events exn_seen (fun _ -> Interp.resume mode stack (Just (f value))) @@ -350,8 +346,8 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev | (Interp.Action (Interp.Fail v) stack, _, _) -> match (Interp.detaint v) with | Interp.V_ctor (Id_aux (Id "Some") _) _ _ (Interp.V_lit (L_aux (L_string s) _)) -> - (Ivh_error (Sail_impl_base.Internal_error ("Assert failed: " ^ s)), events_out) - | _ -> (Ivh_error (Sail_impl_base.Internal_error "Assert failed"), events_out) end + (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 arg ivh_mode err_str instr direction registers events true (fun _ -> Interp.resume mode (Interp.set_in_context stack exp) Nothing) @@ -361,7 +357,7 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev | Interp.SubReg (Id_aux (Id i) _) (Interp.Reg (Id_aux (Id i2) _) _ _) _ -> i2 ^ "." ^ i | _ -> Assert_extra.failwith "Reg not following expected structure" end in let err_value = - (Ivh_error (Sail_impl_base.Internal_error ("Register read of "^ rname^" request in a " ^ errk_str ^ " of " ^ err_str)), + (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 @@ -380,14 +376,14 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev interp_to_value_helper 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 (Sail_impl_base.Internal_error ("Read memory request in a " ^ errk_str)), events_out) + (Ivh_error (Interp_interface.Internal_error ("Read memory request in a " ^ errk_str)), events_out) | (Interp.Action (Interp.Write_mem _ _ _ _) _,_,_) -> - (Ivh_error (Sail_impl_base.Internal_error ("Write memory request in a " ^ errk_str)), events_out) + (Ivh_error (Interp_interface.Internal_error ("Write memory request in a " ^ errk_str)), events_out) | (Interp.Action (Interp.Write_ea _ _) _,_,_) -> - (Ivh_error (Sail_impl_base.Internal_error ("Write ea request in a " ^ errk_str)), events_out) + (Ivh_error (Interp_interface.Internal_error ("Write ea request in a " ^ errk_str)), events_out) | (Interp.Action (Interp.Write_memv _ _ _) _,_,_) -> - (Ivh_error (Sail_impl_base.Internal_error ("Write memory value request in a " ^ errk_str)), events_out) - | _ -> (Ivh_error (Sail_impl_base.Internal_error ("Non expected action in a " ^ errk_str)), events_out) + (Ivh_error (Interp_interface.Internal_error ("Write memory value 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 = @@ -432,7 +428,7 @@ let translate_address top_level end_flag thunk_name registers address = | Ivh_value_after_exn _ -> (Nothing, events) | Ivh_error err -> match err with - | Sail_impl_base.Internal_error msg -> Assert_extra.failwith msg + | Interp_interface.Internal_error msg -> Assert_extra.failwith msg | _ -> Assert_extra.failwith "Not an internal error either" end end @@ -575,7 +571,7 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis | _ -> 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 - | Sail_impl_base.Internal_error msg -> Assert_extra.failwith msg + | Interp_interface.Internal_error msg -> Assert_extra.failwith msg | _ -> Assert_extra.failwith "Not an internal error either" end end diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index b4a6c92b..bf6c6779 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -20,6 +20,104 @@ open import Num open import Assert_extra +(*Type representint the constructor parameters in instruction, other is a type not representable externally*) +type instr_parm_typ = + | Bit (*A single bit, represented as a one element Bitvector as a value*) + | Bvector of maybe nat (* A bitvector type, with length when statically known *) + | Range of maybe nat (*Internally represented as a number, externally as a bitvector of length nat *) + | Enum of string * nat (*Internally represented as either a number or constructor, externally as a bitvector*) + | Other (*An unrepresentable type, will be represented as Unknown in instruciton form *) + +let {coq} instr_parm_typEqual ip1 ip2 = match (ip1,ip2) with + | (Bit,Bit) -> true + | (Bvector i1,Bvector i2) -> i1 = i2 + | (Range i1,Range i2) -> i1 = i2 + | (Enum s1 i1,Enum s2 i2) -> s1 = s2 && i1 = i2 + | (Other,Other) -> true + | _ -> false +end +let inline ~{coq} instr_parm_typEqual = unsafe_structural_equality + +let {coq} instr_parm_typInequal ip1 ip2 = not (instr_parm_typEqual ip1 ip2) +let inline ~{coq} instr_parm_typInequal = unsafe_structural_inequality + +instance (Eq instr_parm_typ) + let (=) = instr_parm_typEqual + let (<>) ip1 ip2 = not (instr_parm_typEqual ip1 ip2) +end + +let instr_parm_typShow ip = match ip with + | Bit -> "Bit" + | Bvector i -> "Bvector " ^ show i + | Range i -> "Range " ^ show i + | Enum s i -> "Enum " ^ s ^ " " ^ show i + | Other -> "Other" + end + +instance (Show instr_parm_typ) +let show = instr_parm_typShow +end + +(*A representation of the AST node for each instruction in the spec, with concrete values from this call, + and the potential static effects from the funcl clause for this instruction + Follows the form of the instruction in instruction_extractor, but populates the parameters with actual values +*) +type instruction = (string * list (string * instr_parm_typ * instruction_field_value)) + +let {coq} instructionEqual i1 i2 = match (i1,i2) with + | ((i1,parms1,effects1),(i2,parms2,effects2)) -> i1=i2 && parms1 = parms2 && effects1 = effects2 +end +let inline ~{coq} instructionEqual = unsafe_structural_equality + +let {coq} instructionInequal i1 i2 = not (instructionEqual i1 i2) +let inline ~{coq} instructionInequal = unsafe_structural_inequality + +type v_kind = Bitv | Bytev + +type decode_error = + | Unsupported_instruction_error of instruction + | Not_an_instruction_error of opcode + | Internal_error of string + + +let decode_error_compare e1 e2 = + match (e1, e2) with + | (Unsupported_instruction_error i1, Unsupported_instruction_error i2) + -> defaultCompare i1 i2 + | (Unsupported_instruction_error _, _) -> LT + | (_, Unsupported_instruction_error _) -> GT + + | (Not_an_instruction_error o1, Not_an_instruction_error o2) -> defaultCompare o1 o2 + | (Not_an_instruction_error _, _) -> LT + | (_, Not_an_instruction_error _) -> GT + + | (Internal_error s1, Internal_error s2) -> compare s1 s2 + (* | (Internal_error _, _) -> LT *) + (* | (_, Internal_error _) -> GT *) + end + +let decode_error_less e1 e2 = decode_error_compare e1 e2 = LT +let decode_error_less_eq e1 e2 = decode_error_compare e1 e2 <> GT +let decode_error_greater e1 e2 = decode_error_compare e1 e2 = GT +let decode_error_greater_eq e1 e2 = decode_error_compare e1 e2 <> LT + +instance (Ord decode_error) + let compare = decode_error_compare + let (<) = decode_error_less + let (<=) = decode_error_less_eq + let (>) = decode_error_greater + let (>=) = decode_error_greater_eq +end + +let decode_error_equal e1 e2 = (decode_error_compare e1 e2) = EQ +let decode_error_inequal e1 e2 = not (decode_error_equal e1 e2) + +instance (Eq decode_error) + let (=) = decode_error_equal + let (<>) = decode_error_inequal +end + + type interpreter_state = Interp.stack (*Deem abstract*) (* Will come from a .lem file generated by Sail, bound to a 'defs' identifier *) type specification = Interp_ast.defs Interp.tannot (*Deem abstract*) diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index 7ede9aa6..88e197d5 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -1,5 +1,4 @@ open import Pervasives_extra -open import Interp_ast (* this can go away *) (* maybe isn't a member of type Ord - this should be in the Lem standard library*) instance forall 'a. Ord 'a => (Ord (maybe 'a)) @@ -794,61 +793,6 @@ instance (Ord barrier_kind) let (>=) = barrier_kindGreaterEq end - - - -(*Type representint the constructor parameters in instruction, other is a type not representable externally*) -type instr_parm_typ = - | Bit (*A single bit, represented as a one element Bitvector as a value*) - | Bvector of maybe nat (* A bitvector type, with length when statically known *) - | Range of maybe nat (*Internally represented as a number, externally as a bitvector of length nat *) - | Enum of string * nat (*Internally represented as either a number or constructor, externally as a bitvector*) - | Other (*An unrepresentable type, will be represented as Unknown in instruciton form *) - -let {coq} instr_parm_typEqual ip1 ip2 = match (ip1,ip2) with - | (Bit,Bit) -> true - | (Bvector i1,Bvector i2) -> i1 = i2 - | (Range i1,Range i2) -> i1 = i2 - | (Enum s1 i1,Enum s2 i2) -> s1 = s2 && i1 = i2 - | (Other,Other) -> true - | _ -> false -end -let inline ~{coq} instr_parm_typEqual = unsafe_structural_equality - -let {coq} instr_parm_typInequal ip1 ip2 = not (instr_parm_typEqual ip1 ip2) -let inline ~{coq} instr_parm_typInequal = unsafe_structural_inequality - -instance (Eq instr_parm_typ) - let (=) = instr_parm_typEqual - let (<>) ip1 ip2 = not (instr_parm_typEqual ip1 ip2) -end - -let instr_parm_typShow ip = match ip with - | Bit -> "Bit" - | Bvector i -> "Bvector " ^ show i - | Range i -> "Range " ^ show i - | Enum s i -> "Enum " ^ s ^ " " ^ show i - | Other -> "Other" - end - -instance (Show instr_parm_typ) -let show = instr_parm_typShow -end - -(*A representation of the AST node for each instruction in the spec, with concrete values from this call, - and the potential static effects from the funcl clause for this instruction - Follows the form of the instruction in instruction_extractor, but populates the parameters with actual values -*) -type instruction = (string * list (string * instr_parm_typ * instruction_field_value)) - -let {coq} instructionEqual i1 i2 = match (i1,i2) with - | ((i1,parms1,effects1),(i2,parms2,effects2)) -> i1=i2 && parms1 = parms2 && effects1 = effects2 -end -let inline ~{coq} instructionEqual = unsafe_structural_equality - -let {coq} instructionInequal i1 i2 = not (instructionEqual i1 i2) -let inline ~{coq} instructionInequal = unsafe_structural_inequality - (** operations and coercions on basic values *) val word8_to_bitls : word8 -> list bit_lifted @@ -1380,49 +1324,3 @@ end instance (Show dia) let show = stringFromDia end - - -type v_kind = Bitv | Bytev - -type decode_error = - | Unsupported_instruction_error of instruction - | Not_an_instruction_error of opcode - | Internal_error of string - - -let decode_error_compare e1 e2 = - match (e1, e2) with - | (Unsupported_instruction_error i1, Unsupported_instruction_error i2) - -> defaultCompare i1 i2 - | (Unsupported_instruction_error _, _) -> LT - | (_, Unsupported_instruction_error _) -> GT - - | (Not_an_instruction_error o1, Not_an_instruction_error o2) -> defaultCompare o1 o2 - | (Not_an_instruction_error _, _) -> LT - | (_, Not_an_instruction_error _) -> GT - - | (Internal_error s1, Internal_error s2) -> compare s1 s2 - (* | (Internal_error _, _) -> LT *) - (* | (_, Internal_error _) -> GT *) - end - -let decode_error_less e1 e2 = decode_error_compare e1 e2 = LT -let decode_error_less_eq e1 e2 = decode_error_compare e1 e2 <> GT -let decode_error_greater e1 e2 = decode_error_compare e1 e2 = GT -let decode_error_greater_eq e1 e2 = decode_error_compare e1 e2 <> LT - -instance (Ord decode_error) - let compare = decode_error_compare - let (<) = decode_error_less - let (<=) = decode_error_less_eq - let (>) = decode_error_greater - let (>=) = decode_error_greater_eq -end - -let decode_error_equal e1 e2 = (decode_error_compare e1 e2) = EQ -let decode_error_inequal e1 e2 = not (decode_error_equal e1 e2) - -instance (Eq decode_error) - let (=) = decode_error_equal - let (<>) = decode_error_inequal -end diff --git a/src/pretty_print.ml b/src/pretty_print.ml index 9e312242..6ecf2be1 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -3109,6 +3109,7 @@ let pp_defs_lem (types_file,types_modules) (prompt_file,prompt_modules) (state_f concat [(separate_map hardline) (fun lib -> separate space [string " import";string lib]) ["Interp";"Interp_ast"]; + string "open import Deep_shallow_convert"; hardline; hardline; string "module SI = Interp"; hardline; diff --git a/src/process_file.ml b/src/process_file.ml index 7bd7e134..a5423cc4 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -183,7 +183,7 @@ let output1 libpath out_arg filename defs = let ((o'',_, _) as ext_o'') = open_output_with_check_unformatted (f' ^ "embed_sequential.lem") in (Pretty_print.pp_defs_lem - (o,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Deep_shallow_convert"]) + (o,["Pervasives_extra";"Sail_impl_base";"Sail_values"]) (o',["Pervasives_extra";"Sail_impl_base";"Prompt";"Sail_values"; String.capitalize types_module]) (o'',["Pervasives_extra";"Sail_impl_base";"State";"Sail_values"; @@ -202,7 +202,7 @@ let output1 libpath out_arg filename defs = let ((o'',_, _) as ext_o'') = open_output_with_check_unformatted (f' ^ "_embed_sequential.lem") in (Pretty_print.pp_defs_lem - (o,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Deep_shallow_convert";lib]) + (o,["Pervasives_extra";"Sail_impl_base";"Sail_values";lib]) (o',["Pervasives_extra";"Sail_impl_base";"Prompt"; "Sail_values";String.capitalize types_module;lib]) (o'',["Pervasives_extra";"Sail_impl_base";"State"; |