From aa08c004b613d11b4e3d6b8909c06eec5cee5b86 Mon Sep 17 00:00:00 2001 From: Jon French Date: Fri, 21 Jul 2017 20:33:31 +0100 Subject: move value type definitions to ott, and introduce new E_internal_value ast node for passing around encapsulated evaluated values; change Interp.to_exp to now just wrap values in this node --- src/lem_interp/interp.lem | 160 ++----- src/lem_interp/interp_ast.lem | 771 ++++++++++++++++++---------------- src/lem_interp/interp_inter_imp.lem | 242 +++++------ src/lem_interp/interp_interface.lem | 10 +- src/lem_interp/pretty_interp.ml | 332 +++++++++------ src/lem_interp/printing_functions.ml | 109 +---- src/lem_interp/printing_functions.mli | 6 +- src/lem_interp/run_interp_model.ml | 4 +- 8 files changed, 787 insertions(+), 847 deletions(-) (limited to 'src/lem_interp') diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 9c88eec7..a0276963 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -54,8 +54,6 @@ open import Interp_ast open import Interp_utilities open import Instruction_extractor -type tannot = Interp_utilities.tannot - val debug_print : string -> unit declare ocaml target_rep function debug_print s = `Printf.eprintf` "%s" s @@ -78,36 +76,14 @@ let non_det_annot annot maybe_id = match annot with | _ -> Nothing end -type i_direction = IInc | IDec let is_inc = function | IInc -> true | _ -> false end let id_of_string s = (Id_aux (Id s) Unknown) -type reg_form = - | Reg of id * tannot * i_direction - | SubReg of id * reg_form * index_range - -type ctor_kind = C_Enum of nat | C_Union - -type value = - | V_boxref of nat * t - | V_lit of lit - | V_tuple of list value - | V_list of list value - (* A full vector: int is the first index, bool says if that's most or least significant *) - | V_vector of nat * i_direction * list value - (* A vector with default values, second int stores length; as above otherwise *) - | V_vector_sparse of nat * nat * i_direction * list (nat * value) * value - | V_record of t * list (id * value) - | V_ctor of id * t * ctor_kind * value - | V_unknown (* Distinct from undefined, used by memory system *) - | V_register of reg_form (* Value to store register access, when not actively reading or writing *) - | V_register_alias of (alias_spec tannot) * tannot (* Same as above, but to a concatenation of two registers *) - | V_track of value * (set reg_form) (* Used when memory system wants to track what register(s) a value came from *) let rec {ocaml} string_of_reg_form r = match r with - | Reg id _ _ -> get_id id - | SubReg id reg_form _ -> (string_of_reg_form reg_form) ^ "." ^ (get_id id) + | Form_Reg id _ _ -> get_id id + | Form_SubReg id reg_form _ -> (string_of_reg_form reg_form) ^ "." ^ (get_id id) end let rec {ocaml} string_of_value v = match v with @@ -249,7 +225,7 @@ end let reg_start_pos reg = match reg with - | Reg _ (Just(typ,_,_,_,_)) _ -> + | Form_Reg _ (Just(typ,_,_,_,_)) _ -> let start_from_vec targs = match targs with | T_args [T_arg_nexp (Ne_const s);_;_;_] -> natFromInteger s | T_args [T_arg_nexp _; T_arg_nexp (Ne_const s); T_arg_order Odec; _] -> (natFromInteger s) - 1 @@ -277,7 +253,7 @@ end let reg_size reg = match reg with - | Reg _ (Just(typ,_,_,_,_)) _ -> + | Form_Reg _ (Just(typ,_,_,_,_)) _ -> let end_from_vec targs = match targs with | T_args [_;T_arg_nexp (Ne_const s);_;_] -> natFromInteger s | _ -> Assert_extra.failwith "register vector type not well formed" @@ -439,7 +415,7 @@ let rec to_registers dd (Defs defs) = | Nothing -> dd | Just(t, _, _, _,_) -> dd (*TODO, lets pull the direction out properly*) end in - Map.insert (get_id id) (V_register(Reg id tannot dir)) (to_registers dd (Defs defs)) + Map.insert (get_id id) (V_register(Form_Reg id tannot dir)) (to_registers dd (Defs defs)) | DEF_reg_dec (DEC_aux (DEC_alias id aspec) (l,tannot)) -> Map.insert (get_id id) (V_register_alias aspec tannot) (to_registers dd (Defs defs)) | _ -> to_registers dd (Defs defs) @@ -1039,7 +1015,7 @@ let rec combine_typs ts = let reg_to_t r = match r with - | Reg _ (Just (t,_,_,_,_)) _ -> t + | Form_Reg _ (Just (t,_,_,_,_)) _ -> t | _ -> T_var "fresh" end @@ -1084,89 +1060,8 @@ let rec val_typ v = | V_register_alias _ _ -> T_var "fresh_alias" end -(* When mode.track_values keeps tracking on registers by extending environment *) let rec to_exp mode env v : (exp tannot * lenv) = - let mk_annot is_ctor ctor_kind = - (Interp_ast.Unknown, - if is_ctor - then match ctor_kind with - | Just(C_Enum i) -> (enum_annot (val_typ v) (integerFromNat i)) - | _ -> (ctor_annot (val_typ v)) end - else (val_annot (val_typ v))) in - let annot = mk_annot false Nothing in - let mapf vs ((LEnv l env) as lenv) : (list (exp tannot) * lenv) = - let (es, env) = - List.foldr (fun v (es,env) -> let (e,ev) = (to_exp mode env v) in - if mode.track_values - then ((e::es), union_env ev env) - else ((e::es), env)) - ([],(LEnv l Map.empty)) vs in - (es, union_env env lenv) - in - match v with - | V_boxref n t -> (E_aux (E_id (Id_aux (Id (show n)) Unknown)) annot, env) - | V_lit lit -> (E_aux (E_lit lit) annot, env) - | V_tuple(vals) -> - let (es,env') = mapf vals env in (E_aux (E_tuple es) annot, env') - | V_vector n dir vals -> - let (es,env') = mapf vals env in - if (is_inc(dir) && n=0) - then (E_aux (E_vector es) annot, env') - else if is_inc(dir) - then (E_aux (E_vector_indexed - (List.reverse (snd (List.foldl (fun (n,acc) e -> (n+1,((integerFromNat n),e)::acc)) (n,[]) es))) - (Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing))) annot, env') - else if (n+1)= List.length vals - then (E_aux (E_vector es) annot, env') - else - (E_aux (E_vector_indexed - (snd (List.foldr (fun e (n,acc) -> (n+1,((integerFromNat n),e)::acc)) (n-(List.length es),[]) es)) - (Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing))) annot, env') - | V_vector_sparse n m dir vals d -> - let ((es : (list (exp tannot))),env') = mapf (List.map (fun (i,v) -> v) vals) env in - let ((d : (exp tannot)),env') = to_exp mode env' d in - (E_aux (E_vector_indexed - ((if is_inc(dir) then List.reverse else (fun i -> i)) - (List.map (fun ((i,v), e) -> ((integerFromNat i), e)) (List.zip vals es))) - (Def_val_aux (Def_val_dec d) (Interp_ast.Unknown, Nothing))) annot, env') - | V_record t ivals -> - let (es,env') = mapf (List.map (fun (i,v) -> v) ivals) env in - (E_aux (E_record(FES_aux (FES_Fexps - (List.map (fun ((id,value), e) -> (FE_aux (FE_Fexp id e) (Unknown,Nothing))) - (List.zip ivals es)) false) - (Unknown,Nothing))) annot, env') - | V_list(vals) -> let (es,env') = mapf vals env in (E_aux (E_list es) annot, env') - | V_ctor id t ckind vals -> - let annotation = mk_annot true (Just ckind) in - (match (vals,ckind) with - | (V_lit (L_aux L_unit _), C_Union) -> (E_aux (E_app id []) annotation, env) - | (V_lit (L_aux L_unit _), C_Enum _) -> (E_aux (E_id id) annotation, env) - | (V_track (V_lit (L_aux L_unit _)) _, C_Union) -> (E_aux (E_app id []) annotation, env) - | (V_track (V_lit (L_aux L_unit _)) _, C_Enum _) -> (E_aux (E_id id) annotation, env) - | (V_tuple vals,_) -> let (es,env') = mapf vals env in (E_aux (E_app id es) annotation, env') - | (V_track (V_tuple vals) _,_) -> let (es,env') = mapf vals env in (E_aux (E_app id es) annotation, env') - | (V_track _ _,_) -> - if mode.track_values - then begin let (fid,env') = fresh_var env in - let env' = add_to_env (fid,vals) env' in - (E_aux - (E_app id [(E_aux (E_id fid) (Interp_ast.Unknown, (val_annot (val_typ vals))))]) - annotation, env') - end - else let (e,env') = (to_exp mode env vals) in (E_aux (E_app id [e]) annotation, env') - | _ -> - let (e,env') = (to_exp mode env vals) in (E_aux (E_app id [e]) annotation,env') end) - | V_register (Reg id tan dir) -> (E_aux (E_id id) annot, env) - | V_register _ -> Assert_extra.failwith "V_register contains subreg" - | V_register_alias _ _ -> (E_aux (E_id (id_of_string "dummy_register")) annot, env) (*If this persists, then alias spec must change*) - | V_track v' _ -> - if mode.track_values - then begin let (fid,env') = fresh_var env in - let env' = add_to_env (fid,v) env' in - (E_aux (E_id fid) annot, env') end - else to_exp mode env v' - | V_unknown -> (E_aux (E_id (id_of_string "-100")) annot, env) -end + ((E_aux (E_internal_value v) (Interp_ast.Unknown, (val_annot (val_typ v)))), env) val env_to_let : interp_mode -> lenv -> (exp tannot) -> lenv -> ((exp tannot) * lenv) let rec env_to_let_help mode env taint_env = match env with @@ -1573,6 +1468,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = (T_var "fresh_v", Tag_empty,[],(Effect_aux (Effect_set []) Unknown),(Effect_aux (Effect_set []) Unknown)) | Just(t, tag, ncs, ef,efr) -> (t,tag,ncs,ef,efr) end in match exp with + | E_internal_value v -> (Value v, l_mem, l_env) | E_lit lit -> if is_lit_vector lit then let is_inc = (match typ with @@ -1637,7 +1533,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = | _ -> match in_env regs name with (* Register isn't a local value, so pull from global environment *) | Just(V_register regform) -> regform - | _ -> Reg id annot default_dir end end in + | _ -> Form_Reg id annot default_dir end end in (Action (Read_reg regf Nothing) (mk_hole l annot t_level l_env l_mem), l_mem, l_env) | Tag_alias -> match in_env aliases name with @@ -1823,7 +1719,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = (match in_env (env_from_list fexps) (get_id id) with | Just v -> (Value (retaint value_whole v),lm,l_env) | Nothing -> (Error l "Internal_error: Field not found in record",lm,le) end) - | V_register ((Reg _ annot _) as reg_form) -> + | V_register ((Form_Reg _ annot _) as reg_form) -> let id' = match annot with | Just((T_id id'),_,_,_,_) -> id' | Just((T_abbrev (T_id id') _),_,_,_,_) -> id' @@ -1833,7 +1729,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = | Just(indexes) -> (match in_env indexes (get_id id) with | Just ir -> - let sub_reg = SubReg id reg_form ir in + let sub_reg = Form_SubReg id reg_form ir in (Action (Read_reg sub_reg Nothing) (mk_hole l (val_annot (reg_to_t sub_reg)) t_level le lm),lm,le) | _ -> (Error l "Internal error: unrecognized read, no id",lm,le) end) @@ -1845,22 +1741,22 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = (fun a -> match (exp,a) with | (E_aux _ (l,Just(_,Tag_extern _,_,_,_)), - (Action (Read_reg ((Reg _ (Just((T_id id'),_,_,_,_)) _) as regf) Nothing) s)) -> + (Action (Read_reg ((Form_Reg _ (Just((T_id id'),_,_,_,_)) _) as regf) Nothing) s)) -> match in_env subregs id' with | Just(indexes) -> (match in_env indexes (get_id id) with | Just ir -> - (Action (Read_reg (SubReg id regf ir) Nothing) s) + (Action (Read_reg (Form_SubReg id regf ir) Nothing) s) | _ -> Error l "Internal error, unrecognized read, no id" end) | Nothing -> Error l "Internal error, unrecognized read, no reg" end | (E_aux _ (l,Just(_,Tag_extern _,_,_,_)), - (Action (Read_reg ((Reg _ (Just((T_abbrev (T_id id') _),_,_,_,_)) _) as regf) Nothing) s))-> + (Action (Read_reg ((Form_Reg _ (Just((T_abbrev (T_id id') _),_,_,_,_)) _) as regf) Nothing) s))-> match in_env subregs id' with | Just(indexes) -> match in_env indexes (get_id id) with | Just ir -> - (Action (Read_reg (SubReg id regf ir) Nothing) s) + (Action (Read_reg (Form_SubReg id regf ir) Nothing) s) | _ -> Error l "Internal error, unrecognized read, no id" end | Nothing -> Error l "Internal error, unrecognized read, no reg" end @@ -2575,7 +2471,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (match in_env indexes (get_id subreg) with | Just ir -> (Action - (Write_reg (SubReg subreg (Reg reg annot' default_dir) ir) Nothing + (Write_reg (Form_SubReg subreg (Form_Reg reg annot' default_dir) ir) Nothing (update_vector_start default_dir (get_first_index_range ir) (get_index_range_size ir) value)) (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot)) @@ -2589,7 +2485,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (match in_env indexes (get_id subreg) with | Just ir -> (Action - (Write_reg (SubReg subreg (Reg reg annot' default_dir) ir) Nothing + (Write_reg (Form_SubReg subreg (Form_Reg reg annot' default_dir) ir) Nothing (update_vector_start default_dir (get_first_index_range ir) (get_index_range_size ir) value)) (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot)) @@ -2602,7 +2498,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (fun v le lm -> match v with | V_lit (L_aux (L_num i) _) -> let i = natFromInteger i in - (Action (Write_reg (Reg reg annot' default_dir) (Just (i,i)) + (Action (Write_reg (Form_Reg reg annot' default_dir) (Just (i,i)) (update_vector_start default_dir i 1 value)) (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot)) t_level l_env l_mem Top), l_mem, l_env) @@ -2619,7 +2515,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level | V_lit (L_aux (L_num stop) _) -> let (start,stop) = (natFromInteger start,natFromInteger stop) in let size = if start < stop then stop - start +1 else start -stop +1 in - (Action (Write_reg (Reg reg annot' default_dir) (Just (start,stop)) + (Action (Write_reg (Form_Reg reg annot' default_dir) (Just (start,stop)) (update_vector_start default_dir start size value)) (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot)) t_level l_env l_mem Top), @@ -2640,7 +2536,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level | (T_app "vector" (T_args [T_arg_nexp (Ne_const b1); T_arg_nexp (Ne_const r1); _;_]), T_app "vector" (T_args [T_arg_nexp (Ne_const b2); T_arg_nexp (Ne_const r2); _;_])) -> (Action - (Write_reg (Reg reg1 annot1 default_dir) Nothing + (Write_reg (Form_Reg reg1 annot1 default_dir) Nothing (slice_vector value (natFromInteger b1) (natFromInteger r1))) (Thunk_frame (E_aux (E_assign (LEXP_aux (LEXP_id reg2) annot2) @@ -3062,13 +2958,13 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level | Read_mem _ _ _ -> ((Action a s,lm,le), next_builder, Nothing) | Read_mem_tagged _ _ _ -> ((Action a s,lm,le), next_builder, Nothing) | Call_extern _ _ -> ((Action a s,lm,le), next_builder, Nothing) - | Write_reg ((Reg _ (Just(T_id id',_,_,_,_)) _) as regf) Nothing value -> + | Write_reg ((Form_Reg _ (Just(T_id id',_,_,_,_)) _) as regf) Nothing value -> match in_env subregs id' with | Just(indexes) -> match in_env indexes (get_id id) with | Just ir -> ((Action - (Write_reg (SubReg id regf ir) Nothing + (Write_reg (Form_SubReg id regf ir) Nothing (update_vector_start default_dir (get_first_index_range ir) (get_index_range_size ir) value)) s, lm,le), @@ -3076,13 +2972,13 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level | _ -> ((Error l "Internal error, unrecognized write, no field",lm,le),Nothing,Nothing) end | Nothing -> ((Error l "Internal error, unrecognized write, no subreges",lm,le),Nothing,Nothing) end - | Write_reg ((Reg _ (Just((T_abbrev(T_id id') _),_,_,_,_)) _) as regf) Nothing value -> + | Write_reg ((Form_Reg _ (Just((T_abbrev(T_id id') _),_,_,_,_)) _) as regf) Nothing value -> match in_env subregs id' with | Just(indexes) -> match in_env indexes (get_id id) with | Just ir -> ((Action - (Write_reg (SubReg id regf ir) Nothing + (Write_reg (Form_SubReg id regf ir) Nothing (update_vector_start default_dir (get_first_index_range ir) (get_index_range_size ir) value)) s, lm,le), @@ -3130,7 +3026,7 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) = (match in_env subregs reg_ti with | Just indexes -> (match in_env indexes (get_id subreg) with - | Just ir -> (Action (Read_reg (SubReg subreg (Reg reg annot' default_dir) ir) Nothing) stack, + | Just ir -> (Action (Read_reg (Form_SubReg subreg (Form_Reg reg annot' default_dir) ir) Nothing) stack, l_mem, l_env) | _ -> (Error l "Internal error, alias spec has unknown field", l_mem, l_env) end) | _ -> (Error l (String.stringAppend "Internal error: alias spec has unknown register type " reg_ti), @@ -3140,7 +3036,7 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) = (fun v le lm -> match v with | V_lit (L_aux (L_num i) _) -> let i = natFromInteger i in - (Action (Read_reg (Reg reg annot' default_dir) (Just (i,i))) stack, l_mem, l_env) + (Action (Read_reg (Form_Reg reg annot' default_dir) (Just (i,i))) stack, l_mem, l_env) | _ -> Assert_extra.failwith "alias bit did not reduce to number" end) (fun a -> a) (*Should not currently happen as type system enforces constants*) | AL_slice (RI_aux (RI_id reg) (_,annot')) start stop -> @@ -3154,7 +3050,7 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) = (match v with | V_lit (L_aux (L_num stop) _) -> let (start,stop) = (natFromInteger start,natFromInteger stop) in - (Action (Read_reg (Reg reg annot' default_dir) (Just (start,stop))) stack, l_mem, l_env) + (Action (Read_reg (Form_Reg reg annot' default_dir) (Just (start,stop))) stack, l_mem, l_env) | _ -> Assert_extra.failwith ("Alias slice evaluted non-lit " ^ (string_of_value v)) end)) (fun a -> a)) @@ -3162,7 +3058,7 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) = end) (fun a -> a) (*Neither action function should occur, due to above*) | AL_concat (RI_aux (RI_id reg1) (l1, annot1)) (RI_aux (RI_id reg2) annot2) -> - (Action (Read_reg (Reg reg1 annot1 default_dir) Nothing) + (Action (Read_reg (Form_Reg reg1 annot1 default_dir) Nothing) (Hole_frame redex_id (E_aux (E_vector_append (E_aux (E_id redex_id) (l1, (intern_annot annot1))) (E_aux (E_id reg2) annot2)) diff --git a/src/lem_interp/interp_ast.lem b/src/lem_interp/interp_ast.lem index b706d3aa..733d1a36 100644 --- a/src/lem_interp/interp_ast.lem +++ b/src/lem_interp/interp_ast.lem @@ -40,9 +40,11 @@ (* SUCH DAMAGE. *) (*========================================================================*) -(* generated by Ott 0.25 from: l2_typ.ott l2.ott *) +(* generated by Ott 0.25 from: l2.ott *) open import Pervasives +open import Pervasives +open import Pervasives_extra open import Map open import Maybe open import Set_extra @@ -72,21 +74,17 @@ type base_kind_aux = (* base kind *) | BK_effect (* kind of effect sets *) -type base_kind = - | BK_aux of base_kind_aux * l - - -type kid_aux = (* variables with kind, ticked to differntiate from program variables *) +type kid_aux = (* kinded IDs: $Type$, $Nat$, $Order$, and $Effect$ variables *) | Var of x -type id_aux = (* Identifier *) +type id_aux = (* identifier *) | Id of x | DeIid of x (* remove infix status *) -type kind_aux = (* kinds *) - | K_kind of list base_kind +type base_kind = + | BK_aux of base_kind_aux * l type kid = @@ -97,24 +95,28 @@ type id = | Id_aux of id_aux * l -type kind = - | K_aux of kind_aux * l +type kind_aux = (* kinds *) + | K_kind of list base_kind -type nexp_aux = (* expression of kind Nat, for vector sizes and origins *) - | Nexp_id of id (* identifier, bound by def Nat x = nexp *) +type nexp_aux = (* numeric expression, of kind $Nat$ *) + | Nexp_id of id (* abbreviation identifier *) | Nexp_var of kid (* variable *) | Nexp_constant of integer (* constant *) | Nexp_times of nexp * nexp (* product *) | Nexp_sum of nexp * nexp (* sum *) | Nexp_minus of nexp * nexp (* subtraction *) | Nexp_exp of nexp (* exponential *) - | Nexp_neg of nexp (* For internal use *) + | Nexp_neg of nexp (* for internal use only *) and nexp = | Nexp_aux of nexp_aux * l +type kind = + | K_aux of kind_aux * l + + type base_effect_aux = (* effect *) | BE_rreg (* read register *) | BE_wreg (* write register *) @@ -129,23 +131,23 @@ type base_effect_aux = (* effect *) | BE_depend (* dynamic footprint *) | BE_undef (* undefined-instruction exception *) | BE_unspec (* unspecified values *) - | BE_nondet (* nondeterminism from intra-instruction parallelism *) - | BE_escape (* Tracking of expressions and functions that might call exit *) - | BE_lset (* Local mutation happend; not user-writable *) - | BE_lret (* Local return happened; not user-writable *) + | BE_nondet (* nondeterminism, from $nondet$ *) + | BE_escape (* potential call of $exit$ *) + | BE_lset (* local mutation; not user-writable *) + | BE_lret (* local return; not user-writable *) type base_effect = | BE_aux of base_effect_aux * l -type order_aux = (* vector order specifications, of kind Order *) +type order_aux = (* vector order specifications, of kind $Order$ *) | Ord_var of kid (* variable *) - | Ord_inc (* increasing (little-endian) *) - | Ord_dec (* decreasing (big-endian) *) + | Ord_inc (* increasing *) + | Ord_dec (* decreasing *) -type effect_aux = (* effect set, of kind Effects *) +type effect_aux = (* effect set, of kind $Effect$ *) | Effect_var of kid | Effect_set of list base_effect (* effect set *) @@ -163,11 +165,6 @@ let effect_union e1 e2 = end -type kinded_id_aux = (* optionally kind-annotated identifier *) - | KOpt_none of kid (* identifier *) - | KOpt_kind of kind * kid (* kind-annotated variable *) - - type n_constraint_aux = (* constraint over kind $Nat$ *) | NC_fixed of nexp * nexp | NC_bounded_ge of nexp * nexp @@ -175,17 +172,22 @@ type n_constraint_aux = (* constraint over kind $Nat$ *) | NC_nat_set_bounded of kid * list integer -type kinded_id = - | KOpt_aux of kinded_id_aux * l +type kinded_id_aux = (* optionally kind-annotated identifier *) + | KOpt_none of kid (* identifier *) + | KOpt_kind of kind * kid (* kind-annotated variable *) type n_constraint = | NC_aux of n_constraint_aux * l -type quant_item_aux = (* Either a kinded identifier or a nexp constraint for a typquant *) - | QI_id of kinded_id (* An optionally kinded identifier *) - | QI_const of n_constraint (* A constraint for this type *) +type kinded_id = + | KOpt_aux of kinded_id_aux * l + + +type quant_item_aux = (* kinded identifier or $Nat$ constraint *) + | QI_id of kinded_id (* optionally kinded identifier *) + | QI_const of n_constraint (* $Nat$ constraint *) type quant_item = @@ -194,38 +196,25 @@ type quant_item = type typquant_aux = (* type quantifiers and constraints *) | TypQ_tq of list quant_item - | TypQ_no_forall (* sugar, omitting quantifier and constraints *) - - -type lit_aux = (* Literal constant *) - | L_unit (* $() : unit$ *) - | L_zero (* $bitzero : bit$ *) - | L_one (* $bitone : bit$ *) - | L_true (* $true : bool$ *) - | L_false (* $false : bool$ *) - | L_num of integer (* natural number constant *) - | L_hex of string (* bit vector constant, C-style *) - | L_bin of string (* bit vector constant, C-style *) - | L_undef (* constant representing undefined values *) - | L_string of string (* string constant *) + | TypQ_no_forall (* empty *) type typquant = | TypQ_aux of typquant_aux * l -type typ_aux = (* Type expressions, of kind $Type$ *) - | Typ_wild (* Unspecified type *) - | Typ_id of id (* Defined type *) - | Typ_var of kid (* Type variable *) - | Typ_fn of typ * typ * effect (* Function type (first-order only in user code) *) - | Typ_tup of list typ (* Tuple type *) +type typ_aux = (* type expressions, of kind $Type$ *) + | Typ_wild (* unspecified type *) + | Typ_id of id (* defined type *) + | Typ_var of kid (* type variable *) + | Typ_fn of typ * typ * effect (* Function (first-order only in user code) *) + | Typ_tup of list typ (* Tuple *) | Typ_app of id * list typ_arg (* type constructor application *) and typ = | Typ_aux of typ_aux * l -and typ_arg_aux = (* Type constructor arguments of all kinds *) +and typ_arg_aux = (* type constructor arguments of all kinds *) | Typ_arg_nexp of nexp | Typ_arg_typ of typ | Typ_arg_order of order @@ -235,15 +224,41 @@ and typ_arg = | Typ_arg_aux of typ_arg_aux * l -type lit = - | L_aux of lit_aux * l +type lit_aux = (* literal constant *) + | L_unit (* $() : unit$ *) + | L_zero (* $bitzero : bit$ *) + | L_one (* $bitone : bit$ *) + | L_true (* $true : bool$ *) + | L_false (* $false : bool$ *) + | L_num of integer (* natural number constant *) + | L_hex of string (* bit vector constant, C-style *) + | L_bin of string (* bit vector constant, C-style *) + | L_string of string (* string constant *) + | L_undef (* undefined-value constant *) + + +type index_range_aux = (* index specification, for bitfields in register types *) + | BF_single of integer (* single index *) + | BF_range of integer * integer (* index range *) + | BF_concat of index_range * index_range (* concatenation of index ranges *) + +and index_range = + | BF_aux of index_range_aux * l type typschm_aux = (* type scheme *) | TypSchm_ts of typquant * typ -type pat_aux 'a = (* Pattern *) +type lit = + | L_aux of lit_aux * l + + +type typschm = + | TypSchm_aux of typschm_aux * l + + +type pat_aux 'a = (* pattern *) | P_lit of lit (* literal constant pattern *) | P_wild (* wildcard *) | P_as of (pat 'a) * id (* named pattern *) @@ -260,455 +275,473 @@ type pat_aux 'a = (* Pattern *) and pat 'a = | P_aux of (pat_aux 'a) * annot 'a -and fpat_aux 'a = (* Field pattern *) +and fpat_aux 'a = (* field pattern *) | FP_Fpat of id * (pat 'a) and fpat 'a = | FP_aux of (fpat_aux 'a) * annot 'a -type typschm = - | TypSchm_aux of typschm_aux * l +type name_scm_opt_aux = (* optional variable naming-scheme constraint *) + | Name_sect_none + | Name_sect_some of string -type reg_id_aux 'a = - | RI_id of id +type type_union_aux = (* type union constructors *) + | Tu_id of id + | Tu_ty_id of typ * id -type exp_aux 'a = (* Expression *) - | E_block of list (exp 'a) (* block *) - | E_nondet of list (exp 'a) (* nondeterminisitic block, expressions evaluate in an unspecified order, or concurrently *) - | E_id of id (* identifier *) - | E_lit of lit (* literal constant *) - | E_cast of typ * (exp 'a) (* cast *) - | E_app of id * list (exp 'a) (* function application *) - | E_app_infix of (exp 'a) * id * (exp 'a) (* infix function application *) - | E_tuple of list (exp 'a) (* tuple *) - | E_if of (exp 'a) * (exp 'a) * (exp 'a) (* conditional *) - | E_for of id * (exp 'a) * (exp 'a) * (exp 'a) * order * (exp 'a) (* loop *) - | E_vector of list (exp 'a) (* vector (indexed from 0) *) - | E_vector_indexed of list (integer * (exp 'a)) * (opt_default 'a) (* vector (indexed consecutively) *) - | E_vector_access of (exp 'a) * (exp 'a) (* vector access *) - | E_vector_subrange of (exp 'a) * (exp 'a) * (exp 'a) (* subvector extraction *) - | E_vector_update of (exp 'a) * (exp 'a) * (exp 'a) (* vector functional update *) - | E_vector_update_subrange of (exp 'a) * (exp 'a) * (exp 'a) * (exp 'a) (* vector subrange update (with vector) *) - | E_vector_append of (exp 'a) * (exp 'a) (* vector concatenation *) - | E_list of list (exp 'a) (* list *) - | E_cons of (exp 'a) * (exp 'a) (* cons *) - | E_record of (fexps 'a) (* struct *) - | E_record_update of (exp 'a) * (fexps 'a) (* functional update of struct *) - | E_field of (exp 'a) * id (* field projection from struct *) - | E_case of (exp 'a) * list (pexp 'a) (* pattern matching *) - | E_let of (letbind 'a) * (exp 'a) (* let expression *) - | E_assign of (lexp 'a) * (exp 'a) (* imperative assignment *) - | E_sizeof of nexp (* Expression to return the value of the nexp variable or expression at run time *) - | E_exit of (exp 'a) (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *) - | E_return of (exp 'a) (* expression to end current function execution and return the value of exp from the function; this can be used to break out of for loops *) - | E_assert of (exp 'a) * (exp 'a) (* expression to halt with error, when the first expression is false, reporting the optional string as an error *) - | E_internal_cast of annot 'a * (exp 'a) (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *) - | E_internal_exp of annot 'a (* This is an internal use for passing nexp information to library functions, postponed for constraint solving *) - | E_sizeof_internal of annot 'a (* For sizeof during type checking, to replace nexp with internal n *) - | E_internal_exp_user of annot 'a * annot 'a (* This is like the above but the user has specified an implicit parameter for the current function *) - | E_comment of string (* For generated unstructured comments *) - | E_comment_struc of (exp 'a) (* For generated structured comments *) - | E_internal_let of (lexp 'a) * (exp 'a) * (exp 'a) (* This is an internal node for compilation that demonstrates the scope of a local mutable variable *) - | E_internal_plet of (pat 'a) * (exp 'a) * (exp 'a) (* This is an internal node, used to distinguised some introduced lets during processing from original ones *) - | E_internal_return of (exp 'a) (* For internal use to embed into monad definition *) +type name_scm_opt = + | Name_sect_aux of name_scm_opt_aux * l -and exp 'a = - | E_aux of (exp_aux 'a) * annot 'a -and lexp_aux 'a = (* lvalue expression *) - | LEXP_id of id (* identifier *) - | LEXP_memory of id * list (exp 'a) (* memory write via function call *) - | LEXP_cast of typ * id - | LEXP_tup of list (lexp 'a) (* set multiple at a time, a check will ensure it's not memory *) - | LEXP_vector of (lexp 'a) * (exp 'a) (* vector element *) - | LEXP_vector_range of (lexp 'a) * (exp 'a) * (exp 'a) (* subvector *) - | LEXP_field of (lexp 'a) * id (* struct field *) +type type_union = + | Tu_aux of type_union_aux * l -and lexp 'a = - | LEXP_aux of (lexp_aux 'a) * annot 'a -and fexp_aux 'a = (* Field-expression *) - | FE_Fexp of id * (exp 'a) +type kind_def_aux 'a = (* Definition body for elements of kind *) + | KD_nabbrev of kind * id * name_scm_opt * nexp (* $Nat$-expression abbreviation *) + | KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *) + | KD_record of kind * id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *) + | KD_variant of kind * id * name_scm_opt * typquant * list type_union * bool (* union type definition *) + | KD_enum of kind * id * name_scm_opt * list id * bool (* enumeration type definition *) + | KD_register of kind * id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) -and fexp 'a = - | FE_aux of (fexp_aux 'a) * annot 'a -and fexps_aux 'a = (* Field-expression list *) - | FES_Fexps of list (fexp 'a) * bool +type type_def_aux 'a = (* type definition body *) + | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) + | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *) + | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* tagged union type definition *) + | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *) + | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) -and fexps 'a = - | FES_aux of (fexps_aux 'a) * annot 'a -and opt_default_aux 'a = (* Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map *) - | Def_val_empty - | Def_val_dec of (exp 'a) +type kind_def 'a = + | KD_aux of (kind_def_aux 'a) * annot 'a -and opt_default 'a = - | Def_val_aux of (opt_default_aux 'a) * annot 'a -and pexp_aux 'a = (* Pattern match *) - | Pat_exp of (pat 'a) * (exp 'a) +type type_def 'a = + | TD_aux of (type_def_aux 'a) * annot 'a -and pexp 'a = - | Pat_aux of (pexp_aux 'a) * annot 'a -and letbind_aux 'a = (* Let binding *) - | LB_val_explicit of typschm * (pat 'a) * (exp 'a) (* value binding, explicit type ((pat 'a) must be total) *) - | LB_val_implicit of (pat 'a) * (exp 'a) (* value binding, implicit type ((pat 'a) must be total) *) +let rec remove_one i l = + match l with + | [] -> [] + | i2::l2 -> if i2 = i then l2 else i2::(remove_one i l2) +end -and letbind 'a = - | LB_aux of (letbind_aux 'a) * annot 'a +let rec remove_from l l2 = + match l2 with + | [] -> l + | i::l2' -> remove_from (remove_one i l) l2' +end +let disjoint s1 s2 = Set.null (s1 inter s2) -type reg_id 'a = - | RI_aux of (reg_id_aux 'a) * annot 'a +let rec disjoint_all sets = + match sets with + | [] -> true + | s1::[] -> true + | s1::s2::sets -> (disjoint s1 s2) && (disjoint_all (s2::sets)) +end -type type_union_aux = (* Type union constructors *) - | Tu_id of id - | Tu_ty_id of typ * id +type ne = (* internal numeric expressions *) + | Ne_id of x + | Ne_var of x + | Ne_const of integer + | Ne_inf + | Ne_mult of ne * ne + | Ne_add of list ne + | Ne_minus of ne * ne + | Ne_exp of ne + | Ne_unary of ne -type name_scm_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) - | Name_sect_none - | Name_sect_some of string +type t = (* Internal types *) + | T_id of x + | T_var of x + | T_fn of t * t * effect + | T_tup of list t + | T_app of x * t_args + | T_abbrev of t * t +and t_arg = (* Argument to type constructors *) + | T_arg_typ of t + | T_arg_nexp of ne + | T_arg_effect of effect + | T_arg_order of order -type effect_opt_aux = (* Optional effect annotation for functions *) - | Effect_opt_pure (* sugar for empty effect set *) - | Effect_opt_effect of effect +and t_args = (* Arguments to type constructors *) + | T_args of list t_arg -type funcl_aux 'a = (* Function clause *) - | FCL_Funcl of id * (pat 'a) * (exp 'a) +type k = (* Internal kinds *) + | Ki_typ + | Ki_nat + | Ki_ord + | Ki_efct + | Ki_ctor of list k * k + | Ki_infer (* Representing an unknown kind, inferred by context *) -type rec_opt_aux = (* Optional recursive annotation for functions *) - | Rec_nonrec (* non-recursive *) - | Rec_rec (* recursive *) +type tid = (* A type identifier or type variable *) + | Tid_id of id + | Tid_var of kid -type tannot_opt_aux = (* Optional type annotation for functions *) - | Typ_annot_opt_some of typquant * typ +type kinf = (* Whether a kind is default or from a local binding *) + | Kinf_k of k + | Kinf_def of k -type alias_spec_aux 'a = (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *) - | AL_subreg of (reg_id 'a) * id - | AL_bit of (reg_id 'a) * (exp 'a) - | AL_slice of (reg_id 'a) * (exp 'a) * (exp 'a) - | AL_concat of (reg_id 'a) * (reg_id 'a) +type nec = (* Numeric expression constraints *) + | Nec_lteq of ne * ne + | Nec_eq of ne * ne + | Nec_gteq of ne * ne + | Nec_in of x * list integer + | Nec_cond of list nec * list nec + | Nec_branch of list nec -type type_union = - | Tu_aux of type_union_aux * l +type tag = (* Data indicating where the identifier arises and thus information necessary in compilation *) + | Tag_empty + | Tag_intro (* Denotes an assignment and lexp that introduces a binding *) + | Tag_set (* Denotes an expression that mutates a local variable *) + | Tag_tuple_assign (* Denotes an assignment with a tuple lexp *) + | Tag_global (* Globally let-bound or enumeration based value/variable *) + | Tag_ctor (* Data constructor from a type union *) + | Tag_extern of maybe string (* External function, specied only with a val statement *) + | Tag_default (* Type has come from default declaration, identifier may not be bound locally *) + | Tag_spec + | Tag_enum of integer + | Tag_alias + | Tag_unknown of maybe string (* Tag to distinguish an unknown path from a non-analysis non deterministic path *) -type index_range_aux = (* index specification, for bitfields in register types *) - | BF_single of integer (* single index *) - | BF_range of integer * integer (* index range *) - | BF_concat of index_range * index_range (* concatenation of index ranges *) +type tinf = (* Type variables, type, and constraints, bound to an identifier *) + | Tinf_typ of t + | Tinf_quant_typ of (map tid kinf) * list nec * tag * t -and index_range = - | BF_aux of index_range_aux * l +type conformsto = (* how much conformance does overloading need *) + | Conformsto_full + | Conformsto_parm -type name_scm_opt = - | Name_sect_aux of name_scm_opt_aux * l +type widennum = + | Widennum_widen + | Widennum_dont + | Widennum_dontcare -type effect_opt = - | Effect_opt_aux of effect_opt_aux * l +type widenvec = + | Widenvec_widen + | Widenvec_dont + | Widenvec_dontcare -type funcl 'a = - | FCL_aux of (funcl_aux 'a) * annot 'a +type widening = (* Should we widen vector start locations, should we widen atoms and ranges *) + | Widening_w of widennum * widenvec -type rec_opt = - | Rec_aux of rec_opt_aux * l +type tinflist = (* In place so that a list of tinfs can be referred to without the dot form *) + | Tinfs_empty + | Tinfs_ls of list tinf -type tannot_opt = - | Typ_annot_opt_aux of tannot_opt_aux * l + type definition_env = + | DenvEmp + | Denv of (map tid kinf) * (map (list (id*t)) tinf) * (map t (list (nat*id))) -type alias_spec 'a = - | AL_aux of (alias_spec_aux 'a) * annot 'a +let blength (bit) = Ne_const 8 +let hlength (bit) = Ne_const 8 + type env = + | EnvEmp + | Env of (map id tinf) * definition_env -type default_spec_aux 'a = (* Default kinding or typing assumption *) - | DT_kind of base_kind * kid - | DT_order of order - | DT_typ of typschm * id + type inf = + | Iemp + | Inf of (list nec) * effect + val denv_union : definition_env -> definition_env -> definition_env + let denv_union de1 de2 = + match (de1,de2) with + | (DenvEmp,de2) -> de2 + | (de1,DenvEmp) -> de1 + | ((Denv ke1 re1 ee1),(Denv ke2 re2 ee2)) -> + Denv (ke1 union ke2) (re1 union re2) (ee1 union ee2) + end -type type_def_aux 'a = (* Type definition body *) - | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) - | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *) - | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* union type definition *) - | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *) - | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) + val env_union : env -> env -> env + let env_union e1 e2 = + match (e1,e2) with + | (EnvEmp,e2) -> e2 + | (e1,EnvEmp) -> e1 + | ((Env te1 de1),(Env te2 de2)) -> + Env (te1 union te2) (denv_union de1 de2) + end +let inf_union i1 i2 = + match (i1,i2) with + | (Iemp,i2) -> i2 + | (i1,Iemp) -> i1 + | (Inf n1 e1,Inf n2 e2) -> (Inf (n1++n2) (effect_union e1 e2)) + end -type val_spec_aux 'a = (* Value type specification *) - | VS_val_spec of typschm * id - | VS_extern_no_rename of typschm * id - | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *) +let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should actually build a fresh string*) -type kind_def_aux 'a = (* Definition body for elements of kind; many are shorthands for type\_defs *) - | KD_nabbrev of kind * id * name_scm_opt * nexp (* nexp abbreviation *) - | KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *) - | KD_record of kind * id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *) - | KD_variant of kind * id * name_scm_opt * typquant * list type_union * bool (* union type definition *) - | KD_enum of kind * id * name_scm_opt * list id * bool (* enumeration type definition *) - | KD_register of kind * id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) +type I = inf -type scattered_def_aux 'a = (* Function and type union definitions that can be spread across - a file. Each one must end in $id$ *) - | SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *) - | SD_scattered_funcl of (funcl 'a) (* scattered function definition clause *) - | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *) - | SD_scattered_unioncl of id * type_union (* scattered union definition member *) - | SD_scattered_end of id (* scattered definition end *) +type E = env -type fundef_aux 'a = (* Function definition *) - | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a) +type tannot = maybe (t * tag * list nec * effect * effect) -type dec_spec_aux 'a = (* Register declarations *) - | DEC_reg of typ * id - | DEC_alias of id * (alias_spec 'a) - | DEC_typ_alias of typ * id * (alias_spec 'a) -type default_spec 'a = - | DT_aux of (default_spec_aux 'a) * l +type i_direction = + | IInc + | IDec -type type_def 'a = - | TD_aux of (type_def_aux 'a) * annot 'a +type reg_id_aux 'a = + | RI_id of id -type val_spec 'a = - | VS_aux of (val_spec_aux 'a) * annot 'a +type reg_form = + | Form_Reg of id * tannot * i_direction + | Form_SubReg of id * reg_form * index_range -type kind_def 'a = - | KD_aux of (kind_def_aux 'a) * annot 'a +type ctor_kind = + | C_Enum of nat + | C_Union -type scattered_def 'a = - | SD_aux of (scattered_def_aux 'a) * annot 'a +type reg_id 'a = + | RI_aux of (reg_id_aux 'a) * annot 'a -type fundef 'a = - | FD_aux of (fundef_aux 'a) * annot 'a +type exp_aux 'a = (* expression *) + | E_block of list (exp 'a) (* sequential block *) + | E_nondet of list (exp 'a) (* nondeterministic block *) + | E_id of id (* identifier *) + | E_lit of lit (* literal constant *) + | E_cast of typ * (exp 'a) (* cast *) + | E_app of id * list (exp 'a) (* function application *) + | E_app_infix of (exp 'a) * id * (exp 'a) (* infix function application *) + | E_tuple of list (exp 'a) (* tuple *) + | E_if of (exp 'a) * (exp 'a) * (exp 'a) (* conditional *) + | E_for of id * (exp 'a) * (exp 'a) * (exp 'a) * order * (exp 'a) (* loop *) + | E_vector of list (exp 'a) (* vector (indexed from 0) *) + | E_vector_indexed of list (integer * (exp 'a)) * (opt_default 'a) (* vector (indexed consecutively) *) + | E_vector_access of (exp 'a) * (exp 'a) (* vector access *) + | E_vector_subrange of (exp 'a) * (exp 'a) * (exp 'a) (* subvector extraction *) + | E_vector_update of (exp 'a) * (exp 'a) * (exp 'a) (* vector functional update *) + | E_vector_update_subrange of (exp 'a) * (exp 'a) * (exp 'a) * (exp 'a) (* vector subrange update, with vector *) + | E_vector_append of (exp 'a) * (exp 'a) (* vector concatenation *) + | E_list of list (exp 'a) (* list *) + | E_cons of (exp 'a) * (exp 'a) (* cons *) + | E_record of (fexps 'a) (* struct *) + | E_record_update of (exp 'a) * (fexps 'a) (* functional update of struct *) + | E_field of (exp 'a) * id (* field projection from struct *) + | E_case of (exp 'a) * list (pexp 'a) (* pattern matching *) + | E_let of (letbind 'a) * (exp 'a) (* let expression *) + | E_assign of (lexp 'a) * (exp 'a) (* imperative assignment *) + | E_sizeof of nexp (* the value of nexp at run time *) + | E_return of (exp 'a) (* return (exp 'a) from current function *) + | E_exit of (exp 'a) (* halt all current execution *) + | E_assert of (exp 'a) * (exp 'a) (* halt with error (exp 'a) when not (exp 'a) *) + | E_internal_cast of annot 'a * (exp 'a) (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *) + | E_internal_exp of annot 'a (* This is an internal use for passing nexp information to library functions, postponed for constraint solving *) + | E_sizeof_internal of annot 'a (* For sizeof during type checking, to replace nexp with internal n *) + | E_internal_exp_user of annot 'a * annot 'a (* This is like the above but the user has specified an implicit parameter for the current function *) + | E_comment of string (* For generated unstructured comments *) + | E_comment_struc of (exp 'a) (* For generated structured comments *) + | E_internal_let of (lexp 'a) * (exp 'a) * (exp 'a) (* This is an internal node for compilation that demonstrates the scope of a local mutable variable *) + | E_internal_plet of (pat 'a) * (exp 'a) * (exp 'a) (* This is an internal node, used to distinguised some introduced lets during processing from original ones *) + | E_internal_return of (exp 'a) (* For internal use to embed into monad definition *) + | E_internal_value of value (* For internal use in interpreter to wrap pre-evaluated values when returning an action *) +and exp 'a = + | E_aux of (exp_aux 'a) * annot 'a -type dec_spec 'a = - | DEC_aux of (dec_spec_aux 'a) * annot 'a +and value = (* interpreter evaluated value *) + | V_boxref of nat * t + | V_lit of lit + | V_tuple of list value + | V_list of list value + | V_vector of nat * i_direction * list value + | V_vector_sparse of nat * nat * i_direction * list (nat * value) * value + | V_record of t * list (id * value) + | V_ctor of id * t * ctor_kind * value + | V_unknown + | V_register of reg_form + | V_register_alias of alias_spec tannot * tannot + | V_track of value * set reg_form +and lexp_aux 'a = (* lvalue expression *) + | LEXP_id of id (* identifier *) + | LEXP_memory of id * list (exp 'a) (* memory or register write via function call *) + | LEXP_cast of typ * id (* cast *) + | LEXP_tup of list (lexp 'a) (* multiple (non-memory) assignment *) + | LEXP_vector of (lexp 'a) * (exp 'a) (* vector element *) + | LEXP_vector_range of (lexp 'a) * (exp 'a) * (exp 'a) (* subvector *) + | LEXP_field of (lexp 'a) * id (* struct field *) -type dec_comm 'a = (* Top-level generated comments *) - | DC_comm of string (* generated unstructured comment *) - | DC_comm_struct of (def 'a) (* generated structured comment *) +and lexp 'a = + | LEXP_aux of (lexp_aux 'a) * annot 'a -and def 'a = (* Top-level definition *) - | DEF_kind of (kind_def 'a) (* definition of named kind identifiers *) - | DEF_type of (type_def 'a) (* type definition *) - | DEF_fundef of (fundef 'a) (* function definition *) - | DEF_val of (letbind 'a) (* value definition *) - | DEF_spec of (val_spec 'a) (* top-level type constraint *) - | DEF_default of (default_spec 'a) (* default kind and type assumptions *) - | DEF_scattered of (scattered_def 'a) (* scattered function and type definition *) - | DEF_reg_dec of (dec_spec 'a) (* register declaration *) - | DEF_comm of (dec_comm 'a) (* generated comments *) +and fexp_aux 'a = (* field expression *) + | FE_Fexp of id * (exp 'a) +and fexp 'a = + | FE_aux of (fexp_aux 'a) * annot 'a -type defs 'a = (* Definition sequence *) - | Defs of list (def 'a) +and fexps_aux 'a = (* field expression list *) + | FES_Fexps of list (fexp 'a) * bool +and fexps 'a = + | FES_aux of (fexps_aux 'a) * annot 'a -let rec remove_one i l = - match l with - | [] -> [] - | i2::l2 -> if i2 = i then l2 else i2::(remove_one i l2) -end +and opt_default_aux 'a = (* optional default value for indexed vector expressions *) + | Def_val_empty + | Def_val_dec of (exp 'a) -let rec remove_from l l2 = - match l2 with - | [] -> l - | i::l2' -> remove_from (remove_one i l) l2' -end +and opt_default 'a = + | Def_val_aux of (opt_default_aux 'a) * annot 'a -let disjoint s1 s2 = Set.null (s1 inter s2) +and pexp_aux 'a = (* pattern match *) + | Pat_exp of (pat 'a) * (exp 'a) -let rec disjoint_all sets = - match sets with - | [] -> true - | s1::[] -> true - | s1::s2::sets -> (disjoint s1 s2) && (disjoint_all (s2::sets)) -end +and pexp 'a = + | Pat_aux of (pexp_aux 'a) * annot 'a +and letbind_aux 'a = (* let binding *) + | LB_val_explicit of typschm * (pat 'a) * (exp 'a) (* let, explicit type ((pat 'a) must be total) *) + | LB_val_implicit of (pat 'a) * (exp 'a) (* let, implicit type ((pat 'a) must be total) *) -type ne = (* internal numeric expressions *) - | Ne_id of x - | Ne_var of x - | Ne_const of integer - | Ne_inf - | Ne_mult of ne * ne - | Ne_add of list ne - | Ne_minus of ne * ne - | Ne_exp of ne - | Ne_unary of ne +and letbind 'a = + | LB_aux of (letbind_aux 'a) * annot 'a +and alias_spec_aux 'a = (* register alias expression forms *) + | AL_subreg of (reg_id 'a) * id + | AL_bit of (reg_id 'a) * (exp 'a) + | AL_slice of (reg_id 'a) * (exp 'a) * (exp 'a) + | AL_concat of (reg_id 'a) * (reg_id 'a) -type k = (* Internal kinds *) - | Ki_typ - | Ki_nat - | Ki_ord - | Ki_efct - | Ki_ctor of list k * k - | Ki_infer (* Representing an unknown kind, inferred by context *) +and alias_spec 'a = + | AL_aux of (alias_spec_aux 'a) * annot 'a -type nec = (* Numeric expression constraints *) - | Nec_lteq of ne * ne - | Nec_eq of ne * ne - | Nec_gteq of ne * ne - | Nec_in of x * list integer - | Nec_cond of list nec * list nec - | Nec_branch of list nec +type funcl_aux 'a = (* function clause *) + | FCL_Funcl of id * (pat 'a) * (exp 'a) -type tid = (* A type identifier or type variable *) - | Tid_id of id - | Tid_var of kid +type rec_opt_aux = (* optional recursive annotation for functions *) + | Rec_nonrec (* non-recursive *) + | Rec_rec (* recursive *) -type kinf = (* Whether a kind is default or from a local binding *) - | Kinf_k of k - | Kinf_def of k +type tannot_opt_aux = (* optional type annotation for functions *) + | Typ_annot_opt_some of typquant * typ -type t = (* Internal types *) - | T_id of x - | T_var of x - | T_fn of t * t * effect - | T_tup of list t - | T_app of x * t_args - | T_abbrev of t * t +type effect_opt_aux = (* optional effect annotation for functions *) + | Effect_opt_pure (* sugar for empty effect set *) + | Effect_opt_effect of effect -and t_arg = (* Argument to type constructors *) - | T_arg_typ of t - | T_arg_nexp of ne - | T_arg_effect of effect - | T_arg_order of order -and t_args = (* Arguments to type constructors *) - | T_args of list t_arg +type funcl 'a = + | FCL_aux of (funcl_aux 'a) * annot 'a -type tag = (* Data indicating where the identifier arises and thus information necessary in compilation *) - | Tag_empty - | Tag_intro (* Denotes an assignment and lexp that introduces a binding *) - | Tag_set (* Denotes an expression that mutates a local variable *) - | Tag_tuple_assign (* Denotes an assignment with a tuple lexp *) - | Tag_global (* Globally let-bound or enumeration based value/variable *) - | Tag_ctor (* Data constructor from a type union *) - | Tag_extern of maybe string (* External function, specied only with a val statement *) - | Tag_default (* Type has come from default declaration, identifier may not be bound locally *) - | Tag_spec - | Tag_enum of integer - | Tag_alias - | Tag_unknown of maybe string (* Tag to distinguish an unknown path from a non-analysis non deterministic path *) +type rec_opt = + | Rec_aux of rec_opt_aux * l -type tinf = (* Type variables, type, and constraints, bound to an identifier *) - | Tinf_typ of t - | Tinf_quant_typ of (map tid kinf) * list nec * tag * t +type tannot_opt = + | Typ_annot_opt_aux of tannot_opt_aux * l -type conformsto = (* how much conformance does overloading need *) - | Conformsto_full - | Conformsto_parm +type effect_opt = + | Effect_opt_aux of effect_opt_aux * l -type widenvec = - | Widenvec_widen - | Widenvec_dont - | Widenvec_dontcare +type val_spec_aux 'a = (* value type specification *) + | VS_val_spec of typschm * id (* specify the type of an upcoming definition *) + | VS_extern_no_rename of typschm * id (* specify the type of an external function *) + | VS_extern_spec of typschm * id * string (* specify the type of a function from Lem *) -type widennum = - | Widennum_widen - | Widennum_dont - | Widennum_dontcare +type fundef_aux 'a = (* function definition *) + | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a) -type tinflist = (* In place so that a list of tinfs can be referred to without the dot form *) - | Tinfs_empty - | Tinfs_ls of list tinf +type scattered_def_aux 'a = (* scattered function and union type definitions *) + | SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *) + | SD_scattered_funcl of (funcl 'a) (* scattered function definition clause *) + | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *) + | SD_scattered_unioncl of id * type_union (* scattered union definition member *) + | SD_scattered_end of id (* scattered definition end *) -type widening = (* Should we widen vector start locations, should we widen atoms and ranges *) - | Widening_w of widennum * widenvec +type default_spec_aux 'a = (* default kinding or typing assumption *) + | DT_order of order + | DT_kind of base_kind * kid + | DT_typ of typschm * id - type definition_env = - | DenvEmp - | Denv of (map tid kinf) * (map (list (id*t)) tinf) * (map t (list (nat*id))) +type dec_spec_aux 'a = (* register declarations *) + | DEC_reg of typ * id + | DEC_alias of id * (alias_spec 'a) + | DEC_typ_alias of typ * id * (alias_spec 'a) -let blength (bit) = Ne_const 8 -let hlength (bit) = Ne_const 8 - type env = - | EnvEmp - | Env of (map id tinf) * definition_env +type val_spec 'a = + | VS_aux of (val_spec_aux 'a) * annot 'a - type inf = - | Iemp - | Inf of (list nec) * effect - val denv_union : definition_env -> definition_env -> definition_env - let denv_union de1 de2 = - match (de1,de2) with - | (DenvEmp,de2) -> de2 - | (de1,DenvEmp) -> de1 - | ((Denv ke1 re1 ee1),(Denv ke2 re2 ee2)) -> - Denv (ke1 union ke2) (re1 union re2) (ee1 union ee2) - end +type fundef 'a = + | FD_aux of (fundef_aux 'a) * annot 'a - val env_union : env -> env -> env - let env_union e1 e2 = - match (e1,e2) with - | (EnvEmp,e2) -> e2 - | (e1,EnvEmp) -> e1 - | ((Env te1 de1),(Env te2 de2)) -> - Env (te1 union te2) (denv_union de1 de2) - end -let inf_union i1 i2 = - match (i1,i2) with - | (Iemp,i2) -> i2 - | (i1,Iemp) -> i1 - | (Inf n1 e1,Inf n2 e2) -> (Inf (n1++n2) (effect_union e1 e2)) - end +type scattered_def 'a = + | SD_aux of (scattered_def_aux 'a) * annot 'a -let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should actually build a fresh string*) +type default_spec 'a = + | DT_aux of (default_spec_aux 'a) * l -type E = env +type dec_spec 'a = + | DEC_aux of (dec_spec_aux 'a) * annot 'a -type I = inf +type dec_comm 'a = (* top-level generated comments *) + | DC_comm of string (* generated unstructured comment *) + | DC_comm_struct of (def 'a) (* generated structured comment *) + +and def 'a = (* top-level definition *) + | DEF_kind of (kind_def 'a) (* definition of named kind identifiers *) + | DEF_type of (type_def 'a) (* type definition *) + | DEF_fundef of (fundef 'a) (* function definition *) + | DEF_val of (letbind 'a) (* value definition *) + | DEF_spec of (val_spec 'a) (* top-level type constraint *) + | DEF_default of (default_spec 'a) (* default kind and type assumptions *) + | DEF_scattered of (scattered_def 'a) (* scattered function and type definition *) + | DEF_reg_dec of (dec_spec 'a) (* register declaration *) + | DEF_comm of (dec_comm 'a) (* generated comments *) + + +type defs 'a = (* definition sequence *) + | Defs of list (def 'a) diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index f0d7dec4..69958109 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -51,13 +51,13 @@ open import Interp_ast open import Sail_impl_base open import Interp_interface -val intern_reg_value : register_value -> Interp.value -val intern_mem_value : interp_mode -> direction -> memory_value -> Interp.value -val extern_reg_value : reg_name -> Interp.value -> register_value -val extern_with_track: forall 'a. interp_mode -> (Interp.value -> 'a) -> Interp.value -> ('a * maybe (list reg_name)) -val extern_vector_value: Interp.value -> list byte_lifted -val extern_mem_value : Interp.value -> memory_value -val extern_reg : Interp.reg_form -> maybe (nat * nat) -> reg_name +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 = <| Interp.eager_eval = eager_eval; Interp.track_values = tracking_values; Interp.track_lmem = false|>;; @@ -71,15 +71,15 @@ let make_eager_mode mode = <| internal_mode = <|mode.internal_mode with Interp.e let make_default_mode = fun () -> <|internal_mode = make_interpreter_mode false false|>;; let bitl_to_ibit = function - | Bitl_zero -> (Interp.V_lit (L_aux L_zero Interp_ast.Unknown)) - | Bitl_one -> (Interp.V_lit (L_aux L_one Interp_ast.Unknown)) - | Bitl_undef -> (Interp.V_lit (L_aux L_undef Interp_ast.Unknown)) - | Bitl_unknown -> Interp.V_unknown + | 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.V_lit (L_aux L_zero Interp_ast.Unknown)) - | Bitc_one -> (Interp.V_lit (L_aux L_one Interp_ast.Unknown)) + | 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 @@ -99,13 +99,13 @@ end let bitl_from_ibit b = let b = Interp.detaint b in match b with - | Interp.V_lit (L_aux L_zero _) -> Bitl_zero - | Interp.V_vector _ _ [Interp.V_lit (L_aux L_zero _)] -> Bitl_zero - | Interp.V_lit (L_aux L_one _) -> Bitl_one - | Interp.V_vector _ _ [Interp.V_lit (L_aux L_one _)] -> Bitl_one - | Interp.V_lit (L_aux L_undef _) -> Bitl_undef - | Interp.V_vector _ _ [Interp.V_lit (L_aux L_undef _)] -> Bitl_undef - | Interp.V_unknown -> Bitl_unknown + | 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 @@ -116,10 +116,10 @@ let bits_from_ibits l = List.map (fun b -> let b = Interp.detaint b in match b with - | Interp.V_lit (L_aux L_zero _) -> Bitc_zero - | Interp.V_vector _ _ [Interp.V_lit (L_aux L_zero _)] -> Bitc_zero - | Interp.V_lit (L_aux L_one _) -> Bitc_one - | Interp.V_vector _ _ [Interp.V_lit (L_aux L_one _)] -> Bitc_one + | 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 @@ -138,23 +138,23 @@ let bits_to_word8 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.IInc - | D_decreasing -> Interp.IDec + | D_increasing -> Interp_ast.IInc + | D_decreasing -> Interp_ast.IDec end let extern_direction = function - | Interp.IInc -> D_increasing - | Interp.IDec -> D_decreasing + | 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.V_vector (if Interp.is_inc(direction) then 0 else (List.length(bits) - 1)) direction bits + 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.V_vector v.rv_start_internal (intern_direction v.rv_dir) (bitls_to_ibits v.rv_bits) + | _ -> 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 = @@ -162,12 +162,12 @@ let intern_mem_value mode direction v = $> List.concatMap (fun (Byte_lifted bits) -> bitls_to_ibits bits) $> fun bits -> let direction = intern_direction direction in - Interp.V_vector (if Interp.is_inc direction then 0 else (List.length bits) -1) direction bits + 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.V_vector (if Interp.is_inc direction then 0 else (List.length(bits) -1)) direction bits + 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 @@ -179,25 +179,25 @@ let extern_slice (d:direction) (start:nat) ((i,j):(nat*nat)) = end let extern_reg r slice = match (r,slice) with - | (Interp.Reg (Id_aux (Id x) _) (Just(t,_,_,_,_)) dir,Nothing) -> + | (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.Reg (Id_aux (Id x) _) (Just(t,_,_,_,_)) dir,Just(i1,i2)) -> + | (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.SubReg (Id_aux (Id x) _) ((Interp.Reg (Id_aux (Id y) _) _ dir) as main_r) (BF_aux(BF_single i) _), + | (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.SubReg (Id_aux (Id x) _) ((Interp.Reg (Id_aux (Id y) _) _ dir) as main_r) (BF_aux(BF_range i 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) _), 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.SubReg (Id_aux (Id x) _) - ((Interp.Reg (Id_aux (Id y) _) _ dir) as main_r) (BF_aux(BF_range i j) _), Just(i1,j1)) -> + | (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)) @@ -207,8 +207,8 @@ end let rec extern_reg_value reg_name v = match v with - | Interp.V_track v regs -> extern_reg_value reg_name v - | Interp.V_vector_sparse fst stop inc bits default -> + | 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) = @@ -226,13 +226,13 @@ let rec extern_reg_value reg_name v = slice_start, dir) end) in let bit_list = (match v with - | Interp.V_vector fst dir bits -> bitls_from_ibits bits - | Interp.V_lit (L_aux L_zero _) -> [Bitl_zero] - | Interp.V_lit (L_aux L_false _) -> [Bitl_zero] - | Interp.V_lit (L_aux L_one _) -> [Bitl_one] - | Interp.V_lit (L_aux L_true _) -> [Bitl_one] - | Interp.V_lit (L_aux L_undef _) -> [Bitl_undef] - | Interp.V_unknown -> [Bitl_unknown] + | 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; @@ -242,7 +242,7 @@ let rec extern_reg_value reg_name v = end let extern_with_track mode f = function - | Interp.V_track v regs -> + | 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))) @@ -251,13 +251,13 @@ let extern_with_track mode f = function end let rec extern_vector_value v = match v with - | Interp.V_vector _fst _inc bits -> + | Interp_ast.V_vector _fst _inc bits -> bitls_from_ibits bits $> to_bytes - | Interp.V_vector_sparse _fst _stop _inc _bits _default -> + | Interp_ast.V_vector_sparse _fst _stop _inc _bits _default -> Interp_lib.fill_in_sparse v $> extern_vector_value - | Interp.V_track v _ -> extern_vector_value v + | 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 @@ -265,19 +265,19 @@ 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.V_track v regs,_) -> extern_ifield_value i_name field_name v ftyp - | (Interp.V_vector fst inc bits,_) -> bits_from_ibits bits - | (Interp.V_vector_sparse fst stop inc bits default,_) -> + | (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.V_lit (L_aux L_zero _),_) -> [Bitc_zero] - | (Interp.V_lit (L_aux L_false _),_) -> [Bitc_zero] - | (Interp.V_lit (L_aux L_one _),_) -> [Bitc_one] - | (Interp.V_lit (L_aux L_true _),_) -> [Bitc_one] - | (Interp.V_lit (L_aux (L_num i) _),Range (Just n)) -> bit_list_of_integer n i - | (Interp.V_lit (L_aux (L_num i) _),Enum _ n) -> bit_list_of_integer n i - | (Interp.V_lit (L_aux (L_num i) _),_) -> bit_list_of_integer 64 i - | (Interp.V_ctor _ _ (Interp.C_Enum i) _,Enum _ n) -> bit_list_of_integer n (integerFromNat i) - | (Interp.V_ctor _ _ (Interp.C_Enum i) _,_) -> bit_list_of_integer 64 (integerFromNat i) + | (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) @@ -351,8 +351,8 @@ let initial_instruction_state top_level main args = type interp_value_helper_mode = Ivh_translate | Ivh_decode | Ivh_unsupported | Ivh_illegal | Ivh_analysis type interp_value_return = - | Ivh_value of Interp.value - | Ivh_value_after_exn of Interp.value + | 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 arg ivh_mode err_str instr direction registers events exn_seen thunk = @@ -374,8 +374,8 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev | Ivh_analysis -> (Ivh_value value, events_out) | _ -> (match value with - | Interp.V_ctor (Id_aux (Id "Some") _) _ _ vinstr -> (Ivh_value vinstr,events_out) - | Interp.V_ctor (Id_aux (Id "None") _) _ _ _ -> + | 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) @@ -395,7 +395,7 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev end | (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) _)) -> + | 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,_,_) -> @@ -403,8 +403,8 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev (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.Reg (Id_aux (Id i) _) _ _ -> i - | Interp.SubReg (Id_aux (Id i) _) (Interp.Reg (Id_aux (Id i2) _) _ _) _ -> i2 ^ "." ^ i + | 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)), @@ -466,7 +466,7 @@ let translate_address top_level end_flag thunk_name registers address = 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.IInc else Interp.IDec 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 (Just (Opcode bytes)) Ivh_translate val_str ("",[]) internal_direction registers [] false @@ -489,7 +489,7 @@ end let value_of_instruction_param direction (name,typ,v) = let vec = intern_ifield_value direction v in let v = match vec with - | Interp.V_vector start dir bits -> + | 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 @@ -500,8 +500,8 @@ let value_of_instruction_param direction (name,typ,v) = end in v let intern_instruction direction (name,parms) = - Interp.V_ctor (Interp.id_of_string name) (T_id "ast") Interp.C_Union - (Interp.V_tuple (List.map (value_of_instruction_param direction) 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 mode = make_mode true false in @@ -510,7 +510,7 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis 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.IInc else Interp.IDec 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 Nothing Ivh_analysis val_str ("",[]) internal_direction registers [] false @@ -523,31 +523,31 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis match (analysis_or_error) with | Ivh_value analysis -> (match analysis with - | Interp.V_tuple [Interp.V_list regs1; - Interp.V_list regs2; - Interp.V_list regs3; - Interp.V_list nias; + | 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.V_ctor (Id_aux (Id "RFull") _) _ _ (Interp.V_lit (L_aux (L_string n) _)) -> + | 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.V_ctor (Id_aux (Id "RSlice") _) _ _ - (Interp.V_tuple [Interp.V_lit (L_aux (L_string n) _); - Interp.V_lit (L_aux (L_num s1) _); - Interp.V_lit (L_aux (L_num s2) _);]) -> + | 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.V_ctor (Id_aux (Id "RSliceBit") _) _ _ - (Interp.V_tuple [Interp.V_lit (L_aux (L_string n) _); - Interp.V_lit (L_aux (L_num s) _);]) -> + | 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.V_ctor (Id_aux (Id "RField") _) _ _ - (Interp.V_tuple [Interp.V_lit (L_aux (L_string n) _); - Interp.V_lit (L_aux (L_string f) _);]) -> + | 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 @@ -556,23 +556,23 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis | Just addr -> addr | Nothing -> failwith "get_nia encountered invalid address" end in let dia_to_dia = function - | Interp.V_ctor (Id_aux (Id "DIAFP_none") _) _ _ _ -> DIA_none - | Interp.V_ctor (Id_aux (Id "DIAFP_concrete") _) _ _ address -> + | 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.V_ctor (Id_aux (Id "DIAFP_reg") _) _ _ reg -> DIA_register (reg_to_reg_name reg) + | 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.V_ctor (Id_aux (Id "NIAFP_successor") _) _ _ _-> NIA_successor - | Interp.V_ctor (Id_aux (Id "NIAFP_concrete_address") _) _ _ address -> + | 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.V_ctor (Id_aux (Id "NIAFP_LR") _) _ _ _ -> NIA_LR - | Interp.V_ctor (Id_aux (Id "NIAFP_CTR") _) _ _ _ -> NIA_CTR - | Interp.V_ctor (Id_aux (Id "NIAFP_register") _) _ _ reg -> + | 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.V_ctor (Id_aux (Id "IK_barrier") _) _ _ - (Interp.V_ctor (Id_aux (Id b) _) _ _ _) -> + | 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 @@ -587,8 +587,8 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis | "Barrier_ISB" -> Barrier_ISB | "Barrier_MIPS_SYNC" -> Barrier_MIPS_SYNC end) - | Interp.V_ctor (Id_aux (Id "IK_mem_read") _) _ _ - (Interp.V_ctor (Id_aux (Id r) _) _ _ _) -> + | 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 @@ -597,8 +597,8 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis | "Read_exclusive_acquire" -> Read_exclusive_acquire | "Read_stream" -> Read_stream end) - | Interp.V_ctor (Id_aux (Id "IK_mem_write") _) _ _ - (Interp.V_ctor (Id_aux (Id w) _) _ _ _) -> + | 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 @@ -606,9 +606,9 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis | "Write_exclusive" -> Write_exclusive | "Write_exclusive_release" -> Write_exclusive_release end) - | Interp.V_ctor (Id_aux (Id "IK_cond_branch") _) _ _ _ -> + | Interp_ast.V_ctor (Id_aux (Id "IK_cond_branch") _) _ _ _ -> IK_cond_branch - | Interp.V_ctor (Id_aux (Id "IK_simple") _) _ _ _ -> + | Interp_ast.V_ctor (Id_aux (Id "IK_simple") _) _ _ _ -> IK_simple | _ -> failwith "Analysis returned unexpected instruction kind" end in @@ -648,15 +648,15 @@ end let interp_value_to_instr_external top_level instr = let (Context (Interp.Env _ instructions _ _ _ _ _ _) _ _ _ _ _ _ _ _ _ _) = top_level in match instr with - | Interp.V_ctor (Id_aux (Id i) _) _ _ parm -> + | 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.V_lit (L_aux L_unit _),[]) -> (name, []) + | (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.V_tuple vals,parms) -> + | (Interp_ast.V_tuple vals,parms) -> (name, (Interp_utilities.map2 (fun value (p_name,ie_typ) -> let t = migrate_typ ie_typ in @@ -675,7 +675,7 @@ let decode_to_instruction top_level registers value : instruction_or_decode_erro let intern_val = intern_opcode direction value in let val_str = Interp.string_of_value intern_val in let (arg,_) = Interp.to_exp mode Interp.eenv intern_val in - let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in + let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in let (instr_decoded_error,events) = interp_to_value_helper (Just value) Ivh_decode val_str ("",[]) internal_direction registers [] false (fun _ -> Interp.resume @@ -729,7 +729,7 @@ let instr_external_to_interp_value top_level instr = let get_value (_,typ,v) = let vec = intern_ifield_value direction v in match vec with - | Interp.V_vector start dir bits -> + | 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 @@ -740,12 +740,12 @@ let instr_external_to_interp_value top_level instr = end in let parmsV = match parms with - | [] -> Interp.V_lit (L_aux L_unit Unknown) - | _ -> Interp.V_tuple (List.map get_value parms) + | [] -> 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.V_ctor (Interp_ast.Id_aux (Interp_ast.Id name) Interp_ast.Unknown) - (T_id "ast") Interp.C_Union parmsV + 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 = @@ -761,7 +761,7 @@ let instruction_to_istate (top_level:context) (((name, parms) as instr):instruct 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.IInc else Interp.IDec 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) @@ -771,7 +771,7 @@ let rec interp_to_outcome mode context thunk = (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.V_track v (Set.fromList [reg_form])) else 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 @@ -798,7 +798,7 @@ let rec interp_to_outcome mode context thunk = | 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.V_tuple ([(bitl_to_ibit tag);(intern_mem_value mode direction v)]))) context) + (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) @@ -844,7 +844,7 @@ let rec interp_to_outcome mode context thunk = | (Just (MV parmf return)) -> let (value, v_tracking) = match (Interp.detaint write_val) with - | Interp.V_tuple[_;v] -> extern_with_track mode extern_mem_value (Interp.retaint write_val v) + | 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 @@ -863,7 +863,7 @@ let rec interp_to_outcome mode context thunk = | (Just (MVT parmf return)) -> let (value, v_tracking) = match (Interp.detaint write_val) with - | Interp.V_tuple[_;v] -> extern_with_track mode extern_mem_value (Interp.retaint write_val v) + | 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 @@ -913,7 +913,7 @@ let rec interp_to_outcome mode context thunk = (Internal (Just name) (Just (fun _ -> Interp.string_of_value value)) (IState next_state context), lm) | Interp.Fail value -> (match value with - | Interp.V_ctor (Id_aux (Id "Some") _) _ _ (Interp.V_lit (L_aux (L_string s) _)) -> (Fail (Just s),lm) + | 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 diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index 0ce7b43a..937db466 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -162,7 +162,7 @@ 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*) +type specification = Interp_ast.defs Interp_ast.tannot (*Deem abstract*) type interpreter_mode = Interp.interp_mode (*Deem abstract*) type interp_mode = <| internal_mode: interpreter_mode |> val make_mode : (*eager*) bool -> (*tracking*) bool -> interp_mode @@ -171,12 +171,12 @@ val tracking_dependencies : interp_mode -> bool (*Map between external functions as preceived from a Sail spec and the actual implementation of the function *) -type external_functions = list (string * (Interp.value -> Interp.value)) +type external_functions = list (string * (Interp_ast.value -> Interp_ast.value)) (*Maps between the memory functions as preceived from a Sail spec and the values needed for actions in the memory model*) type barriers = list (string * barrier_kind) -type memory_parameter_transformer = interp_mode -> Interp.value -> (memory_value * nat * maybe (list reg_name)) -type optional_memory_transformer = interp_mode -> Interp.value -> maybe memory_value +type memory_parameter_transformer = interp_mode -> Interp_ast.value -> (memory_value * nat * maybe (list reg_name)) +type optional_memory_transformer = interp_mode -> Interp_ast.value -> maybe memory_value type memory_read = MR of read_kind * memory_parameter_transformer type memory_reads = list (string * memory_read) type memory_read_tagged = MRT of read_kind * memory_parameter_transformer @@ -264,7 +264,7 @@ val initial_instruction_state : context -> string -> list register_value -> inst (* string is a function name, list of value are the parameters to that function *) type instruction_or_decode_error = - | IDE_instr of instruction * Interp.value + | IDE_instr of instruction * Interp_ast.value | IDE_decode_error of decode_error (** propose to remove the following type and use the above instead *) diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml index b019fb53..a51598b3 100644 --- a/src/lem_interp/pretty_interp.ml +++ b/src/lem_interp/pretty_interp.ml @@ -71,6 +71,92 @@ let pp_format_id (Id_aux(i,_)) = | Id(i) -> i | DeIid(x) -> "(deinfix " ^ x ^ ")" +let lit_to_string = function + | L_unit -> "unit" + | L_zero -> "0b0" + | L_one -> "0b1" + | L_true -> "true" + | L_false -> "false" + | L_num n -> Nat_big_num.to_string n + | L_hex s -> "0x"^s + | L_bin s -> "0b"^s + | L_undef -> "undefined" + | L_string s -> "\"" ^ s ^ "\"" +;; + +let id_to_string = function + | Id_aux(Id s,_) | Id_aux(DeIid s,_) -> s +;; + +let rec loc_to_string = function + | Unknown -> "location unknown" + | Int(s,_) -> s + | Generated l -> "Generated near " ^ loc_to_string l + | Range(s,fline,fchar,tline,tchar) -> + if fline = tline + then sprintf "%s:%d:%d" s fline fchar + else sprintf "%s:%d:%d-%d:%d" s fline fchar tline tchar +;; + +let collapse_leading s = + if String.length s <= 8 then s else + let first_bit = s.[0] in + let templ = sprintf "%c...%c" first_bit first_bit in + + let rec find_first_diff str cha pos = + if pos >= String.length str then None + else if str.[pos] != cha then Some pos + else find_first_diff str cha (pos+1) + in + + match find_first_diff s first_bit 0 with + | None -> templ + | Some pos when pos > 4 -> templ ^ (String.sub s pos ((String.length s)- pos)) + | _ -> s +;; + +(* pp the bytes of a Bytevector as a hex value *) + +let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (function + | Interp_ast.V_lit(L_aux(L_zero, _)) -> "0" + | Interp_ast.V_lit(L_aux(L_one, _)) -> "1" + | Interp_ast.V_lit(L_aux(L_undef, _)) -> "u" + | Interp_ast.V_unknown -> "?" + | v -> (Printf.printf "bitvec found a non bit %s%!\n" (Interp.string_of_value v));assert false) + (List.map Interp.detaint l))) + ;; + + +let rec val_to_string_internal ((Interp.LMem (_,_,memory,_)) as mem) = function + | Interp_ast.V_boxref(n, t) -> val_to_string_internal mem (Pmap.find n memory) + | Interp_ast.V_lit (L_aux(l,_)) -> sprintf "%s" (lit_to_string l) + | Interp_ast.V_tuple l -> + let repr = String.concat ", " (List.map (val_to_string_internal mem) l) in + sprintf "(%s)" repr + | Interp_ast.V_list l -> + let repr = String.concat "; " (List.map (val_to_string_internal mem) l) in + sprintf "[||%s||]" repr + | Interp_ast.V_vector (first_index, inc, l) -> + let last_index = (if (Interp_ast.IInc = inc) then List.length l - 1 else 1 - List.length l) + first_index in + let repr = + try bitvec_to_string l + with Failure _ -> + sprintf "[%s]" (String.concat "; " (List.map (val_to_string_internal mem) l)) in + sprintf "%s [%s..%s]" repr (string_of_int first_index) (string_of_int last_index) + | (Interp_ast.V_vector_sparse(first_index,last_index,inc,l,default) as v) -> + val_to_string_internal mem (Interp_lib.fill_in_sparse v) + | Interp_ast.V_record(_, l) -> + let pp (id, value) = sprintf "%s = %s" (id_to_string id) (val_to_string_internal mem value) in + let repr = String.concat "; " (List.map pp l) in + sprintf "{%s}" repr + | Interp_ast.V_ctor (id,_,_, value) -> + sprintf "%s %s" (id_to_string id) (val_to_string_internal mem value) + | Interp_ast.V_register _ | Interp_ast.V_register_alias _ -> + sprintf "reg-as-value" + | Interp_ast.V_unknown -> "unknown" + | Interp_ast.V_track(v,rs) -> (*"tainted by {" ^ (Interp_utilities.list_to_string Interp.string_of_reg_form "," rs) ^ "} --" ^ *) (val_to_string_internal mem v) +;; + (**************************************************************************** * PPrint-based source-to-source pretty printer ****************************************************************************) @@ -293,108 +379,108 @@ let doc_pat, doc_atomic_pat = in pat, atomic_pat let doc_exp, doc_let = - let rec exp env add_red show_hole_contents e = group (or_exp env add_red show_hole_contents e) - and or_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with + let rec exp env mem add_red show_hole_contents e = group (or_exp env mem add_red show_hole_contents e) + and or_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with | E_app_infix(l,(Id_aux(Id ("|" | "||"),_) as op),r) -> - doc_op (doc_id op) (and_exp env add_red show_hole_contents l) (or_exp env add_red show_hole_contents r) - | _ -> and_exp env add_red show_hole_contents expr - and and_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with + doc_op (doc_id op) (and_exp env mem add_red show_hole_contents l) (or_exp env mem add_red show_hole_contents r) + | _ -> and_exp env mem add_red show_hole_contents expr + and and_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with | E_app_infix(l,(Id_aux(Id ("&" | "&&"),_) as op),r) -> - doc_op (doc_id op) (eq_exp env add_red show_hole_contents l) (and_exp env add_red show_hole_contents r) - | _ -> eq_exp env add_red show_hole_contents expr - and eq_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with + doc_op (doc_id op) (eq_exp env mem add_red show_hole_contents l) (and_exp env mem add_red show_hole_contents r) + | _ -> eq_exp env mem add_red show_hole_contents expr + and eq_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with | E_app_infix(l,(Id_aux(Id ( (* XXX this is not very consistent - is the parser bogus here? *) "=" | "==" | "!=" | ">=" | ">=_s" | ">=_u" | ">" | ">_s" | ">_u" | "<=" | "<=_s" | "<" | "<_s" | "<_si" | "<_u" ),_) as op),r) -> - doc_op (doc_id op) (eq_exp env add_red show_hole_contents l) (at_exp env add_red show_hole_contents r) + doc_op (doc_id op) (eq_exp env mem add_red show_hole_contents l) (at_exp env mem add_red show_hole_contents r) (* XXX assignment should not have the same precedence as equal etc. *) | E_assign(le,exp) -> - doc_op coloneq (doc_lexp env add_red show_hole_contents le) (at_exp env add_red show_hole_contents exp) - | _ -> at_exp env add_red show_hole_contents expr - and at_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with + doc_op coloneq (doc_lexp env mem add_red show_hole_contents le) (at_exp env mem add_red show_hole_contents exp) + | _ -> at_exp env mem add_red show_hole_contents expr + and at_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with | E_app_infix(l,(Id_aux(Id ("@" | "^^" | "^" | "~^"),_) as op),r) -> - doc_op (doc_id op) (cons_exp env add_red show_hole_contents l) (at_exp env add_red show_hole_contents r) - | _ -> cons_exp env add_red show_hole_contents expr - and cons_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with + doc_op (doc_id op) (cons_exp env mem add_red show_hole_contents l) (at_exp env mem add_red show_hole_contents r) + | _ -> cons_exp env mem add_red show_hole_contents expr + and cons_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with | E_vector_append(l,r) -> - doc_op colon (shift_exp env add_red show_hole_contents l) (cons_exp env add_red show_hole_contents r) + doc_op colon (shift_exp env mem add_red show_hole_contents l) (cons_exp env mem add_red show_hole_contents r) | E_cons(l,r) -> - doc_op colon (shift_exp env add_red show_hole_contents l) (cons_exp env add_red show_hole_contents r) - | _ -> shift_exp env add_red show_hole_contents expr - and shift_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with + doc_op colon (shift_exp env mem add_red show_hole_contents l) (cons_exp env mem add_red show_hole_contents r) + | _ -> shift_exp env mem add_red show_hole_contents expr + and shift_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with | E_app_infix(l,(Id_aux(Id (">>" | ">>>" | "<<" | "<<<"),_) as op),r) -> - doc_op (doc_id op) (shift_exp env add_red show_hole_contents l) (plus_exp env add_red show_hole_contents r) - | _ -> plus_exp env add_red show_hole_contents expr - and plus_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with + doc_op (doc_id op) (shift_exp env mem add_red show_hole_contents l) (plus_exp env mem add_red show_hole_contents r) + | _ -> plus_exp env mem add_red show_hole_contents expr + and plus_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with | E_app_infix(l,(Id_aux(Id ("+" | "-"| "+_s" | "-_s" ),_) as op),r) -> - doc_op (doc_id op) (plus_exp env add_red show_hole_contents l) (star_exp env add_red show_hole_contents r) - | _ -> star_exp env add_red show_hole_contents expr - and star_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with + doc_op (doc_id op) (plus_exp env mem add_red show_hole_contents l) (star_exp env mem add_red show_hole_contents r) + | _ -> star_exp env mem add_red show_hole_contents expr + and star_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with | E_app_infix(l,(Id_aux(Id ( "*" | "/" | "div" | "quot" | "rem" | "mod" | "quot_s" | "mod_s" | "*_s" | "*_si" | "*_u" | "*_ui"),_) as op),r) -> - doc_op (doc_id op) (star_exp env add_red show_hole_contents l) (starstar_exp env add_red show_hole_contents r) - | _ -> starstar_exp env add_red show_hole_contents expr - and starstar_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with + doc_op (doc_id op) (star_exp env mem add_red show_hole_contents l) (starstar_exp env mem add_red show_hole_contents r) + | _ -> starstar_exp env mem add_red show_hole_contents expr + and starstar_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with | E_app_infix(l,(Id_aux(Id "**",_) as op),r) -> - doc_op (doc_id op) (starstar_exp env add_red show_hole_contents l) (app_exp env add_red show_hole_contents r) - | E_if _ | E_for _ | E_let _ -> right_atomic_exp env add_red show_hole_contents expr - | _ -> app_exp env add_red show_hole_contents expr - and right_atomic_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with + doc_op (doc_id op) (starstar_exp env mem add_red show_hole_contents l) (app_exp env mem add_red show_hole_contents r) + | E_if _ | E_for _ | E_let _ -> right_atomic_exp env mem add_red show_hole_contents expr + | _ -> app_exp env mem add_red show_hole_contents expr + and right_atomic_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with (* Special case: omit "else ()" when the else branch is empty. *) | E_if(c,t,E_aux(E_block [], _)) -> - string "if" ^^ space ^^ group (exp env add_red show_hole_contents c) ^/^ - string "then" ^^ space ^^ group (exp env add_red show_hole_contents t) + string "if" ^^ space ^^ group (exp env mem add_red show_hole_contents c) ^/^ + string "then" ^^ space ^^ group (exp env mem add_red show_hole_contents t) | E_if(c,t,e) -> - string "if" ^^ space ^^ group (exp env add_red show_hole_contents c) ^/^ - string "then" ^^ space ^^ group (exp env add_red show_hole_contents t) ^/^ - string "else" ^^ space ^^ group (exp env add_red show_hole_contents e) + string "if" ^^ space ^^ group (exp env mem add_red show_hole_contents c) ^/^ + string "then" ^^ space ^^ group (exp env mem add_red show_hole_contents t) ^/^ + string "else" ^^ space ^^ group (exp env mem add_red show_hole_contents e) | E_for(id,exp1,exp2,exp3,order,exp4) -> string "foreach" ^^ space ^^ group (parens ( separate (break 1) [ doc_id id; - string "from " ^^ (atomic_exp env add_red show_hole_contents exp1); - string "to " ^^ (atomic_exp env add_red show_hole_contents exp2); - string "by " ^^ (atomic_exp env add_red show_hole_contents exp3); + string "from " ^^ (atomic_exp env mem add_red show_hole_contents exp1); + string "to " ^^ (atomic_exp env mem add_red show_hole_contents exp2); + string "by " ^^ (atomic_exp env mem add_red show_hole_contents exp3); string "in " ^^ doc_ord order ] )) ^/^ - (exp env add_red show_hole_contents exp4) - | E_let(leb,e) -> doc_op (string "in") (let_exp env add_red show_hole_contents leb) (exp env add_red show_hole_contents e) - | _ -> group (parens (exp env add_red show_hole_contents expr)) - and app_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with + (exp env mem add_red show_hole_contents exp4) + | E_let(leb,e) -> doc_op (string "in") (let_exp env mem add_red show_hole_contents leb) (exp env mem add_red show_hole_contents e) + | _ -> group (parens (exp env mem add_red show_hole_contents expr)) + and app_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with | E_app(f,args) -> - doc_unop (doc_id f) (parens (separate_map comma (exp env add_red show_hole_contents) args)) - | _ -> vaccess_exp env add_red show_hole_contents expr - and vaccess_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with + doc_unop (doc_id f) (parens (separate_map comma (exp env mem add_red show_hole_contents) args)) + | _ -> vaccess_exp env mem add_red show_hole_contents expr + and vaccess_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with | E_vector_access(v,e) -> - (atomic_exp env add_red show_hole_contents v) ^^ brackets (exp env add_red show_hole_contents e) + (atomic_exp env mem add_red show_hole_contents v) ^^ brackets (exp env mem add_red show_hole_contents e) | E_vector_subrange(v,e1,e2) -> - (atomic_exp env add_red show_hole_contents v) ^^ - brackets (doc_op dotdot (exp env add_red show_hole_contents e1) (exp env add_red show_hole_contents e2)) - | _ -> field_exp env add_red show_hole_contents expr - and field_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with - | E_field(fexp,id) -> (atomic_exp env add_red show_hole_contents fexp) ^^ dot ^^ doc_id id - | _ -> atomic_exp env add_red show_hole_contents expr - and atomic_exp env add_red (show_hole_contents:bool) ((E_aux(e,annot)) as expr) = match e with + (atomic_exp env mem add_red show_hole_contents v) ^^ + brackets (doc_op dotdot (exp env mem add_red show_hole_contents e1) (exp env mem add_red show_hole_contents e2)) + | _ -> field_exp env mem add_red show_hole_contents expr + and field_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with + | E_field(fexp,id) -> (atomic_exp env mem add_red show_hole_contents fexp) ^^ dot ^^ doc_id id + | _ -> atomic_exp env mem add_red show_hole_contents expr + and atomic_exp env mem add_red (show_hole_contents:bool) ((E_aux(e,annot)) as expr) = match e with (* Special case: an empty block is equivalent to unit, but { } is a syntactic struct *) | E_block [] -> string "()" | E_block exps -> - let exps_doc = separate_map (semi ^^ hardline) (exp env add_red show_hole_contents) exps in + let exps_doc = separate_map (semi ^^ hardline) (exp env mem add_red show_hole_contents) exps in surround 2 1 lbrace exps_doc rbrace | E_nondet exps -> - let exps_doc = separate_map (semi ^^ hardline) (exp env add_red show_hole_contents) exps in + let exps_doc = separate_map (semi ^^ hardline) (exp env mem add_red show_hole_contents) exps in string "nondet" ^^ space ^^ (surround 2 1 lbrace exps_doc rbrace) | E_id id -> (match id with | Id_aux(Id("0"), _) -> (match Interp.in_lenv env id with - | Interp.V_unknown -> string (add_red "[_]") + | Interp_ast.V_unknown -> string (add_red "[_]") | v -> if show_hole_contents then string (add_red (Interp.string_of_value v)) @@ -403,22 +489,22 @@ let doc_exp, doc_let = | E_lit lit -> doc_lit lit | E_cast(typ,e) -> if !ignore_casts then - atomic_exp env add_red show_hole_contents e + atomic_exp env mem add_red show_hole_contents e else - prefix 2 1 (parens (doc_typ typ)) (group (atomic_exp env add_red show_hole_contents e)) + prefix 2 1 (parens (doc_typ typ)) (group (atomic_exp env mem add_red show_hole_contents e)) | E_internal_cast(_,e) -> (* XXX ignore internal casts in the interpreter *) - atomic_exp env add_red show_hole_contents e + atomic_exp env mem add_red show_hole_contents e | E_tuple exps -> - parens (separate_map comma (exp env add_red show_hole_contents) exps) + parens (separate_map comma (exp env mem add_red show_hole_contents) exps) | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> - braces (separate_map semi_sp (doc_fexp env add_red show_hole_contents) fexps) + braces (separate_map semi_sp (doc_fexp env mem add_red show_hole_contents) fexps) | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) -> braces (doc_op (string "with") - (exp env add_red show_hole_contents e) - (separate_map semi_sp (doc_fexp env add_red show_hole_contents) fexps)) + (exp env mem add_red show_hole_contents e) + (separate_map semi_sp (doc_fexp env mem add_red show_hole_contents) fexps)) | E_vector exps -> - let default_print _ = brackets (separate_map comma (exp env add_red show_hole_contents) exps) in + let default_print _ = brackets (separate_map comma (exp env mem add_red show_hole_contents) exps) in (match exps with | [] -> default_print () | es -> @@ -441,28 +527,28 @@ let doc_exp, doc_let = let default_string = (match default with | Def_val_empty -> string "" - | Def_val_dec e -> concat [semi; space; string "default"; equals; (exp env add_red show_hole_contents e)]) in - let iexp (i,e) = doc_op equals (doc_int i) (exp env add_red show_hole_contents e) in + | Def_val_dec e -> concat [semi; space; string "default"; equals; (exp env mem add_red show_hole_contents e)]) in + let iexp (i,e) = doc_op equals (doc_int i) (exp env mem add_red show_hole_contents e) in brackets (concat [(separate_map comma iexp iexps);default_string]) | E_vector_update(v,e1,e2) -> brackets (doc_op (string "with") - (exp env add_red show_hole_contents v) - (doc_op equals (atomic_exp env add_red show_hole_contents e1) - (exp env add_red show_hole_contents e2))) + (exp env mem add_red show_hole_contents v) + (doc_op equals (atomic_exp env mem add_red show_hole_contents e1) + (exp env mem add_red show_hole_contents e2))) | E_vector_update_subrange(v,e1,e2,e3) -> brackets ( - doc_op (string "with") (exp env add_red show_hole_contents v) - (doc_op equals ((atomic_exp env add_red show_hole_contents e1) ^^ colon - ^^ (atomic_exp env add_red show_hole_contents e2)) (exp env add_red show_hole_contents e3))) + doc_op (string "with") (exp env mem add_red show_hole_contents v) + (doc_op equals ((atomic_exp env mem add_red show_hole_contents e1) ^^ colon + ^^ (atomic_exp env mem add_red show_hole_contents e2)) (exp env mem add_red show_hole_contents e3))) | E_list exps -> - squarebarbars (separate_map comma (exp env add_red show_hole_contents) exps) + squarebarbars (separate_map comma (exp env mem add_red show_hole_contents) exps) | E_case(e,pexps) -> - let opening = separate space [string "switch"; exp env add_red show_hole_contents e; lbrace] in - let cases = separate_map (break 1) (doc_case env add_red show_hole_contents) pexps in + let opening = separate space [string "switch"; exp env mem add_red show_hole_contents e; lbrace] in + let cases = separate_map (break 1) (doc_case env mem add_red show_hole_contents) pexps in surround 2 1 opening cases rbrace - | E_exit e -> separate space [string "exit"; exp env add_red show_hole_contents e;] - | E_return e -> separate space [string "return"; exp env add_red show_hole_contents e;] - | E_assert(e,msg) -> string "assert" ^^ parens (separate_map comma (exp env add_red show_hole_contents) [e; msg]) + | E_exit e -> separate space [string "exit"; exp env mem add_red show_hole_contents e;] + | E_return e -> separate space [string "return"; exp env mem add_red show_hole_contents e;] + | E_assert(e,msg) -> string "assert" ^^ parens (separate_map comma (exp env mem add_red show_hole_contents) [e; msg]) (* adding parens and loop for lower precedence *) | E_app (_, _)|E_vector_access (_, _)|E_vector_subrange (_, _, _) | E_cons (_, _)|E_field (_, _)|E_assign (_, _) @@ -484,57 +570,59 @@ let doc_exp, doc_let = | "*_s" | "*_si" | "*_u" | "*_ui" | "**"), _)) , _) -> - group (parens (exp env add_red show_hole_contents expr)) + group (parens (exp env mem add_red show_hole_contents expr)) (* XXX fixup deinfix into infix ones *) | E_app_infix(l, (Id_aux((DeIid op), annot')), r) -> group (parens - (exp env add_red show_hole_contents (E_aux ((E_app_infix (l, (Id_aux(Id op, annot')), r)), annot)))) + (exp env mem add_red show_hole_contents (E_aux ((E_app_infix (l, (Id_aux(Id op, annot')), r)), annot)))) (* XXX default precedence for app_infix? *) | E_app_infix(l,op,r) -> failwith ("unexpected app_infix operator " ^ (pp_format_id op)) (* doc_op (doc_id op) (exp l) (exp r) *) (* XXX missing case *) - | E_comment _ | E_comment_struc _ -> string "" + | E_comment _ | E_comment_struc _ -> string "" + | E_internal_value v -> + string (val_to_string_internal mem v) | _-> failwith "internal expression escaped" - and let_exp env add_red show_hole_contents (LB_aux(lb,_)) = match lb with + and let_exp env mem add_red show_hole_contents (LB_aux(lb,_)) = match lb with | LB_val_explicit(ts,pat,e) -> prefix 2 1 (separate space [string "let"; doc_typscm_atomic ts; doc_atomic_pat pat; equals]) - (exp env add_red show_hole_contents e) + (exp env mem add_red show_hole_contents e) | LB_val_implicit(pat,e) -> prefix 2 1 (separate space [string "let"; doc_atomic_pat pat; equals]) - (exp env add_red show_hole_contents e) + (exp env mem add_red show_hole_contents e) - and doc_fexp env add_red show_hole_contents (FE_aux(FE_Fexp(id,e),_)) = - doc_op equals (doc_id id) (exp env add_red show_hole_contents e) + and doc_fexp env mem add_red show_hole_contents (FE_aux(FE_Fexp(id,e),_)) = + doc_op equals (doc_id id) (exp env mem add_red show_hole_contents e) - and doc_case env add_red show_hole_contents (Pat_aux(Pat_exp(pat,e),_)) = - doc_op arrow (separate space [string "case"; doc_atomic_pat pat]) (group (exp env add_red show_hole_contents e)) + and doc_case env mem add_red show_hole_contents (Pat_aux(Pat_exp(pat,e),_)) = + doc_op arrow (separate space [string "case"; doc_atomic_pat pat]) (group (exp env mem add_red show_hole_contents e)) (* lexps are parsed as eq_exp - we need to duplicate the precedence * structure for them *) - and doc_lexp env add_red show_hole_contents le = app_lexp env add_red show_hole_contents le - and app_lexp env add_red show_hole_contents ((LEXP_aux(lexp,_)) as le) = match lexp with - | LEXP_memory(id,args) -> doc_id id ^^ parens (separate_map comma (exp env add_red show_hole_contents) args) - | _ -> vaccess_lexp env add_red show_hole_contents le - and vaccess_lexp env add_red show_hole_contents ((LEXP_aux(lexp,_)) as le) = match lexp with + and doc_lexp env mem add_red show_hole_contents le = app_lexp env mem add_red show_hole_contents le + and app_lexp env mem add_red show_hole_contents ((LEXP_aux(lexp,_)) as le) = match lexp with + | LEXP_memory(id,args) -> doc_id id ^^ parens (separate_map comma (exp env mem add_red show_hole_contents) args) + | _ -> vaccess_lexp env mem add_red show_hole_contents le + and vaccess_lexp env mem add_red show_hole_contents ((LEXP_aux(lexp,_)) as le) = match lexp with | LEXP_vector(v,e) -> - (atomic_lexp env add_red show_hole_contents v) ^^ brackets (exp env add_red show_hole_contents e) + (atomic_lexp env mem add_red show_hole_contents v) ^^ brackets (exp env mem add_red show_hole_contents e) | LEXP_vector_range(v,e1,e2) -> - (atomic_lexp env add_red show_hole_contents v) ^^ - brackets ((exp env add_red show_hole_contents e1) ^^ dotdot ^^ (exp env add_red show_hole_contents e2)) - | _ -> field_lexp env add_red show_hole_contents le - and field_lexp env add_red show_hole_contents ((LEXP_aux(lexp,_)) as le) = match lexp with - | LEXP_field(v,id) -> (atomic_lexp env add_red show_hole_contents v) ^^ dot ^^ doc_id id - | _ -> atomic_lexp env add_red show_hole_contents le - and atomic_lexp env add_red show_hole_contents ((LEXP_aux(lexp,_)) as le) = match lexp with + (atomic_lexp env mem add_red show_hole_contents v) ^^ + brackets ((exp env mem add_red show_hole_contents e1) ^^ dotdot ^^ (exp env mem add_red show_hole_contents e2)) + | _ -> field_lexp env mem add_red show_hole_contents le + and field_lexp env mem add_red show_hole_contents ((LEXP_aux(lexp,_)) as le) = match lexp with + | LEXP_field(v,id) -> (atomic_lexp env mem add_red show_hole_contents v) ^^ dot ^^ doc_id id + | _ -> atomic_lexp env mem add_red show_hole_contents le + and atomic_lexp env mem add_red show_hole_contents ((LEXP_aux(lexp,_)) as le) = match lexp with | LEXP_id id -> doc_id id | LEXP_cast(typ,id) -> prefix 2 1 (parens (doc_typ typ)) (doc_id id) - | LEXP_tup(lexps) -> group (parens (separate_map comma (doc_lexp env add_red show_hole_contents) lexps)) + | LEXP_tup(lexps) -> group (parens (separate_map comma (doc_lexp env mem add_red show_hole_contents) lexps)) | LEXP_memory _ | LEXP_vector _ | LEXP_vector_range _ - | LEXP_field _ -> group (parens (doc_lexp env add_red show_hole_contents le)) + | LEXP_field _ -> group (parens (doc_lexp env mem add_red show_hole_contents le)) (* expose doc_exp and doc_let *) in exp, let_exp @@ -611,15 +699,15 @@ let doc_effects_opt (Effect_opt_aux(e,_)) = match e with | Effect_opt_pure -> string "pure" | Effect_opt_effect e -> doc_effects e -let doc_funcl env add_red (FCL_aux(FCL_Funcl(id,pat,exp),_)) = - group (doc_op equals (separate space [doc_id id; doc_atomic_pat pat]) (doc_exp env add_red false exp)) +let doc_funcl env mem add_red (FCL_aux(FCL_Funcl(id,pat,exp),_)) = + group (doc_op equals (separate space [doc_id id; doc_atomic_pat pat]) (doc_exp env mem add_red false exp)) -let doc_fundef env add_red (FD_aux(FD_function(r, typa, efa, fcls),_)) = +let doc_fundef env mem add_red (FD_aux(FD_function(r, typa, efa, fcls),_)) = match fcls with | [] -> failwith "FD_function with empty function list" | _ -> let sep = hardline ^^ string "and" ^^ space in - let clauses = separate_map sep (doc_funcl env add_red) fcls in + let clauses = separate_map sep (doc_funcl env mem add_red) fcls in separate space [string "function"; doc_rec r ^^ doc_tannot_opt typa; string "effect"; doc_effects_opt efa; @@ -629,7 +717,7 @@ let doc_dec (DEC_aux(d,_)) = match d with | DEC_reg(typ,id) -> separate space [string "register"; doc_atomic_typ typ; doc_id id] | _ -> failwith "interpreter printing out declarations unexpectedly" -let doc_scattered env add_red (SD_aux (sdef, _)) = match sdef with +let doc_scattered env mem add_red (SD_aux (sdef, _)) = match sdef with | SD_scattered_function (r, typa, efa, id) -> separate space [ string "scattered function"; @@ -641,35 +729,35 @@ let doc_scattered env add_red (SD_aux (sdef, _)) = match sdef with (string "scattered typedef" ^^ space ^^ doc_id id ^^ doc_namescm ns) (doc_typquant tq empty) | SD_scattered_funcl funcl -> - string "function clause" ^^ space ^^ doc_funcl env add_red funcl + string "function clause" ^^ space ^^ doc_funcl env mem add_red funcl | SD_scattered_unioncl (id, tu) -> separate space [string "union"; doc_id id; string "member"; doc_type_union tu] | SD_scattered_end id -> string "end" ^^ space ^^ doc_id id -let rec doc_def env add_red def = group (match def with +let rec doc_def env mem add_red def = group (match def with | DEF_default df -> doc_default df | DEF_spec v_spec -> doc_spec v_spec | DEF_type t_def -> doc_typdef t_def | DEF_kind k_def -> failwith "interpreter unexpectedly printing kind def" - | DEF_fundef f_def -> doc_fundef env add_red f_def - | DEF_val lbind -> doc_let env add_red false lbind + | DEF_fundef f_def -> doc_fundef env mem add_red f_def + | DEF_val lbind -> doc_let env mem add_red false lbind | DEF_reg_dec dec -> doc_dec dec - | DEF_scattered sdef -> doc_scattered env add_red sdef - | DEF_comm comm_dec -> string "(*" ^^ doc_comm_dec env add_red comm_dec ^^ string "*)" + | DEF_scattered sdef -> doc_scattered env mem add_red sdef + | DEF_comm comm_dec -> string "(*" ^^ doc_comm_dec env mem add_red comm_dec ^^ string "*)" ) ^^ hardline -and doc_comm_dec env add_red dec = match dec with +and doc_comm_dec env mem add_red dec = match dec with | DC_comm s -> string s - | DC_comm_struct d -> doc_def env add_red d + | DC_comm_struct d -> doc_def env mem add_red d -let doc_defs env add_red (Defs(defs)) = - separate_map hardline (doc_def env add_red) defs +let doc_defs env mem add_red (Defs(defs)) = + separate_map hardline (doc_def env mem add_red) defs let print ?(len=80) channel doc = ToChannel.pretty 1. len channel doc let to_buf ?(len=80) buf doc = ToBuffer.pretty 1. len buf doc -let pp_exp env add_red show_hole_contents e = +let pp_exp env mem add_red show_hole_contents e = let b = Buffer.create 20 in - to_buf b (doc_exp env add_red show_hole_contents e); + to_buf b (doc_exp env mem add_red show_hole_contents e); Buffer.contents b diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml index f0c0d392..79a86113 100644 --- a/src/lem_interp/printing_functions.ml +++ b/src/lem_interp/printing_functions.ml @@ -49,60 +49,13 @@ open Interp_interface ;; open Nat_big_num ;; -let lit_to_string = function - | L_unit -> "unit" - | L_zero -> "0b0" - | L_one -> "0b1" - | L_true -> "true" - | L_false -> "false" - | L_num n -> to_string n - | L_hex s -> "0x"^s - | L_bin s -> "0b"^s - | L_undef -> "undefined" - | L_string s -> "\"" ^ s ^ "\"" -;; - -let id_to_string = function - | Id_aux(Id s,_) | Id_aux(DeIid s,_) -> s -;; - -let rec loc_to_string = function - | Unknown -> "location unknown" - | Int(s,_) -> s - | Generated l -> "Generated near " ^ loc_to_string l - | Range(s,fline,fchar,tline,tchar) -> - if fline = tline - then sprintf "%s:%d:%d" s fline fchar - else sprintf "%s:%d:%d-%d:%d" s fline fchar tline tchar -;; - -let collapse_leading s = - if String.length s <= 8 then s else - let first_bit = s.[0] in - let templ = sprintf "%c...%c" first_bit first_bit in - - let rec find_first_diff str cha pos = - if pos >= String.length str then None - else if str.[pos] != cha then Some pos - else find_first_diff str cha (pos+1) - in - - match find_first_diff s first_bit 0 with - | None -> templ - | Some pos when pos > 4 -> templ ^ (String.sub s pos ((String.length s)- pos)) - | _ -> s -;; +let val_to_string_internal = Pretty_interp.val_to_string_internal ;; +let lit_to_string = Pretty_interp.lit_to_string ;; +let id_to_string = Pretty_interp.id_to_string ;; +let loc_to_string = Pretty_interp.loc_to_string ;; +let bitvec_to_string = Pretty_interp.bitvec_to_string ;; +let collapse_leading = Pretty_interp.collapse_leading ;; -let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (function - | Interp.V_lit(L_aux(L_zero, _)) -> "0" - | Interp.V_lit(L_aux(L_one, _)) -> "1" - | Interp.V_lit(L_aux(L_undef, _)) -> "u" - | Interp.V_unknown -> "?" - | v -> (Printf.printf "bitvec found a non bit %s%!\n" (Interp.string_of_value v));assert false) - (List.map Interp.detaint l))) -;; - -(* pp the bytes of a Bytevector as a hex value *) type bits_lifted_homogenous = | Bitslh_concrete of bit list @@ -322,36 +275,6 @@ let reg_name_to_string = function let dependencies_to_string dependencies = String.concat ", " (List.map reg_name_to_string dependencies) -let rec val_to_string_internal ((Interp.LMem (_,_,memory,_)) as mem) = function - | Interp.V_boxref(n, t) -> val_to_string_internal mem (Pmap.find n memory) - | Interp.V_lit (L_aux(l,_)) -> sprintf "%s" (lit_to_string l) - | Interp.V_tuple l -> - let repr = String.concat ", " (List.map (val_to_string_internal mem) l) in - sprintf "(%s)" repr - | Interp.V_list l -> - let repr = String.concat "; " (List.map (val_to_string_internal mem) l) in - sprintf "[||%s||]" repr - | Interp.V_vector (first_index, inc, l) -> - let last_index = (if (Interp.IInc = inc) then List.length l - 1 else 1 - List.length l) + first_index in - let repr = - try bitvec_to_string l - with Failure _ -> - sprintf "[%s]" (String.concat "; " (List.map (val_to_string_internal mem) l)) in - sprintf "%s [%s..%s]" repr (string_of_int first_index) (string_of_int last_index) - | (Interp.V_vector_sparse(first_index,last_index,inc,l,default) as v) -> - val_to_string_internal mem (Interp_lib.fill_in_sparse v) - | Interp.V_record(_, l) -> - let pp (id, value) = sprintf "%s = %s" (id_to_string id) (val_to_string_internal mem value) in - let repr = String.concat "; " (List.map pp l) in - sprintf "{%s}" repr - | Interp.V_ctor (id,_,_, value) -> - sprintf "%s %s" (id_to_string id) (val_to_string_internal mem value) - | Interp.V_register _ | Interp.V_register_alias _ -> - sprintf "reg-as-value" - | Interp.V_unknown -> "unknown" - | Interp.V_track(v,rs) -> (*"tainted by {" ^ (Interp_utilities.list_to_string Interp.string_of_reg_form "," rs) ^ "} --" ^ *) (val_to_string_internal mem v) -;; - let rec top_frame_exp_state = function | Interp.Top -> raise (Invalid_argument "top_frame_exp") | Interp.Hole_frame(_, e, _, env, mem, Interp.Top) @@ -485,27 +408,27 @@ let yellow = color true 3 let blue = color true 4 let grey = color false 7 -let exp_to_string env show_hole_value e = Pretty_interp.pp_exp env red show_hole_value e +let exp_to_string env mem show_hole_value e = Pretty_interp.pp_exp env mem red show_hole_value e let get_loc (E_aux(_, (l, (_ : tannot)))) = loc_to_string l -let print_exp printer env show_hole_value e = - printer ((get_loc e) ^ ": " ^ (Pretty_interp.pp_exp env red show_hole_value e) ^ "\n") +let print_exp printer env mem show_hole_value e = + printer ((get_loc e) ^ ": " ^ (Pretty_interp.pp_exp env mem red show_hole_value e) ^ "\n") let instruction_state_to_string (IState(stack, _)) = - List.fold_right (fun (e,(env,mem)) es -> (exp_to_string env true e) ^ "\n" ^ es) (compact_stack stack) "" + List.fold_right (fun (e,(env,mem)) es -> (exp_to_string env mem true e) ^ "\n" ^ es) (compact_stack stack) "" let top_instruction_state_to_string (IState(stack,_)) = - let (exp,(env,_)) = top_frame_exp_state stack in exp_to_string env true exp + let (exp,(env,mem)) = top_frame_exp_state stack in exp_to_string env mem true exp let instruction_stack_to_string (IState(stack,_)) = let rec stack_to_string = function Interp.Top -> "" | Interp.Hole_frame(_,e,_,env,mem,Interp.Top) | Interp.Thunk_frame(e,_,env,mem,Interp.Top) -> - exp_to_string env true e + exp_to_string env mem true e | Interp.Hole_frame(_,e,_,env,mem,s) | Interp.Thunk_frame(e,_,env,mem,s) -> - (exp_to_string env false e) ^ "\n----------------------------------------------------------\n" ^ + (exp_to_string env mem false e) ^ "\n----------------------------------------------------------\n" ^ (stack_to_string s) in match stack with @@ -536,7 +459,7 @@ let instr_parm_to_string (name, typ, value) = | Other -> "Unrepresentable external value" | _ -> let intern_v = (Interp_inter_imp.intern_ifield_value D_increasing value) in match Interp_lib.to_num Interp_lib.Unsigned intern_v with - | Interp.V_lit (L_aux(L_num n, _)) -> to_string n + | Interp_ast.V_lit (L_aux(L_num n, _)) -> to_string n | _ -> ifield_to_string value let rec instr_parms_to_string ps = @@ -551,12 +474,12 @@ let instruction_to_string (name, parms) = ((*pad 5*) (String.lowercase name)) ^ " " ^ instr_parms_to_string parms let print_backtrace_compact printer (IState(stack,_)) = - List.iter (fun (e,(env,mem)) -> print_exp printer env true e) (compact_stack stack) + List.iter (fun (e,(env,mem)) -> print_exp printer env mem true e) (compact_stack stack) let print_stack printer is = printer (instruction_stack_to_string is) let print_continuation printer (IState(stack,_)) = - let (e,(env,mem)) = top_frame_exp_state stack in print_exp printer env true e + let (e,(env,mem)) = top_frame_exp_state stack in print_exp printer env mem true e let print_instruction printer instr = printer (instruction_to_string instr) let pp_instruction_state state () = diff --git a/src/lem_interp/printing_functions.mli b/src/lem_interp/printing_functions.mli index f629a307..85744d61 100644 --- a/src/lem_interp/printing_functions.mli +++ b/src/lem_interp/printing_functions.mli @@ -10,7 +10,7 @@ val loc_to_string : l -> string val get_loc : tannot exp -> string (*interp_interface.value to string*) val reg_value_to_string : register_value -> string -val val_to_string_internal : Interp.lmem -> Interp.value -> string +val val_to_string_internal : Interp.lmem -> Interp_ast.value -> string (*(*Force all representations to hex strings instead of a mixture of hex and binary strings*) val val_to_hex_string : value0 -> string*) @@ -19,7 +19,7 @@ val reg_name_to_string : reg_name -> string (* format the register dependencies *) val dependencies_to_string : reg_name list -> string (* formats an expression, using interp_pretty *) -val exp_to_string : Interp.lenv -> bool -> tannot exp -> string +val exp_to_string : Interp.lenv -> Interp.lmem -> bool -> tannot exp -> string (* Functions to set the color of parts of the output *) type ppmode = @@ -55,7 +55,7 @@ val local_variables_to_string : instruction_state -> string val instruction_to_string : instruction -> string (*Functions to take a print function and cause a print event for the above functions *) -val print_exp : (string-> unit) -> Interp.lenv -> bool -> tannot exp -> unit +val print_exp : (string-> unit) -> Interp.lenv -> Interp.lmem -> bool -> tannot exp -> unit val print_backtrace_compact : (string -> unit) -> instruction_state -> unit val print_continuation : (string -> unit) -> instruction_state -> unit val print_instruction : (string -> unit) -> instruction -> unit diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml index d6f6e30c..602efad3 100644 --- a/src/lem_interp/run_interp_model.ml +++ b/src/lem_interp/run_interp_model.ml @@ -339,7 +339,7 @@ let run let (top_exp,(top_env,top_mem)) = top_frame_exp_state stack in let loc = get_loc (compact_exp top_exp) in if mode = Step || force then begin - interactf "%s\n" (Pretty_interp.pp_exp top_env Printing_functions.red true top_exp); + interactf "%s\n" (Pretty_interp.pp_exp top_env top_mem Printing_functions.red true top_exp); interact mode env' state end else mode in @@ -470,7 +470,7 @@ let run let (IState(instr_state,context)) = istate in let (top_exp,(top_env,top_mem)) = top_frame_exp_state instr_state in interactf "%s: %s %s\n" (grey name) (blue "evaluate") - (Pretty_interp.pp_exp top_env Printing_functions.red true top_exp); + (Pretty_interp.pp_exp top_env top_mem Printing_functions.red true top_exp); try Printexc.record_backtrace true; loop mode (reg, mem,tagmem) (Interp_inter_imp.interp0 imode istate) -- cgit v1.2.3