diff options
Diffstat (limited to 'src/rewriter.ml')
| -rw-r--r-- | src/rewriter.ml | 53 |
1 files changed, 17 insertions, 36 deletions
diff --git a/src/rewriter.ml b/src/rewriter.ml index 5329b01d..34e4bfd4 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -165,7 +165,7 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with | E_exit e -> union_effects eff (effect_of e) | E_return e -> union_effects eff (effect_of e) | E_sizeof _ | E_sizeof_internal _ | E_constraint _ -> no_effect - | E_assert (c,m) -> union_eff_exps [c; m] + | E_assert (c,m) -> union_effects eff (union_eff_exps [c; m]) | E_comment _ | E_comment_struc _ -> no_effect | E_internal_cast (_,e) -> effect_of e | E_internal_exp _ -> no_effect @@ -1070,7 +1070,7 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp = E_aux (E_lit (L_aux (L_num c, l)), (l, Some (env, atom_typ nexp, no_effect))) | E_sizeof nexp -> begin - match simplify_nexp (rewrite_nexp_ids (env_of orig_exp) nexp) with + match nexp_simp (rewrite_nexp_ids (env_of orig_exp) nexp) with | Nexp_aux (Nexp_constant c, _) -> E_aux (E_lit (L_aux (L_num c, l)), (l, Some (env, atom_typ nexp, no_effect))) | _ -> @@ -1142,7 +1142,7 @@ let rewrite_sizeof (Defs defs) = Id_aux (Id op, Parse_ast.Unknown), E_aux (e_sizeof nmap nexp2, simple_annot l (atom_typ nexp2)) ) in - let (Nexp_aux (nexp, l) as nexp_aux) = simplify_nexp nexp_aux in + let (Nexp_aux (nexp, l) as nexp_aux) = nexp_simp nexp_aux in (match nexp with | Nexp_constant i -> E_lit (L_aux (L_num i, l)) | Nexp_times (nexp1, nexp2) -> binop nexp1 "*" nexp2 @@ -2621,31 +2621,12 @@ let rewrite_overload_cast (Defs defs) = let defs = List.map simple_def defs in Defs (List.filter (fun def -> not (is_overload def)) defs) + let rewrite_undefined mwords = - let rec undefined_of_typ (Typ_aux (typ_aux, _) as typ) = - match typ_aux with - | Typ_id id -> - mk_exp (E_app (prepend_id "undefined_" id, [mk_lit_exp L_unit])) - | Typ_app (_,[start;size;_;_]) when mwords && is_bitvector_typ typ -> - mk_exp (E_app (mk_id "undefined_bitvector", undefined_of_typ_args start @ undefined_of_typ_args size)) - | Typ_app (id, args) -> - mk_exp (E_app (prepend_id "undefined_" id, List.concat (List.map undefined_of_typ_args args))) - | Typ_var kid -> - (* FIXME: bit of a hack, need to add a restriction to how - polymorphic undefined can be in the type checker to - guarantee this always works. *) - mk_exp (E_id (prepend_id "typ_" (id_of_kid kid))) - | Typ_fn _ -> assert false - and undefined_of_typ_args (Typ_arg_aux (typ_arg_aux, _) as typ_arg) = - match typ_arg_aux with - | Typ_arg_nexp n -> [mk_exp (E_sizeof n)] - | Typ_arg_typ typ -> [undefined_of_typ typ] - | Typ_arg_order _ -> [] - in let rewrite_e_aux (E_aux (e_aux, _) as exp) = match e_aux with | E_lit (L_aux (L_undef, l)) -> - check_exp (env_of exp) (undefined_of_typ (Env.expand_synonyms (env_of exp) (typ_of exp))) (typ_of exp) + check_exp (env_of exp) (undefined_of_typ mwords l (fun _ -> ()) (Env.expand_synonyms (env_of exp) (typ_of exp))) (typ_of exp) | _ -> exp in let rewrite_exp_undefined = { id_exp_alg with e_aux = (fun (exp, annot) -> rewrite_e_aux (E_aux (exp, annot))) } in @@ -2735,7 +2716,7 @@ let rewrite_tuple_vector_assignments defs = let ltyp = Env.base_typ_of env (typ_of_annot lannot) in if is_vector_typ ltyp then let (_, len, _, _) = vector_typ_args_of ltyp in - match simplify_nexp len with + match nexp_simp len with | Nexp_aux (Nexp_constant len, _) -> len | _ -> 1 else 1 in @@ -2743,7 +2724,7 @@ let rewrite_tuple_vector_assignments defs = if is_order_inc ord then (i + step - 1, i + step) else (i - step + 1, i - step) in - let i = match simplify_nexp start with + let i = match nexp_simp start with | (Nexp_aux (Nexp_constant i, _)) -> i | _ -> if is_order_inc ord then 0 else List.length lexps - 1 in let l = gen_loc (fst annot) in @@ -3339,17 +3320,17 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = (* 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 fname = match loop, effectful cond, effectful body with + | While, false, false -> "while_PP" + | While, false, true -> "while_PM" + | While, true, false -> "while_MP" + | While, true, true -> "while_MM" + | Until, false, false -> "until_PP" + | Until, false, true -> "until_PM" + | Until, true, false -> "until_MP" + | Until, true, true -> "until_MM" in let funcl = Id_aux (Id fname,gen_loc el) in - let is_while = - match loop with - | While -> annot_exp (E_lit (mk_lit L_true)) (gen_loc el) env bool_typ - | Until -> annot_exp (E_lit (mk_lit L_false)) (gen_loc el) env bool_typ in - let v = E_aux (E_app (funcl,[is_while;cond;body;vartuple]), (gen_loc el, bannot)) in + let v = E_aux (E_app (funcl,[cond;body;vartuple]), (gen_loc el, bannot)) in let pat = if overwrite then mktup_pat el vars else annot_pat (P_tup [pat; mktup_pat pl vars]) pl env (typ_of v) in |