diff options
Diffstat (limited to 'src/rewriter.ml')
| -rw-r--r-- | src/rewriter.ml | 57 |
1 files changed, 47 insertions, 10 deletions
diff --git a/src/rewriter.ml b/src/rewriter.ml index df264d1e..1c02b161 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -130,6 +130,7 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with union_effects (fun_app_effects f env) (union_eff_exps [e1;e2]) | E_if (e1,e2,e3) -> union_eff_exps [e1;e2;e3] | E_for (_,e1,e2,e3,_,e4) -> union_eff_exps [e1;e2;e3;e4] + | E_loop (_,e1,e2) -> union_eff_exps [e1;e2] | E_vector es -> union_eff_exps es | E_vector_access (e1,e2) -> union_eff_exps [e1;e2] | E_vector_subrange (e1,e2,e3) -> union_eff_exps [e1;e2;e3] @@ -383,6 +384,8 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot))) = | E_if (c,t,e) -> rewrap (E_if (rewrite c,rewrite t, rewrite e)) | E_for (id, e1, e2, e3, o, body) -> rewrap (E_for (id, rewrite e1, rewrite e2, rewrite e3, o, rewrite body)) + | E_loop (loop, e1, e2) -> + rewrap (E_loop (loop, rewrite e1, rewrite e2)) | E_vector exps -> rewrap (E_vector (List.map rewrite exps)) | E_vector_access (vec,index) -> rewrap (E_vector_access (rewrite vec,rewrite index)) | E_vector_subrange (vec,i1,i2) -> @@ -682,6 +685,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; e_tuple : 'exp list -> 'exp_aux ; e_if : 'exp * 'exp * 'exp -> 'exp_aux ; e_for : id * 'exp * 'exp * 'exp * Ast.order * 'exp -> 'exp_aux + ; e_loop : loop * 'exp * 'exp -> 'exp_aux ; e_vector : 'exp list -> 'exp_aux ; e_vector_access : 'exp * 'exp -> 'exp_aux ; e_vector_subrange : 'exp * 'exp * 'exp -> 'exp_aux @@ -745,6 +749,8 @@ let rec fold_exp_aux alg = function | E_if (e1,e2,e3) -> alg.e_if (fold_exp alg e1, fold_exp alg e2, fold_exp alg e3) | E_for (id,e1,e2,e3,order,e4) -> alg.e_for (id,fold_exp alg e1, fold_exp alg e2, fold_exp alg e3, order, fold_exp alg e4) + | E_loop (loop_type, e1, e2) -> + alg.e_loop (loop_type, fold_exp alg e1, fold_exp alg e2) | E_vector es -> alg.e_vector (List.map (fold_exp alg) es) | E_vector_access (e1,e2) -> alg.e_vector_access (fold_exp alg e1, fold_exp alg e2) | E_vector_subrange (e1,e2,e3) -> @@ -819,6 +825,7 @@ let id_exp_alg = ; e_tuple = (fun es -> E_tuple es) ; e_if = (fun (e1,e2,e3) -> E_if (e1,e2,e3)) ; e_for = (fun (id,e1,e2,e3,order,e4) -> E_for (id,e1,e2,e3,order,e4)) + ; e_loop = (fun (lt, e1, e2) -> E_loop (lt, e1, e2)) ; e_vector = (fun es -> E_vector es) ; e_vector_access = (fun (e1,e2) -> E_vector_access (e1,e2)) ; e_vector_subrange = (fun (e1,e2,e3) -> E_vector_subrange (e1,e2,e3)) @@ -910,6 +917,8 @@ let compute_exp_alg bot join = ; e_if = (fun ((v1,e1),(v2,e2),(v3,e3)) -> (join_list [v1;v2;v3], E_if (e1,e2,e3))) ; e_for = (fun (id,(v1,e1),(v2,e2),(v3,e3),order,(v4,e4)) -> (join_list [v1;v2;v3;v4], E_for (id,e1,e2,e3,order,e4))) + ; e_loop = (fun (lt, (v1, e1), (v2, e2)) -> + (join_list [v1;v2], E_loop (lt, e1, e2))) ; e_vector = split_join (fun es -> E_vector es) ; e_vector_access = (fun ((v1,e1),(v2,e2)) -> (join v1 v2, E_vector_access (e1,e2))) ; e_vector_subrange = (fun ((v1,e1),(v2,e2),(v3,e3)) -> (join_list [v1;v2;v3], E_vector_subrange (e1,e2,e3))) @@ -1145,6 +1154,7 @@ let rewrite_sizeof (Defs defs) = ; e_tuple = (fun es -> let (es, es') = List.split es in (E_tuple es, E_tuple es')) ; e_if = (fun ((e1,e1'),(e2,e2'),(e3,e3')) -> (E_if (e1,e2,e3), E_if (e1',e2',e3'))) ; e_for = (fun (id,(e1,e1'),(e2,e2'),(e3,e3'),order,(e4,e4')) -> (E_for (id,e1,e2,e3,order,e4), E_for (id,e1',e2',e3',order,e4'))) + ; e_loop = (fun (lt, (e1, e1'), (e2, e2')) -> (E_loop (lt, e1, e2), E_loop (lt, e1', e2'))) ; e_vector = (fun es -> let (es, es') = List.split es in (E_vector es, E_vector es')) ; e_vector_access = (fun ((e1,e1'),(e2,e2')) -> (E_vector_access (e1,e2), E_vector_access (e1',e2'))) ; e_vector_subrange = (fun ((e1,e1'),(e2,e2'),(e3,e3')) -> (E_vector_subrange (e1,e2,e3), E_vector_subrange (e1',e2',e3'))) @@ -1399,10 +1409,10 @@ let remove_vector_concat_pat pat = let index_j = simple_num l j in (* FIXME *) - (* let subv = fix_eff_exp (E_aux (E_vector_subrange (root, index_i, index_j), cannot)) in *) - let (_, _, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of root) (typ_of root)) in + let subv = fix_eff_exp (E_aux (E_vector_subrange (root, index_i, index_j), cannot)) in + (* let (_, _, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of root) (typ_of root)) in let subrange_id = if is_order_inc ord then "bitvector_subrange_inc" else "bitvector_subrange_dec" in - let subv = fix_eff_exp (E_aux (E_app (mk_id subrange_id, [root; index_i; index_j]), cannot)) in + let subv = fix_eff_exp (E_aux (E_app (mk_id subrange_id, [root; index_i; index_j]), cannot)) in *) let id_pat = match typ_opt with @@ -1846,12 +1856,12 @@ let remove_bitvector_pat pat = let access_bit_exp (rootid,rannot) l idx = let root : tannot exp = E_aux (E_id rootid,rannot) in (* FIXME *) - (* E_aux (E_vector_access (root,simple_num l idx), simple_annot l bit_typ) in *) - let env = env_of_annot rannot in + E_aux (E_vector_access (root,simple_num l idx), simple_annot l bit_typ) in + (*let env = env_of_annot rannot in let t = Env.base_typ_of env (typ_of_annot rannot) in let (_, _, ord, _) = vector_typ_args_of t in let access_id = if is_order_inc ord then "bitvector_access_inc" else "bitvector_access_dec" in - E_aux (E_app (mk_id access_id, [root; simple_num l idx]), simple_annot l bit_typ) in + E_aux (E_app (mk_id access_id, [root; simple_num l idx]), simple_annot l bit_typ) in*) let test_bit_exp rootid l t idx exp = let rannot = simple_annot l t in @@ -1877,12 +1887,12 @@ let remove_bitvector_pat pat = (*if vec_start t = i && vec_length t = List.length lits then E_id rootid else*) - (* E_vector_subrange ( + E_vector_subrange ( E_aux (E_id rootid, simple_annot l typ), simple_num l i, - simple_num l j) in *) - let subrange_id = if is_order_inc ord then "bitvector_subrange_inc" else "bitvector_subrange_dec" in - E_app (mk_id subrange_id, [E_aux (E_id rootid, simple_annot l typ); simple_num l i; simple_num l j]) in + simple_num l j) in + (* let subrange_id = if is_order_inc ord then "bitvector_subrange_inc" else "bitvector_subrange_dec" in + E_app (mk_id subrange_id, [E_aux (E_id rootid, simple_annot l typ); simple_num l i; simple_num l j]) in *) E_aux (E_app( Id_aux (Id "eq_vec", Parse_ast.Generated l), [E_aux (subvec_exp, simple_annot l typ'); @@ -2753,6 +2763,10 @@ let rewrite_defs_letbind_effects = n_exp_name by (fun by -> let body = n_exp_term (effectful body) body in k (rewrap (E_for (id,start,stop,by,dir,body)))))) + | E_loop (loop, cond, body) -> + let cond = n_exp_term (effectful cond) cond in + let body = n_exp_term (effectful body) body in + k (rewrap (E_loop (loop,cond,body))) | E_vector exps -> n_exp_nameL exps (fun exps -> k (rewrap (E_vector exps))) @@ -3068,6 +3082,29 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = else P_aux (P_tup [pat; mktup_pat pl vars], simple_annot pl (typ_of v)) in Added_vars (v,pat) + | E_loop(loop,cond,body) -> + let vars = List.map (fun (var,(l,t)) -> E_aux (E_id var,(l,t))) (find_updated_vars body) in + let vartuple = mktup el vars in + (* let cond = rewrite_var_updates (add_vars false cond vartuple) in *) + let body = rewrite_var_updates (add_vars overwrite body vartuple) in + let (E_aux (_,(_,bannot))) = body in + let fname = match effectful cond, effectful body with + | false, false -> "while_PP" + | false, true -> "while_PM" + | true, false -> "while_MP" + | true, true -> "while_MM" in + let funcl = Id_aux (Id fname,Parse_ast.Generated el) in + let is_while = + match loop with + | While -> E_aux (E_lit (mk_lit L_true), simple_annot el bool_typ) + | Until -> E_aux (E_lit (mk_lit L_false), simple_annot el bool_typ) in + let v = E_aux (E_app (funcl,[is_while;cond;body;vartuple]), + (Parse_ast.Generated el, bannot)) in + let pat = + if overwrite then mktup_pat el vars + else P_aux (P_tup [pat; mktup_pat pl vars], + simple_annot pl (typ_of v)) in + Added_vars (v,pat) | E_if (c,e1,e2) -> let vars = List.map (fun (var,(l,t)) -> E_aux (E_id var,(l,t))) (dedup eqidtyp (find_updated_vars e1 @ find_updated_vars e2)) in |