summaryrefslogtreecommitdiff
path: root/src/rewrites.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/rewrites.ml')
-rw-r--r--src/rewrites.ml80
1 files changed, 45 insertions, 35 deletions
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 424931c3..8c0526fe 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -48,7 +48,7 @@
(* SUCH DAMAGE. *)
(**************************************************************************)
-open Big_int
+module Big_int = Nat_big_num
open Ast
open Ast_util
open Type_check
@@ -102,7 +102,6 @@ let effectful_effs = function
| 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))
@@ -169,7 +168,7 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp =
constants? This will resolve a 'n - 1 sizeof when 'n is in
scope. *)
| Some size when prove env (nc_eq (nsum size (nint 1)) nexp) ->
- let one_exp = infer_exp env (mk_lit_exp (L_num unit_big_int)) in
+ let one_exp = infer_exp env (mk_lit_exp (L_num (Big_int.of_int 1))) in
Some (E_aux (E_app (mk_id "add_range", [var; one_exp]), (gen_loc l, Some (env, atom_typ (nsum size (nint 1)), no_effect))))
| _ ->
begin
@@ -366,6 +365,7 @@ let rewrite_sizeof (Defs defs) =
; e_internal_let = (fun ((lexp,lexp'), (e2,e2'), (e3,e3')) -> (E_internal_let (lexp,e2,e3), E_internal_let (lexp',e2',e3')))
; e_internal_plet = (fun (pat, (e1,e1'), (e2,e2')) -> (E_internal_plet (pat,e1,e2), E_internal_plet (pat,e1',e2')))
; e_internal_return = (fun (e,e') -> (E_internal_return e, E_internal_return e'))
+ ; e_internal_value = (fun v -> (E_internal_value v, E_internal_value v))
; e_aux = (fun ((e,e'),annot) -> (E_aux (e,annot), E_aux (e',annot)))
; lEXP_id = (fun id -> (LEXP_id id, LEXP_id id))
; lEXP_memory = (fun (id,es) -> let (es, es') = List.split es in (LEXP_memory (id,es), LEXP_memory (id,es')))
@@ -643,8 +643,8 @@ let remove_vector_concat_pat pat =
let (start,last_idx) = (match vector_typ_args_of rtyp with
| (Nexp_aux (Nexp_constant start,_), Nexp_aux (Nexp_constant length,_), ord, _) ->
(start, if is_order_inc ord
- then sub_big_int (add_big_int start length) unit_big_int
- else add_big_int (sub_big_int start length) unit_big_int)
+ then Big_int.sub (Big_int.add start length) (Big_int.of_int 1)
+ else Big_int.add (Big_int.sub start length) (Big_int.of_int 1))
| _ ->
raise (Reporting_basic.err_unreachable (fst rannot')
("unname_vector_concat_elements: vector of unspecified length in vector-concat pattern"))) in
@@ -654,8 +654,8 @@ let remove_vector_concat_pat pat =
let (pos',index_j) = match length with
| Nexp_aux (Nexp_constant i,_) ->
if is_order_inc ord
- then (add_big_int pos i, sub_big_int (add_big_int pos i) unit_big_int)
- else (sub_big_int pos i, add_big_int (sub_big_int pos i) unit_big_int)
+ then (Big_int.add pos i, Big_int.sub (Big_int.add pos i) (Big_int.of_int 1))
+ else (Big_int.sub pos i, Big_int.add (Big_int.sub pos i) (Big_int.of_int 1))
| Nexp_aux (_,l) ->
if is_last then (pos,last_idx)
else
@@ -755,8 +755,8 @@ let remove_vector_concat_pat pat =
with vector_concats patterns as direct child-nodes anymore *)
let range a b =
- let rec aux a b = if gt_big_int a b then [] else a :: aux (add_big_int a unit_big_int) b in
- if gt_big_int a b then List.rev (aux b a) else aux a b in
+ let rec aux a b = if Big_int.greater a b then [] else a :: aux (Big_int.add a (Big_int.of_int 1)) b in
+ if Big_int.greater a b then List.rev (aux b a) else aux a b in
let remove_vector_concats =
let p_vector_concat ps =
@@ -770,9 +770,9 @@ let remove_vector_concat_pat pat =
match p, vector_typ_args_of typ with
| P_vector ps,_ -> acc @ ps
| _, (_,Nexp_aux (Nexp_constant length,_),_,_) ->
- acc @ (List.map wild (range zero_big_int (sub_big_int length unit_big_int)))
+ acc @ (List.map wild (range Big_int.zero (Big_int.sub length (Big_int.of_int 1))))
| _, _ ->
- (*if is_last then*) acc @ [wild zero_big_int]
+ (*if is_last then*) acc @ [wild Big_int.zero]
else raise
(Reporting_basic.err_unreachable l
("remove_vector_concats: Non-vector in vector-concat pattern " ^
@@ -942,6 +942,7 @@ let rec pat_to_exp (P_aux (pat,(l,annot))) =
| P_wild -> raise (Reporting_basic.err_unreachable l
"pat_to_exp given wildcard pattern")
| P_as (pat,id) -> rewrap (E_id id)
+ | P_var (pat, _) -> pat_to_exp pat
| P_typ (_,pat) -> pat_to_exp pat
| P_id id -> rewrap (E_id id)
| P_app (id,pats) -> rewrap (E_app (id, List.map pat_to_exp pats))
@@ -1030,7 +1031,7 @@ let bitwise_and_exp exp1 exp2 =
let rec contains_bitvector_pat (P_aux (pat,annot)) = match pat with
| P_lit _ | P_wild | P_id _ -> false
-| P_as (pat,_) | P_typ (_,pat) -> contains_bitvector_pat pat
+| P_as (pat,_) | P_typ (_,pat) | P_var (pat,_) -> contains_bitvector_pat pat
| P_vector _ | P_vector_concat _ ->
let typ = Env.base_typ_of (env_of_annot annot) (typ_of_annot annot) in
is_bitvector_typ typ
@@ -1106,7 +1107,7 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
let subvec_exp =
match start, length with
| Nexp_aux (Nexp_constant s, _), Nexp_aux (Nexp_constant l, _)
- when eq_big_int s i && eq_big_int l (big_int_of_int (List.length lits)) ->
+ when Big_int.equal s i && Big_int.equal l (Big_int.of_int (List.length lits)) ->
mk_exp (E_id rootid)
| _ ->
mk_exp (E_vector_subrange (mk_exp (E_id rootid), mk_num_exp i, mk_num_exp j)) in
@@ -1139,7 +1140,7 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
let collect_guards_decls ps rootid t =
let (start,_,ord,_) = vector_typ_args_of t in
let rec collect current (guards,dls) idx ps =
- let idx' = if is_order_inc ord then add_big_int idx unit_big_int else sub_big_int idx unit_big_int in
+ let idx' = if is_order_inc ord then Big_int.add idx (Big_int.of_int 1) else Big_int.sub idx (Big_int.of_int 1) in
(match ps with
| pat :: ps' ->
(match pat with
@@ -1333,7 +1334,7 @@ let rewrite_fun_guarded_pats rewriters (FD_aux (FD_function (r,t,e,funcls),(l,fd
(pat,guard,exp,annot) in
let cs = rewrite_guarded_clauses l (List.map clause funcls) in
List.map (fun (pat,exp,annot) ->
- FCL_aux (FCL_Funcl(id,construct_pexp (pat,None,exp,(Unknown,None))),annot)) cs
+ FCL_aux (FCL_Funcl(id,construct_pexp (pat,None,exp,(Parse_ast.Unknown,None))),annot)) cs
| _ -> funcls (* TODO is the empty list possible here? *) in
FD_aux (FD_function(r,t,e,funcls),(l,fdannot))
@@ -1547,7 +1548,7 @@ let rewrite_register_ref_writes (Defs defs) =
let dir_b = i1 < i2 in
let dir = (if dir_b then "true" else "false") in
let ord = Ord_aux ((if dir_b then Ord_inc else Ord_dec), Parse_ast.Unknown) in
- let size = if dir_b then succ_big_int (sub_big_int i2 i1) else succ_big_int (sub_big_int i1 i2) in
+ let size = if dir_b then Big_int.succ (Big_int.sub i2 i1) else Big_int.succ (Big_int.sub i1 i2) in
let rtyp = mk_id_typ id in
let vtyp = vector_typ (nconstant i1) (nconstant size) ord bit_typ in
let accessors (fr, fid) =
@@ -1765,6 +1766,7 @@ let rewrite_fix_val_specs (Defs defs) =
let args_t' = rewrite_typ_nexp_ids (env_of exp) (pat_typ_of pat) in
let ret_t' = rewrite_typ_nexp_ids (env_of exp) (typ_of exp) in
(tq, Typ_aux (Typ_fn (args_t', ret_t', eff'), a)), eff'
+ | _ -> assert false (* find_vs must return a function type *)
in
let annot = add_effect_annot annot eff in
(Bindings.add id vs val_specs,
@@ -2016,15 +2018,15 @@ let rewrite_tuple_vector_assignments defs =
let (_, len, _, _) = vector_typ_args_of ltyp in
match nexp_simp len with
| Nexp_aux (Nexp_constant len, _) -> len
- | _ -> unit_big_int
- else unit_big_int in
+ | _ -> (Big_int.of_int 1)
+ else (Big_int.of_int 1) in
let next i step =
if is_order_inc ord
- then (sub_big_int (add_big_int i step) unit_big_int, add_big_int i step)
- else (add_big_int (sub_big_int i step) unit_big_int, sub_big_int i step) in
+ then (Big_int.sub (Big_int.add i step) (Big_int.of_int 1), Big_int.add i step)
+ else (Big_int.add (Big_int.sub i step) (Big_int.of_int 1), Big_int.sub i step) in
let i = match nexp_simp start with
| (Nexp_aux (Nexp_constant i, _)) -> i
- | _ -> if is_order_inc ord then zero_big_int else big_int_of_int (List.length lexps - 1) in
+ | _ -> if is_order_inc ord then Big_int.zero else Big_int.of_int (List.length lexps - 1) in
let l = gen_loc (fst annot) in
let exp' =
if small exp then strip_exp exp
@@ -2288,7 +2290,7 @@ let rewrite_defs_letbind_effects =
let exp3 = n_exp_term newreturn exp3 in
k (rewrap (E_if (exp1,exp2,exp3))))
| E_for (id,start,stop,by,dir,body) ->
- n_exp_name start (fun start ->
+ n_exp_name start (fun start ->
n_exp_name stop (fun stop ->
n_exp_name by (fun by ->
let body = n_exp_term (effectful body) body in
@@ -2305,19 +2307,19 @@ let rewrite_defs_letbind_effects =
n_exp_name exp2 (fun exp2 ->
k (rewrap (E_vector_access (exp1,exp2)))))
| E_vector_subrange (exp1,exp2,exp3) ->
- n_exp_name exp1 (fun exp1 ->
- n_exp_name exp2 (fun exp2 ->
+ n_exp_name exp1 (fun exp1 ->
+ n_exp_name exp2 (fun exp2 ->
n_exp_name exp3 (fun exp3 ->
k (rewrap (E_vector_subrange (exp1,exp2,exp3))))))
| E_vector_update (exp1,exp2,exp3) ->
- n_exp_name exp1 (fun exp1 ->
- n_exp_name exp2 (fun exp2 ->
+ n_exp_name exp1 (fun exp1 ->
+ n_exp_name exp2 (fun exp2 ->
n_exp_name exp3 (fun exp3 ->
k (rewrap (E_vector_update (exp1,exp2,exp3))))))
| E_vector_update_subrange (exp1,exp2,exp3,exp4) ->
- n_exp_name exp1 (fun exp1 ->
- n_exp_name exp2 (fun exp2 ->
- n_exp_name exp3 (fun exp3 ->
+ n_exp_name exp1 (fun exp1 ->
+ n_exp_name exp2 (fun exp2 ->
+ n_exp_name exp3 (fun exp3 ->
n_exp_name exp4 (fun exp4 ->
k (rewrap (E_vector_update_subrange (exp1,exp2,exp3,exp4)))))))
| E_vector_append (exp1,exp2) ->
@@ -2327,14 +2329,14 @@ let rewrite_defs_letbind_effects =
| E_list exps ->
n_exp_nameL exps (fun exps ->
k (rewrap (E_list exps)))
- | E_cons (exp1,exp2) ->
+ | E_cons (exp1,exp2) ->
n_exp_name exp1 (fun exp1 ->
n_exp_name exp2 (fun exp2 ->
k (rewrap (E_cons (exp1,exp2)))))
| E_record fexps ->
n_fexps fexps (fun fexps ->
k (rewrap (E_record fexps)))
- | E_record_update (exp1,fexps) ->
+ | E_record_update (exp1,fexps) ->
n_exp_name exp1 (fun exp1 ->
n_fexps fexps (fun fexps ->
k (rewrap (E_record_update (exp1,fexps)))))
@@ -2343,11 +2345,16 @@ let rewrite_defs_letbind_effects =
k (rewrap (E_field (exp1,id))))
| E_case (exp1,pexps) ->
let newreturn = List.exists effectful_pexp pexps in
- n_exp_name exp1 (fun exp1 ->
+ n_exp_name exp1 (fun exp1 ->
n_pexpL newreturn pexps (fun pexps ->
k (rewrap (E_case (exp1,pexps)))))
+ | E_try (exp1,pexps) ->
+ let newreturn = List.exists effectful_pexp pexps in
+ n_exp_name exp1 (fun exp1 ->
+ n_pexpL newreturn pexps (fun pexps ->
+ k (rewrap (E_try (exp1,pexps)))))
| E_let (lb,body) ->
- n_lb lb (fun lb ->
+ n_lb lb (fun lb ->
rewrap (E_let (lb,n_exp body k)))
| E_sizeof nexp ->
k (rewrap (E_sizeof nexp))
@@ -2360,6 +2367,7 @@ let rewrite_defs_letbind_effects =
n_exp_name exp1 (fun exp1 ->
k (rewrap (E_assign (lexp,exp1)))))
| E_exit exp' -> k (E_aux (E_exit (n_exp_term (effectful exp') exp'),annot))
+ | E_throw exp' -> k (E_aux (E_throw (n_exp_term (effectful exp') exp'),annot))
| E_assert (exp1,exp2) ->
n_exp_name exp1 (fun exp1 ->
n_exp_name exp2 (fun exp2 ->
@@ -2376,11 +2384,13 @@ let rewrite_defs_letbind_effects =
| E_internal_return exp1 ->
n_exp_name exp1 (fun exp1 ->
k (rewrap (E_internal_return exp1)))
+ | E_internal_value v ->
+ k (rewrap (E_internal_value v))
| E_comment str ->
- k (rewrap (E_comment str))
+ k (rewrap (E_comment str))
| E_comment_struc exp' ->
n_exp exp' (fun exp' ->
- k (rewrap (E_comment_struc exp')))
+ k (rewrap (E_comment_struc exp')))
| E_return exp' ->
n_exp_name exp' (fun exp' ->
k (rewrap (E_return exp')))
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 21:49:30 +0000