diff options
| -rw-r--r-- | src/lem_interp/interp.lem | 257 |
1 files changed, 159 insertions, 98 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 9cf0e41d..201bd0cc 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -346,6 +346,13 @@ let list_nth l n = List_extra.nth l (natFromInteger n) val list_length : forall 'a . list 'a -> integer let list_length l = integerFromNat (List.length l) +val taint: value -> list reg_form -> value +let taint value regs = + match value with + | V_track value rs -> V_track value (regs ++ rs) + | _ -> V_track value regs +end + val access_vector : value -> integer -> value let rec access_vector v n = match v with @@ -502,9 +509,9 @@ let rec fupdate_vector_slice vec replace start stop = | (V_vector_sparse m n inc vals d,V_vector _ _ reps) -> let (_,repsi) = List.foldr (fun r (i,rs) -> ((if inc then i+1 else i-1), (i,r)::rs)) (start,[]) reps in (V_vector_sparse m n inc (replace_sparse (if inc then (<) else (>)) vals repsi) d) - | (V_track v r, V_track vr rr) -> (V_track (fupdate_vector_slice v vr start stop) (r++rr)) - | (V_track v r, replace) -> V_track (fupdate_vector_slice v replace start stop) r - | (vec, V_track vr rr) -> V_track (fupdate_vector_slice vec vr start stop) rr + | (V_track v r, V_track vr rr) -> (taint (fupdate_vector_slice v vr start stop) (r++rr)) + | (V_track v r, replace) -> taint (fupdate_vector_slice v replace start stop) r + | (vec, V_track vr rr) -> taint (fupdate_vector_slice vec vr start stop) rr end val in_ctors : list (id * typ) -> id -> maybe typ @@ -745,7 +752,7 @@ let rec find_function (Defs defs) id = val match_pattern : pat tannot -> value -> bool * bool * lenv let rec match_pattern (P_aux p _) value_whole = let value = match value_whole with | V_track v _ -> v | _ -> value_whole end in - let taint v = + let taint_pat v = match (v,value_whole) with | (V_track v r,V_track _ wr) -> V_track v (r++wr) | (v, V_track _ r) -> V_track v r @@ -787,7 +794,7 @@ let rec match_pattern (P_aux p _) value_whole = then foldr2 (fun pat value (matched_p,used_unknown,bounds) -> if matched_p then - let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint value) in + let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint_pat value) in (matched_p, (used_unknown || used_unknown'), (union_env new_bounds bounds)) else (false,false,eenv)) (true,false,eenv) pats vals else (false,false,eenv) @@ -796,7 +803,7 @@ let rec match_pattern (P_aux p _) value_whole = then foldr2 (fun pat value (matched_p,used_unknown,bounds) -> if matched_p then - let (matched_p,used_unknown',new_bounds) = match_pattern pat (V_track value r) in + let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint value r) in (matched_p, (used_unknown || used_unknown'), (union_env new_bounds bounds)) else (false,false,eenv)) (true,false,eenv) pats vals else (false,false,eenv) @@ -833,7 +840,7 @@ let rec match_pattern (P_aux p _) value_whole = then foldr2 (fun pat value (matched_p,used_unknown,bounds) -> if matched_p then - let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint value) in + let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint_pat value) in (matched_p, (used_unknown||used_unknown'), (union_env new_bounds bounds)) else (false,false,eenv)) (true,false,eenv) (if inc then pats else List.reverse pats) vals @@ -847,7 +854,7 @@ let rec match_pattern (P_aux p _) value_whole = then let (matched_p,used_unknown',new_bounds) = match_pattern pat (match List.lookup i vals with | Nothing -> d - | Just v -> (taint v) end) in + | Just v -> (taint_pat v) end) in ((if inc then i+1 else i-1),matched_p,used_unknown||used_unknown',(union_env new_bounds bounds)) else (i,false,false,eenv)) (n,true,false,eenv) pats in (matched_p,used_unknown,bounds) @@ -861,7 +868,7 @@ let rec match_pattern (P_aux p _) value_whole = let v_len = if inc then list_length vals + n else n - list_length vals in List.foldr (fun (i,pat) (matched_p,used_unknown,bounds) -> if matched_p && i < v_len then - let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint (list_nth vals (if inc then i+n else i-n))) in + let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint_pat (list_nth vals (if inc then i+n else i-n))) in (matched_p,used_unknown||used_unknown',(union_env new_bounds bounds)) else (false,false,eenv)) (true,false,eenv) ipats @@ -869,7 +876,7 @@ let rec match_pattern (P_aux p _) value_whole = List.foldr (fun (i,pat) (matched_p,used_unknown,bounds) -> if matched_p && i < m then let (matched_p,used_unknown',new_bounds) = - match_pattern pat (match List.lookup i vals with | Nothing -> d | Just v -> (taint v) end) in + match_pattern pat (match List.lookup i vals with | Nothing -> d | Just v -> (taint_pat v) end) in (matched_p,used_unknown||used_unknown',(union_env new_bounds bounds)) else (false,false,eenv)) (true,false,eenv) ipats @@ -894,7 +901,7 @@ let rec match_pattern (P_aux p _) value_whole = if ((List.length pats)= (List.length vals)) then foldr2 (fun pat v (matched_p,used_unknown,bounds) -> if matched_p then - let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint v) in + let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint_pat v) in (matched_p,used_unknown ||used_unknown', (union_env bounds new_bounds)) else (false,false,eenv)) (true,false,eenv) pats vals @@ -908,7 +915,7 @@ let rec match_pattern (P_aux p _) value_whole = if ((List.length pats)= (List.length vals)) then foldr2 (fun pat v (matched_p,used_unknown,bounds) -> if matched_p then - let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint v) in + let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint_pat v) in (matched_p,used_unknown|| used_unknown', (union_env bounds new_bounds)) else (false,false,eenv)) (true,false,eenv) pats vals @@ -1064,12 +1071,12 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = (*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 -> (V_track (V_vector i 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 -> (V_track (V_vector_sparse i 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)) (fun a -> update_stack a (add_to_top_frame (fun e env -> (E_aux (E_cast ctyp e) (l,annot), env)))) | E_id id -> @@ -1309,13 +1316,13 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = | V_vector _ _ _ -> (Value (access_vector vvec n),lm,le) | V_track ((V_vector _ _ _) as vvec) r -> (match iv_whole with - | V_track _ ir -> (Value (V_track (access_vector vvec n) (r++ir)),lm,le) - | _ -> (Value (V_track (access_vector vvec n) r),lm,le) end) + | V_track _ ir -> (Value (taint (access_vector vvec n) (r++ir)),lm,le) + | _ -> (Value (taint (access_vector vvec n) r),lm,le) end) | V_vector_sparse _ _ _ _ _ -> (Value (access_vector vvec n),lm,le) | V_track ((V_vector_sparse _ _ _ _ _) as vvec) r -> (match iv_whole with - | V_track _ ir -> (Value (V_track (access_vector vvec n) (r++ir)),lm,le) - | _ -> (Value (V_track (access_vector vvec n) r),lm,le) end) + | V_track _ ir -> (Value (taint (access_vector vvec n) (r++ir)),lm,le) + | _ -> (Value (taint (access_vector vvec n) r),lm,le) end) | V_unknown -> (Value V_unknown,lm,le) | _ -> (Error l "Vector access of non-vector",lm,le)end) (fun a -> @@ -1364,13 +1371,13 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = | (V_lit (L_aux (L_num n1) ln1),V_lit (L_aux (L_num n2) ln2)) -> (match (vvec,tracking) with | (V_vector _ _ _,[]) -> (Value (slice_vector vvec n1 n2),lm,le) - | (V_vector _ _ _,tr) -> (Value (V_track (slice_vector vvec n1 n2) tr), lm,le) + | (V_vector _ _ _,tr) -> (Value (taint (slice_vector vvec n1 n2) tr), lm,le) | (V_track ((V_vector _ _ _) as vvec) r,_) -> - (Value (V_track (slice_vector vvec n1 n2) (r++tracking)), lm,le) + (Value (taint (slice_vector vvec n1 n2) (r++tracking)), lm,le) | (V_vector_sparse _ _ _ _ _,[]) -> (Value (slice_vector vvec n1 n2), lm,le) - | (V_vector_sparse _ _ _ _ _,tr) -> (Value (V_track (slice_vector vvec n1 n2) tr),lm,le) + | (V_vector_sparse _ _ _ _ _,tr) -> (Value (taint (slice_vector vvec n1 n2) tr),lm,le) | (V_track ((V_vector_sparse _ _ _ _ _) as vvec) r,_) -> - (Value (V_track (slice_vector vvec n1 n2) (r++tracking)), lm,le) + (Value (taint (slice_vector vvec n1 n2) (r++tracking)), lm,le) | (V_unknown,_) -> (Value V_unknown,lm,le) | _ -> (Error l "Vector slice of non-vector",lm,le) end) end) @@ -1408,10 +1415,10 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = match (vec,tracking) with | (V_vector _ _ _,[]) -> (Value (fupdate_vec vec n1 vup), lm,le) | (V_track ((V_vector _ _ _) as vvec) r, tracking) -> - (Value (V_track (fupdate_vec vec n1 vup) (r++tracking)),lm,le) + (Value (taint (fupdate_vec vec n1 vup) (r++tracking)),lm,le) | (V_vector_sparse _ _ _ _ _,[]) -> (Value (fupdate_vec vec n1 vup),lm,le) | (V_track ((V_vector_sparse _ _ _ _ _) as vvec) r, tracking) -> - (Value (V_track (fupdate_vec vec n1 vup) (r++tracking)),lm,le) + (Value (taint (fupdate_vec vec n1 vup) (r++tracking)),lm,le) | (V_unknown,_) -> (Value V_unknown, lm, le) | _ -> (Error l "Update of vector given non-vector",lm,le) end) (fun a -> update_stack a @@ -1438,7 +1445,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = resolve_outcome (interp_main mode t_level l_env lm i2) (fun vi2_whole lm le -> - let (vi2,tracking) = match vi2_whole with | V_track v r -> (v,(r++v1_t) | _ -> (vi2_whole,v1_t) end in + let (vi2,tracking) = match vi2_whole with | V_track v r -> (v,(r++v1_t)) | _ -> (vi2_whole,v1_t) end in match vi2 with | V_lit (L_aux (L_num n2) ln2) -> resolve_outcome @@ -1449,19 +1456,22 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = (fun vvec lm le -> match (vvec,tracking) with | (V_vector _ _ _,[]) -> (Value (fupdate_vector_slice vvec v_rep n1 n2),lm,le) + | (V_vector _ _ _,tr) -> (Value (taint (fupdate_vector_slice vvec v_rep n1 n2) tr),lm,le) | (V_track ((V_vector _ _ _) as vvec) r,t) -> - (Value (V_track (fupdate_vector_slice vvec v_rep n1 n2) (r++tracking)),lm,le) + (Value (taint (fupdate_vector_slice vvec v_rep n1 n2) (r++tracking)),lm,le) | (V_vector_sparse _ _ _ _ _,[]) -> (Value (fupdate_vector_slice vvec v_rep n1 n2),lm,le) + | (V_vector_sparse _ _ _ _ _,tr) -> (Value (taint (fupdate_vector_slice vvec v_rep n1 n2) tr),lm,le) + | (V_track ((V_vector_sparse _ _ _ _ _) as vvec) rs,tr) -> + (Value (taint (fupdate_vector_slice vvec v_rep n1 n2) (rs++tr)),lm,le) | (V_unknown,_) -> (Value V_unknown,lm,le) | _ -> (Error l "Vector update requires vector",lm,le) end) (fun a -> update_stack a (add_to_top_frame (fun v env -> let (e_rep,env') = to_exp mode env v_rep in - (E_aux (E_vector_update_subrange v - (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing)) - (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing)) - e_rep) (l,annot), env')))))) + let (ei1, env') = to_exp mode env' vi1_whole in + let (ei2, env') = to_exp mode env' vi2_whole in + (E_aux (E_vector_update_subrange v ei1 ei2 e_rep) (l,annot), env')))))) (fun a -> update_stack a (add_to_top_frame (fun e env -> @@ -1481,20 +1491,36 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = | E_vector_append e1 e2 -> resolve_outcome (interp_main mode t_level l_env l_mem e1) - (fun v1 lm le -> + (fun v1_whole lm le -> + let (v1,tracking) = match v1_whole with | V_track v r -> (v,r) | _ -> (v1_whole,[]) end in match v1 with | V_vector m inc vals1 -> (resolve_outcome (interp_main mode t_level l_env lm e2) (fun v2 lm le -> - match v2 with - | V_vector _ _ vals2 -> (Value (V_vector m inc (vals1++vals2)),lm,l_env) - | V_vector_sparse _ len _ vals2 d -> + match (v2,tracking) with + | (V_vector _ _ vals2,[]) -> (Value (V_vector m inc (vals1++vals2)),lm,l_env) + | (V_vector _ _ vals2,tr) -> (Value (V_track (V_vector m inc (vals1++vals2)) tr),lm,l_env) + | (V_track (V_vector _ _ vals2) r,tr) -> + (Value (V_track (V_vector m inc (vals1++vals2)) (r++tr)), lm,l_env) + | (V_vector_sparse _ len _ vals2 d,[]) -> let original_len = integerFromNat (List.length vals1) in let (_,sparse_vals) = List.foldr (fun v (i,vals) -> (i+1,(i,v)::vals)) (m,[]) vals1 in let sparse_update = List.map (fun (i,v) -> (i+m+original_len,v)) vals2 in (Value (V_vector_sparse m (len+original_len) inc (sparse_vals ++ sparse_update) d), lm,l_env) - | V_unknown -> (Value V_unknown,lm,l_env) + | (V_vector_sparse _ len _ vals2 d,tr) -> + let original_len = integerFromNat (List.length vals1) in + let (_,sparse_vals) = List.foldr (fun v (i,vals) -> (i+1,(i,v)::vals)) (m,[]) vals1 in + let sparse_update = List.map (fun (i,v) -> (i+m+original_len,v)) vals2 in + (Value + (V_track (V_vector_sparse m (len+original_len) inc (sparse_vals ++ sparse_update) d) tr), lm,l_env) + | (V_track (V_vector_sparse _ len _ vals2 d) reg, tr) -> + let original_len = integerFromNat (List.length vals1) in + let (_,sparse_vals) = List.foldr (fun v (i,vals) -> (i+1,(i,v)::vals)) (m,[]) vals1 in + let sparse_update = List.map (fun (i,v) -> (i+m+original_len,v)) vals2 in + (Value + (V_track (V_vector_sparse m (len+original_len) inc (sparse_vals ++ sparse_update) d) (reg++tr)), lm,l_env) + | (V_unknown,_) -> (Value V_unknown,lm,l_env) | _ -> (Error l "vector concat requires vector",lm,le) end) (fun a -> update_stack a (add_to_top_frame (fun e env -> @@ -1504,15 +1530,29 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = (resolve_outcome (interp_main mode t_level l_env lm e2) (fun v2 lm le -> - match v2 with - | V_vector _ _ vals2 -> + match (v2,tracking) with + | (V_vector _ _ vals2,[]) -> let new_len = integerFromNat (List.length vals2) in let (_,sparse_vals) = List.foldr (fun v (i,vals) -> (i+1,(i,v)::vals)) (len,[]) vals2 in (Value (V_vector_sparse m (len+new_len) inc (vals1++sparse_vals) d), lm,l_env) - | V_vector_sparse _ new_len _ vals2 _ -> + | (V_vector _ _ vals2,tr) -> + let new_len = integerFromNat (List.length vals2) in + let (_,sparse_vals) = List.foldr (fun v (i,vals) -> (i+1,(i,v)::vals)) (len,[]) vals2 in + (Value (V_track (V_vector_sparse m (len+new_len) inc (vals1++sparse_vals) d) tr), lm,l_env) + | (V_track (V_vector _ _ vals2) rs,tr) -> + let new_len = integerFromNat (List.length vals2) in + let (_,sparse_vals) = List.foldr (fun v (i,vals) -> (i+1,(i,v)::vals)) (len,[]) vals2 in + (Value (V_track (V_vector_sparse m (len+new_len) inc (vals1++sparse_vals) d) (rs++tr)), lm,l_env) + | (V_vector_sparse _ new_len _ vals2 _,[]) -> let sparse_update = List.map (fun (i,v) -> (i+len,v)) vals2 in (Value (V_vector_sparse m (len+new_len) inc (vals1 ++ sparse_update) d), lm,l_env) - | V_unknown -> (Value V_unknown,lm,l_env) + | (V_vector_sparse _ new_len _ vals2 _, tr) -> + let sparse_update = List.map (fun (i,v) -> (i+len,v)) vals2 in + (Value (V_track (V_vector_sparse m (len+new_len) inc (vals1 ++ sparse_update) d) tr), lm,l_env) + | (V_track (V_vector_sparse _ new_len _ vals2 _) rs, tr) -> + let sparse_update = List.map (fun (i,v) -> (i+len,v)) vals2 in + (Value (V_track (V_vector_sparse m (len+new_len) inc (vals1 ++ sparse_update) d) (rs++tr)), lm,l_env) + | (V_unknown,_) -> (Value V_unknown,lm,l_env) | _ -> (Error l "vector concat requires vector",lm,le) end) (fun a -> update_stack a (add_to_top_frame (fun e env -> let (e1,env') = to_exp mode env v1 in @@ -1557,9 +1597,10 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = (Action (Nondet exps) (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) | E_app f args -> - (match (exp_list mode t_level (fun es -> E_aux (E_app f es) (l,annot)) - (fun vs -> match vs with | [] -> V_lit (L_aux L_unit l) | [v] -> v | vs -> V_tuple vs end) - l_env l_mem [] args) with + (match (exp_list mode t_level + (fun es -> E_aux (E_app f es) (l,annot)) + (fun vs -> match vs with | [] -> V_lit (L_aux L_unit l) | [v] -> v | vs -> V_tuple vs end) + l_env l_mem [] args) with | (Value v,lm,le) -> let name = get_id f in (match tag with @@ -1570,9 +1611,10 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = | [] -> (Error l (String.stringAppend "No matching pattern for function " name ),l_mem,l_env) | [(env,used_unknown,exp)] -> - resolve_outcome (if mode.eager_eval - then (interp_main mode t_level env emem exp) - else (debug_out exp t_level emem env)) + resolve_outcome + (if mode.eager_eval + then (interp_main mode t_level env emem exp) + else (debug_out exp t_level emem env)) (fun ret lm le -> (Value ret, l_mem,l_env)) (fun a -> update_stack a (fun stack -> (Hole_frame (id_of_string "0") @@ -1582,7 +1624,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = let lets = List.map (fun (env,_,exp) -> env_to_let mode env exp) multi_matches in interp_main mode t_level l_env l_mem (E_aux (E_block lets) (l,annot)) end) - | Nothing -> (Error l (String.stringAppend "Internal error: function with empty tag unfound " name),lm,le) end) + | Nothing -> (Error l (String.stringAppend "Internal error: function with empty tag unfound " name),lm,le) end) | Tag_empty -> (match find_function defs f with | Just(funcls) -> @@ -1590,14 +1632,15 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = | [] -> (Error l (String.stringAppend "No matching pattern for function " name ),l_mem,l_env) | [(env,used_unknown,exp)] -> - resolve_outcome (if mode.eager_eval - then (interp_main mode t_level env emem exp) - else (debug_out exp t_level emem env)) - (fun ret lm le -> (Value ret, l_mem,l_env)) - (fun a -> update_stack a - (fun stack -> (Hole_frame (id_of_string "0") - (E_aux (E_id (Id_aux (Id "0") l)) (l,(intern_annot annot))) - t_level l_env l_mem stack))) + resolve_outcome + (if mode.eager_eval + then (interp_main mode t_level env emem exp) + else (debug_out exp t_level emem env)) + (fun ret lm le -> (Value ret, l_mem,l_env)) + (fun a -> update_stack a + (fun stack -> (Hole_frame (id_of_string "0") + (E_aux (E_id (Id_aux (Id "0") l)) (l,(intern_annot annot))) + t_level l_env l_mem stack))) end) | Nothing -> (Error l (String.stringAppend "Internal error: function with empty tag unfound " name),lm,le) end) | Tag_spec -> @@ -1613,7 +1656,9 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = else (debug_out exp t_level emem env)) (fun ret lm le -> (Value ret, l_mem,l_env)) (fun a -> update_stack a - (fun stack -> (Hole_frame (id_of_string "0") (E_aux (E_id (Id_aux (Id "0") l)) (l,(intern_annot annot))) t_level l_env l_mem stack))) + (fun stack -> + (Hole_frame (id_of_string "0") + (E_aux (E_id (Id_aux (Id "0") l)) (l,(intern_annot annot))) t_level l_env l_mem stack))) end) | Nothing -> (Error l (String.stringAppend "Specified function must be defined before executing " name),lm,le) end) | Tag_ctor -> @@ -1743,7 +1788,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = | _ -> update_stack a (add_to_top_frame (fun e env -> let (ev,env') = (to_exp mode env v) in - (E_aux (E_assign (lexp_builder e) ev) (l,annot),env'))) end)) + let (lexp,env') = (lexp_builder e env') in + (E_aux (E_assign lexp ev) (l,annot),env'))) end)) end)) (fun a -> update_stack a (add_to_top_frame (fun v env -> (E_aux (E_assign lexp v) (l,annot), env)))) end @@ -1766,7 +1812,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = end (*TODO The rebuilder function should take an environment and thread through as in to_exp and add_to_top_frame *) -and create_write_message_or_update mode t_level value l_env l_mem is_top_level ((LEXP_aux lexp (l,annot)):lexp tannot) = +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))) = let (Env defs lets regs ctors subregs aliases) = t_level in let (typ,tag,ncs,ef) = match annot with | Nothing -> (T_var "fresh_v", Tag_empty, [], (Effect_aux (Effect_set []) Unknown)) @@ -1779,7 +1825,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level ( | (V_boxref n t) -> if is_top_level then ((Value (V_lit (L_aux L_unit l)), update_mem l_mem n value, l_env),Nothing) - else ((Value (in_mem l_mem n), l_mem, l_env),Just (fun e -> LEXP_aux (LEXP_id id) (l,annot))) + else ((Value (in_mem l_mem n), l_mem, l_env),Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env))) | V_unknown -> if is_top_level then let (LMem c m) = l_mem in @@ -1787,21 +1833,22 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level ( ((Value (V_lit (L_aux L_unit l)), update_mem l_mem c value, (add_to_env (id,(V_boxref c typ)) l_env)),Nothing) else ((Error l (String.stringAppend "Unknown local id " (get_id id)),l_mem,l_env),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 -> LEXP_aux(LEXP_id id) (l,annot))) + 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_id id) (l,annot), env))) end | Tag_global -> (match in_env lets id 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 -> LEXP_aux(LEXP_id id) (l,annot))) + else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_id id) (l,annot), env))) | Nothing -> ((Error l (String.stringAppend "Undefined id " (get_id id)),l_mem,l_env),Nothing) end) | Tag_extern _ -> let regf = Reg id annot in - let request = (Action (Write_reg regf Nothing 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 -> LEXP_aux (LEXP_id id) (l,annot))) + let request = + (Action (Write_reg regf Nothing 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))) | Tag_alias -> let request = (match in_env aliases id with @@ -1813,7 +1860,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level ( (match in_env indexes subreg with | Just ir -> (Action (Write_reg (SubReg subreg (Reg reg annot') ir) Nothing value) - (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot)) + (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) | _ -> (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 " id), l_mem, l_env) end) @@ -1823,7 +1870,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level ( (match in_env indexes subreg with | Just ir -> (Action (Write_reg (SubReg subreg (Reg reg annot') ir) Nothing value) - (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot)) + (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) | _ -> (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 " id), l_mem, l_env) end) @@ -1832,7 +1879,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) _) -> (Action (Write_reg (Reg reg annot') (Just (i,i)) value) - (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot)) + (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) end) (fun a -> a) | AL_slice (RI_aux (RI_id reg) (_,annot')) start stop -> @@ -1878,11 +1925,13 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level ( let request = (Action (Write_mem id v Nothing value) (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) - else (request,Just (fun e -> - (LEXP_aux (LEXP_memory id - (fst (to_exps mode eenv (match v with | V_tuple vs -> vs | v -> [v]end)))) (l,annot)))) + 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))) end) - | (Action a s,lm, le) -> ((Action a s,lm,le), Just (fun (E_aux (E_tuple es) _) -> (LEXP_aux (LEXP_memory id es) (l,annot)))) + | (Action a s,lm, le) -> ((Action a s,lm,le), Just (fun (E_aux (E_tuple es) _) env -> (LEXP_aux (LEXP_memory id es) (l,annot), env))) | e -> (e,Nothing) end | LEXP_cast typc id -> match tag with @@ -1891,7 +1940,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level ( | V_boxref n t -> if is_top_level then ((Value (V_lit (L_aux L_unit l)), update_mem l_mem n value, l_env),Nothing) - else ((Value (in_mem l_mem n), l_mem, l_env),Just (fun e -> LEXP_aux (LEXP_cast typc id) (l,annot))) + else ((Value (in_mem l_mem n), l_mem, l_env),Just (fun e env -> (LEXP_aux (LEXP_cast typc id) (l,annot), env))) | V_unknown -> if is_top_level then begin @@ -1902,27 +1951,32 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level ( else ((Error l (String.stringAppend "Undefined id " (get_id id)),l_mem,l_env),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 -> LEXP_aux(LEXP_cast typc id) (l,annot))) + else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_cast typc id) (l,annot), env))) end | Tag_extern _ -> let regf = Reg id annot in let request = (Action (Write_reg regf Nothing 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 -> LEXP_aux (LEXP_cast typc id) (l,annot))) + if is_top_level then (request,Nothing) else (request,Just (fun e env -> (LEXP_aux (LEXP_cast typc id) (l,annot), env))) | _ -> ((Error l (String.stringAppend "Internal error: writing to id with tag other than extern or empty " (get_id id)),l_mem,l_env),Nothing) end | LEXP_vector lexp exp -> match (interp_main mode t_level l_env l_mem exp) with - | (Value i,lm,le) -> + | (Value i_whole,lm,le) -> + let i = match i_whole with | V_track v _ -> v | _ -> i_whole end in (match i with | V_lit (L_aux (L_num n) ln) -> - let next_builder le_builder = (fun e -> - LEXP_aux (LEXP_vector (le_builder e) (E_aux (E_lit (L_aux (L_num n) ln)) (ln,Nothing))) (l,annot)) in + let next_builder le_builder = + (fun e env -> + let (lexp,env) = le_builder e env in + let (ie,env) = to_exp mode env i_whole in + (LEXP_aux (LEXP_vector lexp ie) (l,annot), env)) in (match (create_write_message_or_update mode t_level value l_env lm false lexp) with - | ((Value v,lm,le),maybe_builder) -> + | ((Value v_whole,lm,le),maybe_builder) -> + let v = (match v_whole with | V_track v _ -> v | _ -> v_whole end) in + let nth = (match access_vector v n with | V_track v _ -> v | v -> v end) in (match v with | V_vector inc m vs -> - let nth = access_vector v n in (match (nth,is_top_level,maybe_builder) with | (V_register regform,true,_) -> ((Action (Write_reg regform Nothing value) @@ -1936,7 +1990,6 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level ( | ((V_boxref n t),false, Just lexp_builder) -> ((Value (in_mem lm n),lm, l_env),Just (next_builder lexp_builder)) | (v,false, Just lexp_builder) -> ((Value v,lm,le), Just (next_builder lexp_builder)) end) | V_vector_sparse n m inc vs d -> - let nth = access_vector v n in (match (nth,is_top_level,maybe_builder) with | (V_register regform,true,_) -> ((Action (Write_reg regform Nothing value) @@ -1961,21 +2014,25 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level ( | _ -> ((Action a s,lm,le), Just (next_builder lexp_builder)) end) | e -> e end) | _ -> ((Error l "Vector access must be a number",lm,le),Nothing) end) - | (Action a s,lm,le) -> ((Action a s,lm,le), Just (fun e -> (LEXP_aux (LEXP_vector lexp e) (l,annot)))) + | (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 | LEXP_vector_range lexp exp1 exp2 -> match (interp_main mode t_level l_env l_mem exp1) with - | (Value i1, lm, le) -> + | (Value i1_whole, lm, le) -> + let i1 = match i1_whole with | V_track v _ -> v | _ -> i1_whole end in (match i1 with | V_lit (L_aux (L_num n1) ln1) -> (match (interp_main mode t_level l_env l_mem exp2) with - | (Value i2,lm,le) -> + | (Value i2_whole,lm,le) -> + let i2 = match i2_whole with | V_track v _ -> v | _ -> i2_whole end in (match i2 with | V_lit (L_aux (L_num n2) ln2) -> let next_builder le_builder = - (fun e -> LEXP_aux (LEXP_vector_range (le_builder e) - (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing)) - (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing))) (l,annot)) in + (fun e env -> + let (e1,env) = to_exp mode env i1_whole in + let (e2,env) = to_exp mode env i2_whole in + let (lexp,env) = le_builder e env in + (LEXP_aux (LEXP_vector_range lexp e1 e2) (l,annot), env)) in (match (create_write_message_or_update mode t_level value l_env lm false lexp) with | ((Value v,lm,le), Just lexp_builder) -> (match (v,is_top_level) with @@ -1993,36 +2050,40 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level ( | e -> e end) | _ -> ((Error l "Vector slice requires a number", lm, le),Nothing) end) | (Action a s,lm,le) -> - ((Action a s,lm, le), Just (fun e -> LEXP_aux (LEXP_vector_range lexp - (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing)) - e) (l,annot))) + ((Action a s,lm, le), + Just (fun e env -> + let (e1,env) = to_exp mode env i1_whole 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) | (Action a s,lm,le) -> - ((Action a s, lm,le), Just (fun e -> LEXP_aux (LEXP_vector_range lexp e exp2) (l,annot))) + ((Action a s, lm,le), Just (fun e env -> (LEXP_aux (LEXP_vector_range lexp e exp2) (l,annot), env))) | e -> (e,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) -> + 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 fexps id,is_top_level) with | (Just (V_boxref n t),true) -> ((Value (V_lit (L_aux L_unit l)), update_mem lm n value, l_env),Nothing) - | (Just (V_boxref n t),false) -> - ((Value (in_mem lm n),lm,l_env),Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot))) + | (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),Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot))) + | (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) -> + 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), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot))) - | Read_mem _ _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot))) - | Call_extern _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot))) + | 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) | Write_reg ((Reg _ (Just(T_id id',_,_,_))) as regf) Nothing value -> match in_env subregs (Id_aux (Id id') Unknown) with | Just(indexes) -> match in_env indexes id with | Just ir -> ((Action (Write_reg (SubReg id regf ir) Nothing value) s,lm,le), - (if is_top_level then Nothing else Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))) + (if is_top_level then Nothing else next_builder)) | _ -> ((Error l "Internal error, unrecognized write, no field",lm,le),Nothing) end | Nothing -> ((Error l "Internal error, unrecognized write, no subreges",lm,le),Nothing) end @@ -2032,7 +2093,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level ( match in_env indexes id with | Just ir -> ((Action (Write_reg (SubReg id regf ir) Nothing value) s,lm,le), - (if is_top_level then Nothing else Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))) + (if is_top_level then Nothing else next_builder)) | _ -> ((Error l "Internal error, unrecognized write, no field",lm,le),Nothing) end | Nothing -> ((Error l "Internal error, unrecognized write, no subreges",lm,le),Nothing) end |