summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/lem_interp/interp.lem99
-rw-r--r--src/lem_interp/interp_inter_imp.lem2
-rw-r--r--src/pretty_print.ml9
3 files changed, 65 insertions, 45 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 8cdd13ce..19609c6d 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -1016,9 +1016,9 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
match exp with
| E_lit lit ->
if is_lit_vector lit
- then
- let is_inc = (match typ with | T_app "vector" (T_args [_;_;T_arg_order (Ord_aux Ord_inc _);_]) -> true | _ -> false end) in
- (Value (litV_to_vec lit is_inc),l_mem,l_env)
+ then let is_inc = (match typ with
+ | T_app "vector" (T_args [_;_;T_arg_order (Ord_aux Ord_inc _);_]) -> true | _ -> false end) in
+ (Value (litV_to_vec lit is_inc),l_mem,l_env)
else (Value (V_lit lit), l_mem,l_env)
| E_cast ((Typ_aux typ _) as ctyp) exp ->
(*Cast is either a no-op, a signal to read a register, or a signal to change the start of a vector *)
@@ -1026,12 +1026,15 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
(interp_main mode t_level l_env l_mem exp)
(fun v lm le ->
(* Potentially use cast to change vector start position *)
- let update_vector_start start update_v =
+ let conditional_update_vstart () =
match typ with
| Typ_app (Id_aux (Id "vector") _) [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_constant i) _)) _;_;_;_] ->
- if start = i
- then (Value v,lm,le)
- else (Value (update_v i),lm,le)
+ match v with
+ | V_vector start inc vs ->
+ if start = i then (Value v,lm,le) else (Value (update_vector_start i v),lm,le)
+ | V_track (V_vector start inc vs) r ->
+ if start = i then (Value v,lm,le) else (Value (update_vector_start i v),lm,le)
+ | _ -> (Value v,lm,le) end
| _ -> (Value v,lm,le) end in
(match (tag,v) with
(*Cast is telling us to read a register*)
@@ -1040,15 +1043,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
(Hole_frame (id_of_string "0")
(E_aux (E_id (id_of_string "0")) (Unknown, (val_annot (reg_to_t regform)))) t_level le lm Top), lm,le)
(*Cast is changing vector start position, potentially*)
- | (_,V_vector start inc items) -> update_vector_start start (fun i -> (V_vector i inc items))
- | (_,V_track (V_vector start inc items) regs) ->
- update_vector_start start (fun i -> (taint (V_vector i inc items) regs))
- (*TODO trim items below if i > (or < for dec) start *)
- | (_,V_vector_sparse start inc len items def) ->
- update_vector_start start (fun i -> (V_vector_sparse i inc len items def))
- | (_,V_track (V_vector_sparse start inc len items def) regs) ->
- update_vector_start start (fun i -> (taint (V_vector_sparse i inc len items def) regs))
- | _ -> (Value v,lm,le) end))
+ | (_,v) -> conditional_update_vstart () end))
(fun a -> update_stack a (add_to_top_frame (fun e env -> (E_aux (E_cast ctyp e) (l,annot), env))))
| E_id id ->
let name = get_id id in
@@ -1063,17 +1058,17 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| Nothing ->
(match in_env regs id with
| Just(value) -> (Value value, l_mem,l_env)
- | Nothing -> (Error l (String.stringAppend "Internal error: unbound id on Tag_global " name),l_mem,l_env) end) end
+ | Nothing -> (Error l ("Internal error: " ^ name ^ " unbound on Tag_global"),l_mem,l_env) end) end
| Tag_enum ->
match in_env lets id with
| Just(value) -> (Value value,l_mem,l_env)
- | Nothing -> (Error l (String.stringAppend "Internal error: unbound id on Tag_enum " name), l_mem,l_env)
+ | Nothing -> (Error l ("Internal error: " ^ name ^ " unbound on Tag_enum "), l_mem,l_env)
end
| Tag_extern _ -> (* update with id here when it's never just "register" *)
- let regf = match in_lenv l_env id with
+ let regf = match in_lenv l_env id with (* Check for local treatment of a register as a value *)
| V_register regform -> regform
| _ ->
- match in_env regs id with
+ match in_env regs id with (* Register isn't a local value, so pull from global environment *)
| Just(V_register regform) -> regform
| _ -> Reg id annot end end in
(Action (Read_reg regf Nothing)
@@ -1084,13 +1079,14 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
match in_env aliases id with
| Just aspec -> interp_alias_read mode t_level l_env l_mem aspec
| _ -> (Error l ("Internal error: alias not found"), l_mem,l_env) end
- | _ -> (Error l (String.stringAppend "Internal error: tag other than empty,enum,or extern " name),l_mem,l_env)
+ | _ -> (Error l ("Internal error: tag other than empty,enum,or extern for " ^ name),l_mem,l_env)
end
| E_if cond thn els ->
resolve_outcome
(interp_main mode t_level l_env l_mem cond)
(fun value lm le ->
match (value,mode.eager_eval) with
+ (*TODO remove booleans here when fully removed elsewhere *)
| (V_lit(L_aux L_true _),true) -> interp_main mode t_level l_env lm thn
| (V_track (V_lit (L_aux L_true _)) _, true) -> interp_main mode t_level l_env lm thn
| (V_lit(L_aux L_one _),true) -> interp_main mode t_level l_env lm thn
@@ -1137,13 +1133,15 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| (V_lit _, V_lit _) -> ((E_aux (E_lit diff) augment_annot), env)
| (V_track _ rs, V_lit _) -> to_exp mode env (V_track (V_lit diff) rs)
| (V_lit _, V_track _ rs) -> to_exp mode env (V_track (V_lit diff) rs)
- | (V_track _ r1, V_track _ r2) -> (to_exp mode env (V_track (V_lit diff) (r1 ++ r2))) end in
+ | (V_track _ r1, V_track _ r2) ->
+ (to_exp mode env (V_track (V_lit diff) (r1 ++ r2))) end in
let e =
(E_aux (E_block
- [(E_aux (E_let
- (LB_aux (LB_val_implicit (P_aux (P_id id) (fl,val_annot ftyp)) from_e)
- (Unknown,val_annot ftyp))
- exp) (l,annot));
+ [(E_aux
+ (E_let
+ (LB_aux (LB_val_implicit (P_aux (P_id id) (fl,val_annot ftyp)) from_e)
+ (Unknown,val_annot ftyp))
+ exp) (l,annot));
(E_aux (E_for id augment_e to_e by_e order exp) (l,annot))])
(l,annot)) in
if mode.eager_eval
@@ -1152,8 +1150,9 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| V_unknown ->
let e =
(E_aux (E_let
- (LB_aux (LB_val_implicit (P_aux (P_id id) (fl, val_annot (val_typ from_val))) from_e)
- (fl, val_annot (val_typ from_val)))
+ (LB_aux
+ (LB_val_implicit (P_aux (P_id id) (fl, val_annot (val_typ from_val))) from_e)
+ (fl, val_annot (val_typ from_val)))
exp) (l,annot)) in
interp_main mode t_level env lm e
| _ -> (Error l "internal error: by must be a number",lm,le) end)
@@ -1217,7 +1216,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
(l,annot)))
(fun vs -> (V_record t (List.zip fields vs))) l_env l_mem [] exps)
(fun vs lm le -> (Value (fupdate_record rv vs), lm, le))
- (fun a -> a) (*Due to exp_list this should never happen, but needed to perform the functional update on Value *)
+ (fun a -> a) (*Due to exp_list this won't happen, but we want to functionaly update on Value *)
| V_unknown -> (Value V_unknown, lm, le)
| _ -> (Error l "internal error: record update requires record",lm,le) end)
(fun a -> update_stack a
@@ -1236,7 +1235,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| V_unknown -> (Value V_unknown,lm,le)
| V_track (V_list t) r -> (Value (V_track (V_list (hdv::t)) r),lm,le)
| V_track V_unknown r -> (Value (V_track V_unknown r),lm,le)
- | _ -> (Error l ":: of non-list value",lm,le) end)
+ | _ -> (Error l "Internal error '::' of non-list value",lm,le) end)
(fun a -> update_stack a
(add_to_top_frame
(fun t env -> let (hde,env') = to_exp mode env hdv in (E_aux (E_cons hde t) (l,annot),env')))))
@@ -1279,7 +1278,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| _ -> Error l "Internal error, unrecognized read, no id"
end
| Nothing -> Error l "Internal error, unrecognized read, no reg" end
- | _ -> update_stack a (add_to_top_frame (fun e env -> (E_aux(E_field e id) (l,annot),env))) end)
+ | _ -> update_stack a (add_to_top_frame (fun e env -> (E_aux(E_field e id) (l,annot),env))) end)
| E_vector_access vec i ->
resolve_outcome
(interp_main mode t_level l_env l_mem i)
@@ -1305,16 +1304,24 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| V_unknown -> (Value V_unknown,lm,le)
| V_track V_unknown r -> (Value (V_track V_unknown r),lm,le)
| _ -> (Error l "Vector access reading of non-vector",lm,le)end)
- (fun a ->
- match a with
+ (fun a ->
+ match a with
| Action (Read_reg reg Nothing) stack ->
- if (top_hole stack)
- then Action (Read_reg reg (Just(n,n))) stack
- else Action (Read_reg reg Nothing)
- (add_to_top_frame
- (fun v env ->
- let (iv_e, env) = to_exp mode env iv_whole in
- (E_aux (E_vector_access v iv_e) (l,annot),env)) stack)
+ match vec with
+ | (E_aux _ (l,Just(_,Tag_extern _,_,_))) -> Action (Read_reg reg (Just(n,n))) stack
+ | _ -> Action (Read_reg reg Nothing)
+ (add_to_top_frame
+ (fun v env ->
+ let (iv_e, env) = to_exp mode env iv_whole in
+ (E_aux (E_vector_access v iv_e) (l,annot),env)) stack) end
+ | Action (Read_reg reg (Just (o,p))) stack ->
+ match vec with
+ | (E_aux _ (l,Just(_,Tag_extern _,_,_))) -> Action (Read_reg reg (Just(n,n))) stack
+ | _ -> Action (Read_reg reg (Just (o,p)))
+ (add_to_top_frame
+ (fun v env ->
+ let (iv_e, env) = to_exp mode env iv_whole in
+ (E_aux (E_vector_access v iv_e) (l,annot),env)) stack) end
| _ ->
update_stack a
(add_to_top_frame
@@ -1367,9 +1374,15 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
(E_aux (E_vector_subrange v ie1 ie2) (l,annot), env) in
match a with
| Action (Read_reg reg Nothing) stack ->
- if (top_hole stack)
- then Action (Read_reg reg (Just((get_num iv1),(get_num iv2)))) stack
- else Action (Read_reg reg Nothing) (add_to_top_frame rebuild stack)
+ match vec with
+ | (E_aux _ (l,Just(_,Tag_extern _,_,_))) ->
+ Action (Read_reg reg (Just((get_num iv1),(get_num iv2)))) stack
+ | _ -> Action (Read_reg reg Nothing) (add_to_top_frame rebuild stack) end
+ | Action (Read_reg reg (Just (o,p))) stack ->
+ match vec with
+ | (E_aux _ (l,Just(_,Tag_extern _,_,_))) ->
+ Action (Read_reg reg (Just((get_num iv1),(get_num iv2)))) stack
+ | _ -> Action (Read_reg reg (Just (o,p))) (add_to_top_frame rebuild stack) end
| _ -> update_stack a (add_to_top_frame rebuild) end)
end)
(fun a -> update_stack a
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 06782451..7c338600 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -29,6 +29,8 @@ let rec to_bytes l = match l with
end
let intern_value v = match v with
+ | Bitvector [true] _ _ -> Interp.V_lit (L_aux L_one Interp_ast.Unknown)
+ | Bitvector [false] _ _ -> Interp.V_lit (L_aux L_zero Interp_ast.Unknown)
| Bitvector bs inc fst -> Interp.V_vector fst inc (to_bits bs)
| Bytevector bys -> Interp.V_vector 0 true
(List.concat (List.map (fun by ->
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index faa75224..d0b02650 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -366,12 +366,17 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) =
| E_cast(typ,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_cast" pp_lem_typ typ pp_lem_exp exp pp_lem_l l pp_annot annot
| E_internal_cast((_,NoTyp),e) -> pp_lem_exp ppf e
| E_internal_cast((_,Base((_,t),_,_,_)), (E_aux(ec,(_,eannot)) as exp)) ->
+ let print_cast () = fprintf ppf "@[<0>(E_aux (E_cast %a %a) (%a, %a))@]"
+ pp_lem_typ (t_to_typ t) pp_lem_exp exp pp_lem_l l pp_annot annot in
(match t.t,eannot with
| Tapp("vector",[TA_nexp n1;_;_;_]),Base((_,{t=Tapp("vector",[TA_nexp n2;_;_;_])}),_,_,_) ->
if nexp_eq n1 n2
then pp_lem_exp ppf exp
- else fprintf ppf "@[<0>(E_aux (E_cast %a %a) (%a, %a))@]" pp_lem_typ (t_to_typ t) pp_lem_exp exp pp_lem_l l pp_annot annot
- | _ -> fprintf ppf "@[<0>(E_aux (E_cast %a %a) (%a, %a))@]" pp_lem_typ (t_to_typ t) pp_lem_exp exp pp_lem_l l pp_annot annot)
+ else (match (n1.nexp,n2.nexp) with
+ | Nconst i1,Nconst i2 -> if i1=i2 then pp_lem_exp ppf exp else print_cast ()
+ | Nconst i1,_ -> print_cast ()
+ | _ -> pp_lem_exp ppf exp)
+ | _ -> pp_lem_exp ppf exp)
| E_app(f,args) -> fprintf ppf "@[<0>(E_aux (%a %a [%a]) (%a, %a))@]" kwd "E_app" pp_lem_id f (list_pp pp_semi_lem_exp pp_lem_exp) args pp_lem_l l pp_annot annot
| E_app_infix(l',op,r) -> fprintf ppf "@[<0>(E_aux (%a %a %a %a) (%a, %a))@]" kwd "E_app_infix" pp_lem_exp l' pp_lem_id op pp_lem_exp r pp_lem_l l pp_annot annot
| E_tuple(exps) -> fprintf ppf "@[<0>(E_aux %a [%a] %a (%a, %a))@]" kwd "(E_tuple" (list_pp pp_semi_lem_exp pp_lem_exp) exps kwd ")" pp_lem_l l pp_annot annot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 07:31:01 +0000