From 32c15509e02ba00f406fa341f65457e62c0b9e53 Mon Sep 17 00:00:00 2001 From: Kathy Gray Date: Wed, 17 Aug 2016 19:07:48 +0100 Subject: tuple assignment now implemented so (a,b) := foo() will now work --- language/l2_typ.ott | 1 + src/lem_interp/interp.lem | 306 +++++++++++++++++++++++++--------------------- 2 files changed, 167 insertions(+), 140 deletions(-) diff --git a/language/l2_typ.ott b/language/l2_typ.ott index f768c65b..c4c6d0b2 100644 --- a/language/l2_typ.ott +++ b/language/l2_typ.ott @@ -72,6 +72,7 @@ tag :: 'Tag_' ::= | None :: :: empty | Intro :: :: intro {{ com Denotes an assignment and lexp that introduces a binding }} | Set :: :: set {{ com Denotes an expression that mutates a local variable }} + | Tuple :: :: tuple_assign {{ com Denotes an assignment with a tuple lexp }} | Global :: :: global {{ com Globally let-bound or enumeration based value/variable }} | Ctor :: :: ctor {{ com Data constructor from a type union }} | Extern optx :: :: extern {{ com External function, specied only with a val statement }} diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 09fb745b..addc37ba 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -2250,8 +2250,8 @@ 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 -> (match create_write_message_or_update mode t_level v l_env lm true lexp with - | (outcome,Nothing) -> outcome - | (outcome,Just lexp_builder) -> + | (outcome,Nothing,_) -> outcome + | (outcome,Just lexp_builder,Nothing) -> resolve_outcome outcome (fun v lm le -> (Value v,lm,le)) (fun a -> @@ -2264,6 +2264,14 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = let (ev,env') = (to_exp mode env v) in let (lexp,env') = (lexp_builder e env') in (E_aux (E_assign lexp ev) (l,annot),env'))) end)) + | (outcome,Just lexp_builder, Just v) -> + resolve_outcome outcome + (fun v lm le -> (Value v,lm,le)) + (fun a -> update_stack a (add_to_top_frame + (fun e env -> + let (ev,env') = to_exp mode env v in + let (lexp,env') = (lexp_builder e env') in + (E_aux (E_assign lexp ev) (l,annot),env')))) end)) (fun a -> update_stack a (add_to_top_frame (fun v env -> (E_aux (E_assign lexp v) (l,annot), env)))) | _ -> (Error l "Internal expression escaped to interpreter", l_mem, l_env) @@ -2289,7 +2297,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = and create_write_message_or_update mode t_level value l_env l_mem is_top_level ((LEXP_aux lexp (l,annot)):lexp tannot) - : ((outcome * lmem * lenv) * maybe ((exp tannot) -> lenv -> ((lexp tannot) * lenv))) = + : ((outcome * lmem * lenv) * maybe ((exp tannot) -> lenv -> ((lexp tannot) * lenv)) * maybe value) = let (Env fdefs instrs default_dir lets regs ctors subregs aliases) = t_level in let (typ,tag,ncs,ef,efr) = match annot with | Nothing -> (T_var "fresh_v", Tag_empty, [], @@ -2311,85 +2319,85 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level | V_unknown -> if is_top_level then if name = "0" then - ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing) + ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing, Nothing) else let (LMem owner c m s) = l_mem in let l_mem = (LMem owner (c+1) m s) in ((Value (V_lit (L_aux L_unit l)), update_mem mode.track_lmem l_mem c value, - (add_to_env (id,(V_boxref c typ)) l_env)),Nothing) - else ((Error l ("Unknown local id " ^ (get_id id)),l_mem,l_env),Nothing) + (add_to_env (id,(V_boxref c typ)) l_env)),Nothing, Nothing) + else ((Error l ("Unknown local id " ^ (get_id id)),l_mem,l_env),Nothing,Nothing) | v -> if is_top_level then if name = "0" then - ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing) + ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing,Nothing) else ((Error l ("Writes must be to reg values given " ^ (string_of_value v)),l_mem,l_env), - Nothing) - else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_id id) (l,annot), env))) + Nothing, Nothing) + else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_id id) (l,annot), env)), Nothing) end | Tag_set -> match detaint (in_lenv l_env id) with | ((V_boxref n t) as v) -> if is_top_level then ((Value (V_lit (L_aux L_unit l)), - update_mem mode.track_lmem l_mem n (recenter_val t value), l_env),Nothing) - else ((Value v, l_mem, l_env),Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env))) + update_mem mode.track_lmem l_mem n (recenter_val t value), l_env),Nothing, Nothing) + else ((Value v, l_mem, l_env),Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env)), Nothing) | V_unknown -> if is_top_level then if name = "0" then - ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing) + ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing, Nothing) else let (LMem owner c m s) = l_mem in let l_mem = (LMem owner (c+1) m s) in ((Value (V_lit (L_aux L_unit l)), update_mem mode.track_lmem l_mem c value, - (add_to_env (id,(V_boxref c typ)) l_env)),Nothing) - else ((Error l ("Unknown local id " ^ (get_id id)),l_mem,l_env),Nothing) + (add_to_env (id,(V_boxref c typ)) l_env)),Nothing,Nothing) + else ((Error l ("Unknown local id " ^ (get_id id)),l_mem,l_env),Nothing, Nothing) | v -> if is_top_level then if name = "0" then - ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing) + ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing, Nothing) else ((Error l ("Writes must be to reg values given " ^ (string_of_value v)),l_mem,l_env), - Nothing) - else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_id id) (l,annot), env))) + Nothing, Nothing) + else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_id id) (l,annot), env)), Nothing) end | Tag_empty -> match detaint (in_lenv l_env id) with | ((V_boxref n t) as v) -> if is_top_level then ((Value (V_lit (L_aux L_unit l)), - update_mem mode.track_lmem l_mem n (recenter_val t value), l_env),Nothing) - else ((Value v, l_mem, l_env),Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env))) + update_mem mode.track_lmem l_mem n (recenter_val t value), l_env),Nothing, Nothing) + else ((Value v, l_mem, l_env),Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env)), Nothing) | V_unknown -> if is_top_level then if name = "0" then - ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing) + ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing, Nothing) else let (LMem owner c m s) = l_mem in let l_mem = (LMem owner (c+1) m s) in ((Value (V_lit (L_aux L_unit l)), update_mem mode.track_lmem l_mem c value, - (add_to_env (id,(V_boxref c typ)) l_env)),Nothing) - else ((Error l ("Unknown local id " ^ (get_id id)),l_mem,l_env),Nothing) + (add_to_env (id,(V_boxref c typ)) l_env)),Nothing, Nothing) + else ((Error l ("Unknown local id " ^ (get_id id)),l_mem,l_env),Nothing,Nothing) | v -> if is_top_level then if name = "0" then - ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing) + ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing, Nothing) else ((Error l ("Writes must be to reg values given " ^ (string_of_value v)),l_mem,l_env), - Nothing) - else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_id id) (l,annot), env))) + Nothing, Nothing) + else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_id id) (l,annot), env)), Nothing) end | Tag_global -> (match in_env lets name with | Just v -> - if is_top_level then ((Error l "Writes must be to reg or registers",l_mem,l_env),Nothing) - else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_id id) (l,annot), env))) + if is_top_level then ((Error l "Writes must be to reg or registers",l_mem,l_env),Nothing,Nothing) + else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_id id) (l,annot), env)), Nothing) | Nothing -> let regf = match in_env regs name with (*pull the regform with the most specific type annotation from env *) @@ -2402,8 +2410,8 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (if is_top_level then (update_vector_start default_dir start_pos reg_size value) else 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) in - if is_top_level then (request,Nothing) - else (request,Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env))) end) + if is_top_level then (request,Nothing,Nothing) + else (request,Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env)), Nothing) end) | Tag_extern _ -> let regf = match in_env regs name with (*pull the regform with the most specific type annotation from env *) @@ -2416,8 +2424,8 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (if is_top_level then (update_vector_start default_dir start_pos reg_size value) else 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) in - if is_top_level then (request,Nothing) - else (request,Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env))) + if is_top_level then (request,Nothing,Nothing) + else (request,Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env)),Nothing) | Tag_alias -> let request = (match in_env aliases name with @@ -2505,10 +2513,10 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level | _ -> (Error l "Internal error: alias vector types ill formed", l_mem, l_env) end) | _ -> (Error l "Internal error: alias spec ill formed", l_mem, l_env) end) | _ -> (Error l ("Internal error: alias not found for id " ^(get_id id)),l_mem,l_env) end) in - (request,Nothing) + (request,Nothing,Nothing) | _ -> ((Error l ("Internal error: writing to id with tag other than extern, empty, or alias " ^ (get_id id)), - l_mem,l_env),Nothing) + l_mem,l_env),Nothing,Nothing) end | LEXP_memory id exps -> match (exp_list mode t_level (fun exps env -> (E_aux (E_tuple exps) (Unknown,Nothing),env)) @@ -2526,12 +2534,12 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (Action act (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env lm Top), lm,l_env) in - if is_top_level then (request,Nothing) + if is_top_level then (request,Nothing,Nothing) else (request, Just (fun e env-> let (parms,env) = (to_exps mode env (match v with | V_tuple vs -> vs | v -> [v] end)) in - (LEXP_aux (LEXP_memory id parms) (l,annot), env))) + (LEXP_aux (LEXP_memory id parms) (l,annot), env)), Nothing) | Tag_global -> let name = get_id id in (match Map.lookup name fdefs with @@ -2542,17 +2550,17 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level | v -> V_tuple [v;value] end in (match find_funcl t_level funcls new_vals with | [] -> ((Error l ("No matching pattern for function " ^ name ^ - " on value " ^ (string_of_value new_vals)),l_mem,l_env),Nothing) + " on value " ^ (string_of_value new_vals)),l_mem,l_env),Nothing, Nothing) | [(env,used_unknown,exp)] -> (match (if mode.eager_eval then (interp_main mode t_level env (emem name) exp) else (debug_out (Just name) (Just new_vals) exp t_level (emem name) env)) with - | (Value ret, _,_) -> ((Value ret, l_mem,l_env),Nothing) + | (Value ret, _,_) -> ((Value ret, l_mem,l_env),Nothing, Nothing) | (Action action stack,lm,le) -> (((update_stack (Action action stack) (fun stack -> (Hole_frame redex_id (E_aux (E_id redex_id) (l,(intern_annot annot))) - t_level l_env l_mem stack))), l_mem,l_env), Nothing) - | (e,lm,le) -> ((e,lm,le),Nothing) end) + t_level l_env l_mem stack))), l_mem,l_env), Nothing, Nothing) + | (e,lm,le) -> ((e,lm,le),Nothing,Nothing) end) | multi_matches -> let (lets,taint_env) = List.foldr (fun (env,_,exp) (rst,taint_env) -> @@ -2560,10 +2568,10 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level let (branches,maybe_id) = fix_up_nondet typ lets (l,annot) in (interp_main mode t_level taint_env lm (E_aux (E_nondet branches) (l,non_det_annot annot maybe_id)), - Nothing) + Nothing, Nothing) end) | Nothing -> - ((Error l ("Internal error: function unfound " ^ name),lm,le),Nothing) end) + ((Error l ("Internal error: function unfound " ^ name),lm,le),Nothing,Nothing) end) | Tag_spec -> let name = get_id id in (match Map.lookup name fdefs with @@ -2574,17 +2582,17 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level | v -> V_tuple [v;value] end in (match find_funcl t_level funcls new_vals with | [] -> ((Error l ("No matching pattern for function " ^ name ^ - " on value " ^ (string_of_value new_vals)),l_mem,l_env),Nothing) + " on value " ^ (string_of_value new_vals)),l_mem,l_env),Nothing,Nothing) | [(env,used_unknown,exp)] -> (match (if mode.eager_eval then (interp_main mode t_level env (emem name) exp) else (debug_out (Just name) (Just new_vals) exp t_level (emem name) env)) with - | (Value ret, _,_) -> ((Value ret, l_mem,l_env),Nothing) + | (Value ret, _,_) -> ((Value ret, l_mem,l_env),Nothing,Nothing) | (Action action stack,lm,le) -> (((update_stack (Action action stack) (fun stack -> (Hole_frame redex_id (E_aux (E_id redex_id) (l,(intern_annot annot))) - t_level l_env l_mem stack))), l_mem,l_env), Nothing) - | (e,lm,le) -> ((e,lm,le),Nothing) end) + t_level l_env l_mem stack))), l_mem,l_env), Nothing, Nothing) + | (e,lm,le) -> ((e,lm,le),Nothing,Nothing) end) | multi_matches -> let (lets,taint_env) = List.foldr (fun (env,_,exp) (rst,taint_env) -> @@ -2592,18 +2600,18 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level let (branches,maybe_id) = fix_up_nondet typ lets (l,annot) in (interp_main mode t_level taint_env lm (E_aux (E_nondet branches) (l,non_det_annot annot maybe_id)), - Nothing) + Nothing,Nothing) end) | Nothing -> - ((Error l ("Internal error: function unfound " ^ name),lm,le),Nothing) end) - | _ -> ((Error l "Internal error: unexpected tag for memory or register write", lm,le),Nothing) + ((Error l ("Internal error: function unfound " ^ name),lm,le),Nothing,Nothing) end) + | _ -> ((Error l "Internal error: unexpected tag for memory or register write", lm,le),Nothing,Nothing) end) | (Action a s,lm, le) -> ((Action a s,lm,le), Just (fun (E_aux e _) env -> (match e with | E_tuple es -> (LEXP_aux (LEXP_memory id es) (l,annot), env) - | _ -> Assert_extra.failwith "Lexp builder not well formed" end))) - | e -> (e,Nothing) end + | _ -> Assert_extra.failwith "Lexp builder not well formed" end)), Nothing) + | e -> (e,Nothing,Nothing) end | LEXP_cast typc id -> let name = get_id id in match tag with @@ -2615,54 +2623,55 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level let (LMem owner c m s) = l_mem in let l_mem = (LMem owner (c+1) m s) in ((Value (V_lit (L_aux L_unit l)), update_mem mode.track_lmem l_mem c value, - (add_to_env (id,(V_boxref c typ)) l_env)),Nothing) + (add_to_env (id,(V_boxref c typ)) l_env)),Nothing, Nothing) end - else ((Error l ("LEXP:cast1: Undefined id " ^ (get_id id)),l_mem,l_env),Nothing) + else ((Error l ("LEXP:cast1: Undefined id " ^ (get_id id)),l_mem,l_env),Nothing, Nothing) | v -> - if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing) - else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_cast typc id) (l,annot), env))) + if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing, Nothing) + else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_cast typc id) (l,annot), env)), Nothing) end | Tag_set -> match detaint (in_lenv l_env id) with | ((V_boxref n t) as v) -> if is_top_level then ((Value (V_lit (L_aux L_unit l)), - update_mem mode.track_lmem l_mem n (recenter_val t value), l_env),Nothing) + update_mem mode.track_lmem l_mem n (recenter_val t value), l_env),Nothing,Nothing) else ((Value v, l_mem, l_env), - Just (fun e env -> (LEXP_aux (LEXP_cast typc id) (l,annot), env))) + Just (fun e env -> (LEXP_aux (LEXP_cast typc id) (l,annot), env)), Nothing) | V_unknown -> if is_top_level then begin let (LMem owner c m s) = l_mem in let l_mem = (LMem owner (c+1) m s) in ((Value (V_lit (L_aux L_unit l)), update_mem mode.track_lmem l_mem c value, - (add_to_env (id,(V_boxref c typ)) l_env)),Nothing) + (add_to_env (id,(V_boxref c typ)) l_env)),Nothing,Nothing) end - else ((Error l ("LEXP:cast2: Undefined id " ^ (get_id id)),l_mem,l_env),Nothing) + else ((Error l ("LEXP:cast2: Undefined id " ^ (get_id id)),l_mem,l_env),Nothing,Nothing) | v -> - if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing) - else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_cast typc id) (l,annot), env))) + if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing,Nothing) + else ((Value v,l_mem,l_env), + Just (fun e env -> (LEXP_aux(LEXP_cast typc id) (l,annot), env)),Nothing) end | Tag_empty -> match detaint (in_lenv l_env id) with | ((V_boxref n t) as v) -> if is_top_level then ((Value (V_lit (L_aux L_unit l)), - update_mem mode.track_lmem l_mem n (recenter_val t value), l_env),Nothing) + update_mem mode.track_lmem l_mem n (recenter_val t value), l_env),Nothing,Nothing) else ((Value v, l_mem, l_env), - Just (fun e env -> (LEXP_aux (LEXP_cast typc id) (l,annot), env))) + Just (fun e env -> (LEXP_aux (LEXP_cast typc id) (l,annot), env)), Nothing) | V_unknown -> if is_top_level then begin let (LMem owner c m s) = l_mem in let l_mem = (LMem owner (c+1) m s) in ((Value (V_lit (L_aux L_unit l)), update_mem mode.track_lmem l_mem c value, - (add_to_env (id,(V_boxref c typ)) l_env)),Nothing) + (add_to_env (id,(V_boxref c typ)) l_env)),Nothing,Nothing) end - else ((Error l ("LEXP:cast3: Undefined id " ^ (get_id id)),l_mem,l_env),Nothing) + else ((Error l ("LEXP:cast3: Undefined id " ^ (get_id id)),l_mem,l_env),Nothing,Nothing) | v -> - if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing) - else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_cast typc id) (l,annot), env))) + if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing,Nothing) + else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_cast typc id) (l,annot), env)),Nothing) end | Tag_extern _ -> let regf = @@ -2678,27 +2687,44 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level else 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) in - if is_top_level then (request,Nothing) - else (request,Just (fun e env -> (LEXP_aux (LEXP_cast typc id) (l,annot), env))) + if is_top_level then (request,Nothing,Nothing) + else (request,Just (fun e env -> (LEXP_aux (LEXP_cast typc id) (l,annot), env)),Nothing) | _ -> ((Error l ("Internal error: writing to id not extern or empty " ^(get_id id)),l_mem,l_env), - Nothing) + Nothing,Nothing) end | LEXP_tup ltups -> match (ltups,value) with - | ([],_) -> ((Error l "Internal error: found an empty tuple of assignments as an lexp", l_mem, l_env), Nothing) + | ([],_) -> + ((Error l "Internal error: found an empty tuple of assignments as an lexp", l_mem, l_env), Nothing,Nothing) | ([le],V_tuple[v]) -> create_write_message_or_update mode t_level v l_env l_mem true le | (le::ltups,V_tuple (v::vs)) -> + let new_v = V_tuple vs in (match (create_write_message_or_update mode t_level v l_env l_mem true le) with - | ((Value v_whole,lm,le),Nothing) -> - create_write_message_or_update mode t_level (V_tuple vs) le lm true (LEXP_aux (LEXP_tup ltups) (l,annot)) - | _ -> ((Error l "In progress",l_mem,l_env),Nothing) end) + | ((Value v_whole,lm,le),Nothing,Nothing) -> + create_write_message_or_update mode t_level new_v le lm true (LEXP_aux (LEXP_tup ltups) (l,annot)) + | ((Action act stack,lm,le),Nothing,Nothing) -> + ((Action act stack,lm,le), Just (fun e env -> (LEXP_aux (LEXP_tup ltups) (l,annot),env)), Just new_v) + | ((Action act stack,lm,le), Just le_builder, Nothing) -> + ((Action act stack,lm,le), + Just (fun e env -> + let (lexp,env) = le_builder e env in + (LEXP_aux (LEXP_tup (lexp::ltups)) (l,annot),env)), Just value) + | ((Action act stack, lm,le), Just le_builder, Just v) -> + ((Action act stack, lm, le), + Just (fun e env -> + let (lexp,env) = le_builder e env in + (LEXP_aux (LEXP_tup (lexp::ltups)) (l,annot),env)), Just (V_tuple (v::vs))) + | ((Error l msg,lm,le),_,_) -> ((Error l msg,lm,le),Nothing,Nothing) + | _ -> + ((Error l "Internal error: Unexpected pattern match failure in LEXP_tup",l_mem,l_env),Nothing,Nothing) + end) end | LEXP_vector lexp exp -> match (interp_main mode t_level l_env l_mem exp) with | (Value i,lm,le) -> (match detaint i with - | V_unknown -> ((Value i,lm,le),Nothing) + | V_unknown -> ((Value i,lm,le),Nothing,Nothing) | V_lit (L_aux (L_num n) ln) -> let next_builder le_builder = (fun e env -> @@ -2707,23 +2733,23 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (LEXP_aux (LEXP_vector lexp ie) (l,annot), env)) in let n = natFromInteger n in (match (create_write_message_or_update mode t_level value l_env lm false lexp) with - | ((Value v_whole,lm,le),maybe_builder) -> + | ((Value v_whole,lm,le),maybe_builder,maybe_value) -> let v = detaint v_whole in let nth _ = detaint (access_vector v n) in (match v with - | V_unknown -> ((Value v_whole,lm,le),Nothing) + | V_unknown -> ((Value v_whole,lm,le),Nothing,Nothing) | V_boxref i _ -> (match (in_mem lm i,is_top_level,maybe_builder) with | ((V_vector _ _ _ as vec),true,_) -> let new_vec = fupdate_vector_slice vec (V_vector 1 default_dir [value]) n n in ((Value (V_lit (L_aux L_unit Unknown)), - update_mem mode.track_lmem lm i new_vec, l_env), Nothing) + update_mem mode.track_lmem lm i new_vec, l_env), Nothing,Nothing) | ((V_track (V_vector _ _ _ as vec) r), true,_) -> let new_vec = fupdate_vector_slice vec (V_vector 1 default_dir [value]) n n in ((Value (V_lit (L_aux L_unit Unknown)), - update_mem mode.track_lmem lm i (taint new_vec r),l_env),Nothing) + update_mem mode.track_lmem lm i (taint new_vec r),l_env),Nothing,Nothing) | ((V_vector _ _ _ as vec),false, Just lexp_builder) -> - ((Value (access_vector vec n), lm, l_env), Just (next_builder lexp_builder)) + ((Value (access_vector vec n), lm, l_env), Just (next_builder lexp_builder),Nothing) | (v,_,_) -> Assert_extra.failwith("no vector findable in set bit, found " ^ (string_of_value v)) end ) @@ -2736,7 +2762,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (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), - Nothing) + Nothing,Nothing) | (V_register regform,false,Just lexp_builder) -> let start_pos = reg_start_pos regform in let reg_size = reg_size regform in @@ -2744,17 +2770,17 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (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), - Just (next_builder lexp_builder)) + Just (next_builder lexp_builder),maybe_value) | (V_boxref n t,true,_) -> ((Value (V_lit (L_aux L_unit Unknown)), update_mem mode.track_lmem lm n value, l_env), - Nothing) - | (V_unknown,true,_) -> ((Value (V_lit (L_aux L_unit Unknown)), lm, l_env),Nothing) + Nothing,Nothing) + | (V_unknown,true,_) -> ((Value (V_lit (L_aux L_unit Unknown)), lm, l_env),Nothing,Nothing) | (v,true,_) -> - ((Error l "Vector does not contain reg or register values",lm,l_env),Nothing) + ((Error l "Vector does not contain reg or register values",lm,l_env),Nothing,Nothing) | ((V_boxref n t),false, Just lexp_builder) -> - ((Value (in_mem lm n),lm, l_env),Just (next_builder lexp_builder)) + ((Value (in_mem lm n),lm, l_env),Just (next_builder lexp_builder),Nothing) | (v,false, Just lexp_builder) -> - ((Value v,lm,le), Just (next_builder lexp_builder)) + ((Value v,lm,le), Just (next_builder lexp_builder),Nothing) | _ -> Assert_extra.failwith "Vector assignment logic incomplete" end) | V_vector_sparse n m inc vs d -> @@ -2764,63 +2790,63 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level let reg_size = reg_size regform in ((Action (Write_reg regform Nothing (update_vector_start default_dir start_pos reg_size 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),Nothing) + l_mem,l_env),Nothing,Nothing) | (V_register regform,false,Just lexp_builder) -> let start_pos = reg_start_pos regform in let reg_size = reg_size regform in ((Action (Write_reg regform Nothing (update_vector_start default_dir start_pos reg_size 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), - Just (next_builder lexp_builder)) + Just (next_builder lexp_builder),Nothing) | (V_boxref n t,true,_) -> ((Value (V_lit (L_aux L_unit Unknown)), update_mem mode.track_lmem lm n value, l_env), - Nothing) + Nothing,Nothing) | (v,true,_) -> ((Error l ("Vector does not contain reg or register values " ^ (string_of_value v)), - lm,l_env), Nothing) + lm,l_env), Nothing,Nothing) | ((V_boxref n t),false, Just lexp_builder) -> - ((Value (in_mem lm n),lm, l_env),Just (next_builder lexp_builder)) + ((Value (in_mem lm n),lm, l_env),Just (next_builder lexp_builder),Nothing) | (v,false, Just lexp_builder) -> - ((Value v,lm,le), Just (next_builder lexp_builder)) + ((Value v,lm,le), Just (next_builder lexp_builder), Nothing) | _ -> Assert_extra.failwith "Vector assignment logic incomplete" end) | v -> - ((Error l ("Vector access to write of non-vector" ^ (string_of_value v)),lm,l_env),Nothing) + ((Error l ("Vector access to write of non-vector" ^ (string_of_value v)),lm,l_env),Nothing,Nothing) end) - | ((Action a s,lm,le),Just lexp_builder) -> + | ((Action a s,lm,le),Just lexp_builder,maybe_value) -> (match (a,is_top_level) with | ((Write_reg regf Nothing value),true) -> ((Action (Write_reg regf (Just (n,n)) (if (vector_length value) = 1 then (update_vector_start default_dir n 1 value) - else (access_vector value n))) s, lm,le), Nothing) + else (access_vector value n))) s, lm,le), Nothing, Nothing) | ((Write_reg regf Nothing value),false) -> ((Action (Write_reg regf (Just (n,n)) (if (vector_length value) = 1 then (update_vector_start default_dir n 1 value) else (access_vector value n))) s,lm,le), - Just (next_builder lexp_builder)) + Just (next_builder lexp_builder), Nothing) | ((Write_mem id a Nothing value),true) -> - ((Action (Write_mem id a (Just (n,n)) value) s,lm,le), Nothing) + ((Action (Write_mem id a (Just (n,n)) value) s,lm,le), Nothing, Nothing) | ((Write_mem id a Nothing value),false) -> - ((Action (Write_mem id a (Just (n,n)) value) s,lm,le), Just (next_builder lexp_builder)) - | _ -> ((Action a s,lm,le), Just (next_builder lexp_builder)) end) + ((Action (Write_mem id a (Just (n,n)) value) s,lm,le), Just (next_builder lexp_builder), Nothing) + | _ -> ((Action a s,lm,le), Just (next_builder lexp_builder), Nothing) end) | e -> e end) | v -> - ((Error l ("Vector access must be a number given " ^ (string_of_value v)),lm,le),Nothing) end) + ((Error l ("Vector access must be a number given " ^ (string_of_value v)),lm,le),Nothing,Nothing) end) | (Action a s,lm,le) -> - ((Action a s,lm,le), Just (fun e env -> (LEXP_aux (LEXP_vector lexp e) (l,annot), env))) - | e -> (e,Nothing) end + ((Action a s,lm,le), Just (fun e env -> (LEXP_aux (LEXP_vector lexp e) (l,annot), env)), Nothing) + | e -> (e,Nothing,Nothing) end | LEXP_vector_range lexp exp1 exp2 -> match (interp_main mode t_level l_env l_mem exp1) with | (Value i1, lm, le) -> (match detaint i1 with - | V_unknown -> ((Value i1,lm,le),Nothing) + | V_unknown -> ((Value i1,lm,le),Nothing,Nothing) | V_lit (L_aux (L_num n1) ln1) -> (match (interp_main mode t_level l_env l_mem exp2) with | (Value i2,lm,le) -> (match detaint i2 with - | V_unknown -> ((Value i2,lm,le),Nothing) + | V_unknown -> ((Value i2,lm,le),Nothing,Nothing) | V_lit (L_aux (L_num n2) ln2) -> let next_builder le_builder = (fun e env -> @@ -2830,73 +2856,73 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (LEXP_aux (LEXP_vector_range lexp e1 e2) (l,annot), env)) in let (n1,n2) = (natFromInteger n1,natFromInteger n2) in (match (create_write_message_or_update mode t_level value l_env lm false lexp) with - | ((Value v,lm,le), Just lexp_builder) -> + | ((Value v,lm,le), Just lexp_builder,_) -> (match (detaint v,is_top_level) with | (V_vector m inc vs,true) -> ((Value (V_lit (L_aux L_unit Unknown)), - update_vector_slice mode.track_lmem v value n1 n2 lm, l_env), Nothing) + update_vector_slice mode.track_lmem v value n1 n2 lm, l_env), Nothing, Nothing) | (V_boxref _ _, true) -> ((Value (V_lit (L_aux L_unit Unknown)), - update_vector_slice mode.track_lmem v value n1 n2 lm, l_env), Nothing) + update_vector_slice mode.track_lmem v value n1 n2 lm, l_env), Nothing, Nothing) | (V_vector m inc vs,false) -> - ((Value (slice_vector v n1 n2),lm,l_env), Just (next_builder lexp_builder)) + ((Value (slice_vector v n1 n2),lm,l_env), Just (next_builder lexp_builder), Nothing) | (V_register regform,true) -> let start_pos = reg_start_pos regform in let reg_size = reg_size regform in ((Action (Write_reg regform (Just (n1,n2)) (update_vector_start default_dir start_pos reg_size v)) (mk_thunk l annot t_level l_env l_mem), l_mem,l_env), - Just (next_builder lexp_builder)) + Just (next_builder lexp_builder), Nothing) | (V_unknown,_) -> let inc = n1 < n2 in let start = if inc then n1 else (n2-1) in let size = if inc then n2-n1 +1 else n1 -n2 +1 in ((Value (V_vector start (if inc then IInc else IDec) (List.replicate size V_unknown)), - lm,l_env),Nothing) - | _ -> ((Error l "Vector required",lm,le),Nothing) end) - | ((Action (Write_reg regf Nothing value) s, lm,le), Just lexp_builder) -> + lm,l_env),Nothing,Nothing) + | _ -> ((Error l "Vector required",lm,le),Nothing,Nothing) end) + | ((Action (Write_reg regf Nothing value) s, lm,le), Just lexp_builder,_) -> let len = (if n1 < n2 then n2 -n1 else n1 - n2) +1 in ((Action (Write_reg regf (Just (n1,n2)) (if (vector_length value) <= len then (update_vector_start default_dir n1 len value) else (slice_vector value n1 n2))) s,lm,le), - Just (next_builder lexp_builder)) - | ((Action (Write_mem id a Nothing value) s,lm,le), Just lexp_builder) -> - ((Action (Write_mem id a (Just (n1,n2)) value) s,lm,le), Just (next_builder lexp_builder)) - | ((Action a s,lm,le), Just lexp_builder) -> - ((Action a s,lm,le), Just (next_builder lexp_builder)) + Just (next_builder lexp_builder), Nothing) + | ((Action (Write_mem id a Nothing value) s,lm,le), Just lexp_builder,_) -> + ((Action (Write_mem id a (Just (n1,n2)) value) s,lm,le), Just (next_builder lexp_builder), Nothing) + | ((Action a s,lm,le), Just lexp_builder,_ ) -> + ((Action a s,lm,le), Just (next_builder lexp_builder), Nothing) | e -> e end) - | _ -> ((Error l "Vector slice requires a number", lm, le),Nothing) end) + | _ -> ((Error l "Vector slice requires a number", lm, le),Nothing,Nothing) end) | (Action a s,lm,le) -> ((Action a s,lm, le), Just (fun e env -> let (e1,env) = to_exp mode env i1 in - (LEXP_aux (LEXP_vector_range lexp e1 e) (l,annot), env))) - | e -> (e,Nothing) end) - | _ -> ((Error l "Vector slice requires a number", lm, le),Nothing) end) + (LEXP_aux (LEXP_vector_range lexp e1 e) (l,annot), env)), Nothing) + | e -> (e,Nothing,Nothing) end) + | _ -> ((Error l "Vector slice requires a number", lm, le),Nothing,Nothing) end) | (Action a s,lm,le) -> - ((Action a s, lm,le), Just (fun e env -> (LEXP_aux (LEXP_vector_range lexp e exp2) (l,annot), env))) - | e -> (e,Nothing) end + ((Action a s, lm,le), Just (fun e env -> (LEXP_aux (LEXP_vector_range lexp e exp2) (l,annot), env)), Nothing) + | e -> (e,Nothing,Nothing) end | LEXP_field lexp id -> (match (create_write_message_or_update mode t_level value l_env l_mem false lexp) with - | ((Value (V_record t fexps),lm,le),Just lexp_builder) -> + | ((Value (V_record t fexps),lm,le),Just lexp_builder,_) -> let next_builder = Just (fun e env -> let (lexp,env) = (lexp_builder e env) in (LEXP_aux (LEXP_field lexp id) (l,annot), env)) in match (in_env (env_from_list fexps) (get_id id),is_top_level) with | (Just (V_boxref n t),true) -> - ((Value (V_lit (L_aux L_unit l)), update_mem mode.track_lmem lm n value, l_env),Nothing) - | (Just (V_boxref n t),false) -> ((Value (in_mem lm n),lm,l_env),next_builder) - | (Just v, true) -> ((Error l "Mutating a field access requires a reg type",lm,le),Nothing) - | (Just v,false) -> ((Value v,lm,l_env),next_builder) - | (Nothing,_) -> ((Error l "Field not found in specified record",lm,le),Nothing) end - | ((Action a s,lm,le), Just lexp_builder) -> + ((Value (V_lit (L_aux L_unit l)), update_mem mode.track_lmem lm n value, l_env),Nothing,Nothing) + | (Just (V_boxref n t),false) -> ((Value (in_mem lm n),lm,l_env),next_builder,Nothing) + | (Just v, true) -> ((Error l "Mutating a field access requires a reg type",lm,le),Nothing,Nothing) + | (Just v,false) -> ((Value v,lm,l_env),next_builder,Nothing) + | (Nothing,_) -> ((Error l "Field not found in specified record",lm,le),Nothing,Nothing) end + | ((Action a s,lm,le), Just lexp_builder,_) -> let next_builder = Just (fun e env -> let (lexp,env) = (lexp_builder e env) in (LEXP_aux (LEXP_field lexp id) (l,annot), env)) in match a with - | Read_reg _ _ -> ((Action a s,lm,le), next_builder) - | Read_mem _ _ _ -> ((Action a s,lm,le), next_builder) - | Call_extern _ _ -> ((Action a s,lm,le), next_builder) + | Read_reg _ _ -> ((Action a s,lm,le), next_builder, Nothing) + | Read_mem _ _ _ -> ((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 -> match in_env subregs id' with | Just(indexes) -> @@ -2907,10 +2933,10 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (update_vector_start default_dir (get_first_index_range ir) (get_index_range_size ir) value)) s, lm,le), - (if is_top_level then Nothing else next_builder)) - | _ -> ((Error l "Internal error, unrecognized write, no field",lm,le),Nothing) + (if is_top_level then Nothing else next_builder), Nothing) + | _ -> ((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) 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 -> match in_env subregs id' with | Just(indexes) -> @@ -2921,11 +2947,11 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (update_vector_start default_dir (get_first_index_range ir) (get_index_range_size ir) value)) s, lm,le), - (if is_top_level then Nothing else next_builder)) - | _ -> ((Error l "Internal error, unrecognized write, no field",lm,le),Nothing) + (if is_top_level then Nothing else next_builder), Nothing) + | _ -> ((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) end - | _ -> ((Error l "Internal error, unrecognized write, no matching action",lm,le),Nothing) + | Nothing -> ((Error l "Internal error, unrecognized write, no subreges",lm,le),Nothing,Nothing) end + | _ -> ((Error l "Internal error, unrecognized write, no matching action",lm,le),Nothing,Nothing) end | e -> e end) end -- cgit v1.2.3