diff options
Diffstat (limited to 'src/rewriter.ml')
| -rw-r--r-- | src/rewriter.ml | 49 |
1 files changed, 23 insertions, 26 deletions
diff --git a/src/rewriter.ml b/src/rewriter.ml index 31bcb577..9e9409ec 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -48,7 +48,7 @@ (* SUCH DAMAGE. *) (**************************************************************************) -open Big_int +module Big_int = Nat_big_num open Ast open Ast_util open Type_check @@ -107,7 +107,7 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with let effsum = match e with | E_block es -> union_eff_exps es | E_nondet es -> union_eff_exps es - | E_id _ + | E_id _ | E_ref _ | E_lit _ -> eff | E_cast (_,e) -> effect_of e | E_app (f,es) -> @@ -141,11 +141,12 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with | E_internal_cast (_,e) -> effect_of e | E_internal_exp _ -> no_effect | E_internal_exp_user _ -> no_effect - | E_internal_let (lexp,e1,e2) -> + | E_var (lexp,e1,e2) -> union_effects (effect_of_lexp lexp) (union_effects (effect_of e1) (effect_of e2)) | E_internal_plet (_,e1,e2) -> union_effects (effect_of e1) (effect_of e2) | E_internal_return e1 -> effect_of e1 + | E_internal_value v -> no_effect in E_aux (e, (l, Some (env, typ, effsum))) | None -> @@ -156,6 +157,7 @@ let fix_eff_lexp (LEXP_aux (lexp,((l,_) as annot))) = match snd annot with let effsum = union_effects eff (match lexp with | LEXP_id _ -> no_effect | LEXP_cast _ -> no_effect + | LEXP_deref e -> effect_of e | LEXP_memory (_,es) -> union_eff_exps es | LEXP_tup les -> List.fold_left (fun eff le -> union_effects eff (effect_of_lexp le)) no_effect les @@ -204,24 +206,6 @@ let fix_eff_lb (LB_aux (lb,((l,_) as annot))) = match snd annot with | None -> LB_aux (lb, (l, None)) -let effectful_effs = function - | Effect_aux (Effect_set effs, _) -> - List.exists - (fun (BE_aux (be,_)) -> - match be with - | BE_nondet | BE_unspec | BE_undef | BE_lset -> false - | _ -> true - ) effs - | _ -> true - -let effectful eaux = effectful_effs (effect_of (propagate_exp_effect eaux)) -let effectful_pexp pexp = effectful_effs (snd (propagate_pexp_effect pexp)) - -(* let id_to_string (Id_aux(id,l)) = - match id with - | Id(s) -> s - | DeIid(s) -> s *) - let explode s = let rec exp i l = if i < 0 then l else exp (i - 1) (s.[i] :: l) in exp (String.length s - 1) [] @@ -338,8 +322,8 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot)) as orig_exp) = | E_assert(e1,e2) -> rewrap (E_assert(rewrite e1,rewrite e2)) | E_internal_cast (casted_annot,exp) -> rewrap (E_internal_cast (casted_annot, rewrite exp)) - | E_internal_let (lexp, e1, e2) -> - rewrap (E_internal_let (rewriters.rewrite_lexp rewriters lexp, rewriters.rewrite_exp rewriters e1, rewriters.rewrite_exp rewriters e2)) + | E_var (lexp, e1, e2) -> + rewrap (E_var (rewriters.rewrite_lexp rewriters lexp, rewriters.rewrite_exp rewriters e1, rewriters.rewrite_exp rewriters e2)) | E_internal_return _ -> raise (Reporting_basic.err_unreachable l "Internal return found before it should have been introduced") | E_internal_plet _ -> raise (Reporting_basic.err_unreachable l " Internal plet found before it should have been introduced") | _ -> rewrap exp @@ -355,6 +339,7 @@ let rewrite_lexp rewriters (LEXP_aux(lexp,(l,annot))) = let rewrap le = LEXP_aux(le,(l,annot)) in match lexp with | LEXP_id _ | LEXP_cast _ -> rewrap lexp + | LEXP_deref exp -> rewrap (LEXP_deref (rewriters.rewrite_exp rewriters exp)) | LEXP_tup tupls -> rewrap (LEXP_tup (List.map (rewriters.rewrite_lexp rewriters) tupls)) | LEXP_memory (id,exps) -> rewrap (LEXP_memory(id,List.map (rewriters.rewrite_exp rewriters) exps)) | LEXP_vector (lexp,exp) -> @@ -488,6 +473,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, { e_block : 'exp list -> 'exp_aux ; e_nondet : 'exp list -> 'exp_aux ; e_id : id -> 'exp_aux + ; e_ref : id -> 'exp_aux ; e_lit : lit -> 'exp_aux ; e_cast : Ast.typ * 'exp -> 'exp_aux ; e_app : id * 'exp list -> 'exp_aux @@ -525,8 +511,10 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; e_internal_let : 'lexp * 'exp * 'exp -> 'exp_aux ; e_internal_plet : 'pat * 'exp * 'exp -> 'exp_aux ; e_internal_return : 'exp -> 'exp_aux + ; e_internal_value : Value.value -> 'exp_aux ; e_aux : 'exp_aux * 'a annot -> 'exp ; lEXP_id : id -> 'lexp_aux + ; lEXP_deref : 'exp -> 'lexp_aux ; lEXP_memory : id * 'exp list -> 'lexp_aux ; lEXP_cast : Ast.typ * id -> 'lexp_aux ; lEXP_tup : 'lexp list -> 'lexp_aux @@ -553,6 +541,7 @@ let rec fold_exp_aux alg = function | E_block es -> alg.e_block (List.map (fold_exp alg) es) | E_nondet es -> alg.e_nondet (List.map (fold_exp alg) es) | E_id id -> alg.e_id id + | E_ref id -> alg.e_ref id | E_lit lit -> alg.e_lit lit | E_cast (typ,e) -> alg.e_cast (typ, fold_exp alg e) | E_app (id,es) -> alg.e_app (id, List.map (fold_exp alg) es) @@ -594,14 +583,16 @@ let rec fold_exp_aux alg = function | E_internal_exp_user (annot1,annot2) -> alg.e_internal_exp_user (annot1,annot2) | E_comment c -> alg.e_comment c | E_comment_struc e -> alg.e_comment_struc (fold_exp alg e) - | E_internal_let (lexp,e1,e2) -> + | E_var (lexp,e1,e2) -> alg.e_internal_let (fold_lexp alg lexp, fold_exp alg e1, fold_exp alg e2) | E_internal_plet (pat,e1,e2) -> alg.e_internal_plet (fold_pat alg.pat_alg pat, fold_exp alg e1, fold_exp alg e2) | E_internal_return e -> alg.e_internal_return (fold_exp alg e) + | E_internal_value v -> alg.e_internal_value v and fold_exp alg (E_aux (exp_aux,annot)) = alg.e_aux (fold_exp_aux alg exp_aux, annot) and fold_lexp_aux alg = function | LEXP_id id -> alg.lEXP_id id + | LEXP_deref exp -> alg.lEXP_deref (fold_exp alg exp) | LEXP_memory (id,es) -> alg.lEXP_memory (id, List.map (fold_exp alg) es) | LEXP_tup les -> alg.lEXP_tup (List.map (fold_lexp alg) les) | LEXP_cast (typ,id) -> alg.lEXP_cast (typ,id) @@ -632,6 +623,7 @@ let id_exp_alg = { e_block = (fun es -> E_block es) ; e_nondet = (fun es -> E_nondet es) ; e_id = (fun id -> E_id id) + ; e_ref = (fun id -> E_ref id) ; e_lit = (fun lit -> (E_lit lit)) ; e_cast = (fun (typ,e) -> E_cast (typ,e)) ; e_app = (fun (id,es) -> E_app (id,es)) @@ -666,11 +658,13 @@ let id_exp_alg = ; e_internal_exp_user = (fun (a1,a2) -> E_internal_exp_user (a1,a2)) ; e_comment = (fun c -> E_comment c) ; e_comment_struc = (fun e -> E_comment_struc e) - ; e_internal_let = (fun (lexp, e2, e3) -> E_internal_let (lexp,e2,e3)) + ; e_internal_let = (fun (lexp, e2, e3) -> E_var (lexp,e2,e3)) ; e_internal_plet = (fun (pat, e1, e2) -> E_internal_plet (pat,e1,e2)) ; e_internal_return = (fun e -> E_internal_return e) + ; e_internal_value = (fun v -> E_internal_value v) ; e_aux = (fun (e,annot) -> E_aux (e,annot)) ; lEXP_id = (fun id -> LEXP_id id) + ; lEXP_deref = (fun e -> LEXP_deref e) ; lEXP_memory = (fun (id,es) -> LEXP_memory (id,es)) ; lEXP_cast = (fun (typ,id) -> LEXP_cast (typ,id)) ; lEXP_tup = (fun tups -> LEXP_tup tups) @@ -725,6 +719,7 @@ let compute_exp_alg bot join = { e_block = split_join (fun es -> E_block es) ; e_nondet = split_join (fun es -> E_nondet es) ; e_id = (fun id -> (bot, E_id id)) + ; e_ref = (fun id -> (bot, E_ref id)) ; e_lit = (fun lit -> (bot, E_lit lit)) ; e_cast = (fun (typ,(v,e)) -> (v, E_cast (typ,e))) ; e_app = (fun (id,es) -> split_join (fun es -> E_app (id,es)) es) @@ -766,12 +761,14 @@ let compute_exp_alg bot join = ; e_comment = (fun c -> (bot, E_comment c)) ; e_comment_struc = (fun (v,e) -> (bot, E_comment_struc e)) (* ignore value by default, since it is comes from a comment *) ; e_internal_let = (fun ((vl, lexp), (v2,e2), (v3,e3)) -> - (join_list [vl;v2;v3], E_internal_let (lexp,e2,e3))) + (join_list [vl;v2;v3], E_var (lexp,e2,e3))) ; e_internal_plet = (fun ((vp,pat), (v1,e1), (v2,e2)) -> (join_list [vp;v1;v2], E_internal_plet (pat,e1,e2))) ; e_internal_return = (fun (v,e) -> (v, E_internal_return e)) + ; e_internal_value = (fun v -> (bot, E_internal_value v)) ; e_aux = (fun ((v,e),annot) -> (v, E_aux (e,annot))) ; lEXP_id = (fun id -> (bot, LEXP_id id)) + ; lEXP_deref = (fun (v, e) -> (v, LEXP_deref e)) ; lEXP_memory = (fun (id,es) -> split_join (fun es -> LEXP_memory (id,es)) es) ; lEXP_cast = (fun (typ,id) -> (bot, LEXP_cast (typ,id))) ; lEXP_tup = (fun ls -> |