summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/anf.ml8
-rw-r--r--src/profile.ml2
-rw-r--r--src/rewriter.ml15
-rw-r--r--src/rewrites.ml34
-rw-r--r--src/util.ml11
-rw-r--r--src/util.mli2
6 files changed, 56 insertions, 16 deletions
diff --git a/src/anf.ml b/src/anf.ml
index 915ab738..38c77e0b 100644
--- a/src/anf.ml
+++ b/src/anf.ml
@@ -699,9 +699,13 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) =
(* Interpreter specific *)
raise (Reporting.err_unreachable l __POS__ "encountered E_internal_value when converting to ANF")
- | E_sizeof _ | E_constraint _ ->
+ | E_sizeof nexp ->
(* Sizeof nodes removed by sizeof rewriting pass *)
- raise (Reporting.err_unreachable l __POS__ "encountered E_sizeof or E_constraint node when converting to ANF")
+ raise (Reporting.err_unreachable l __POS__ ("encountered E_sizeof node " ^ string_of_nexp nexp ^ " when converting to ANF"))
+
+ | E_constraint _ ->
+ (* Sizeof nodes removed by sizeof rewriting pass *)
+ raise (Reporting.err_unreachable l __POS__ "encountered E_constraint node when converting to ANF")
| E_nondet _ ->
(* We don't compile E_nondet nodes *)
diff --git a/src/profile.ml b/src/profile.ml
index cb374403..1a8bd30b 100644
--- a/src/profile.ml
+++ b/src/profile.ml
@@ -83,7 +83,7 @@ let finish msg t =
if !opt_profile then
begin match !profile_stack with
| p :: ps ->
- prerr_endline (Printf.sprintf "%s %s: %fs" Util.("Profile" |> magenta |> clear) msg (Sys.time () -. t));
+ prerr_endline (Printf.sprintf "%s %s: %fs" Util.("Profiled" |> magenta |> clear) msg (Sys.time () -. t));
prerr_endline (Printf.sprintf " Z3 calls: %d, Z3 time: %fs" p.z3_calls p.z3_time);
profile_stack := ps
| [] -> ()
diff --git a/src/rewriter.ml b/src/rewriter.ml
index ae19e447..39b437f4 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -336,7 +336,7 @@ let rewrite_lexp rewriters (LEXP_aux(lexp,(l,annot))) =
| LEXP_memory (id,exps) -> rewrap (LEXP_memory(id,List.map (rewriters.rewrite_exp rewriters) exps))
| LEXP_vector (lexp,exp) ->
rewrap (LEXP_vector (rewriters.rewrite_lexp rewriters lexp,rewriters.rewrite_exp rewriters exp))
- | LEXP_vector_range (lexp,exp1,exp2) ->
+ | LEXP_vector_range (lexp,exp1,exp2) ->
rewrap (LEXP_vector_range (rewriters.rewrite_lexp rewriters lexp,
rewriters.rewrite_exp rewriters exp1,
rewriters.rewrite_exp rewriters exp2))
@@ -363,13 +363,18 @@ let rewrite_def rewriters d = match d with
| DEF_internal_mutrec fdefs -> DEF_internal_mutrec (List.map (rewriters.rewrite_fun rewriters) fdefs)
| DEF_val letbind -> DEF_val (rewriters.rewrite_let rewriters letbind)
| DEF_pragma (pragma, arg, l) -> DEF_pragma (pragma, arg, l)
- | DEF_scattered _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "DEF_scattered survived to rewritter")
+ | DEF_scattered _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "DEF_scattered survived to rewriter")
let rewrite_defs_base rewriters (Defs defs) =
- let rec rewrite ds = match ds with
+ let total = List.length defs in
+ let rec rewrite n = function
| [] -> []
- | d::ds -> (rewriters.rewrite_def rewriters d)::(rewrite ds) in
- Defs (rewrite defs)
+ | d :: ds ->
+ if !Profile.opt_profile then Util.progress n total else ();
+ let d = rewriters.rewrite_def rewriters d in
+ d :: rewrite (n + 1) ds
+ in
+ Defs (rewrite 1 defs)
let rewriters_base =
{rewrite_exp = rewrite_exp;
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 7536edf4..88ea5304 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -350,13 +350,24 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp =
let rec split_nexp (Nexp_aux (nexp_aux, l) as nexp) =
match nexp_aux with
| Nexp_sum (n1, n2) ->
- mk_exp (E_app (mk_id "add_atom", [split_nexp n1; split_nexp n2]))
+ mk_exp ~loc:l (E_app (mk_id "add_atom", [split_nexp n1; split_nexp n2]))
| Nexp_minus (n1, n2) ->
- mk_exp (E_app (mk_id "sub_atom", [split_nexp n1; split_nexp n2]))
+ mk_exp ~loc:l (E_app (mk_id "sub_atom", [split_nexp n1; split_nexp n2]))
| Nexp_times (n1, n2) ->
- mk_exp (E_app (mk_id "mult_atom", [split_nexp n1; split_nexp n2]))
- | Nexp_neg nexp -> mk_exp (E_app (mk_id "negate_atom", [split_nexp nexp]))
- | _ -> mk_exp (E_sizeof nexp)
+ mk_exp ~loc:l (E_app (mk_id "mult_atom", [split_nexp n1; split_nexp n2]))
+ | Nexp_neg nexp ->
+ mk_exp ~loc:l (E_app (mk_id "negate_atom", [split_nexp nexp]))
+ | Nexp_app (f, [n1; n2]) when string_of_id f = "div" ->
+ (* We should be more careful about the right division here *)
+ mk_exp ~loc:l (E_app (mk_id "div", [split_nexp n1; split_nexp n2]))
+ | _ ->
+ mk_exp ~loc:l (E_sizeof nexp)
+ in
+ let is_int_typ env v _ = function
+ | (_, Typ_aux (Typ_app (f, [A_aux (A_nexp (Nexp_aux (Nexp_var v', _)), _)]), _))
+ when Kid.compare v v' = 0 && string_of_id f = "atom" ->
+ true
+ | _ -> false
in
let rec rewrite_e_aux split_sizeof (E_aux (e_aux, (l, _)) as orig_exp) =
let env = env_of orig_exp in
@@ -365,9 +376,13 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp =
E_aux (E_lit (L_aux (L_num c, l)), (l, mk_tannot env (atom_typ nexp) no_effect))
| E_sizeof nexp ->
begin
+ let locals = Env.get_locals env in
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, mk_tannot env (atom_typ nexp) no_effect))
+ | Nexp_aux (Nexp_var v, _) when Bindings.exists (is_int_typ env v) locals ->
+ let id = fst (Bindings.choose (Bindings.filter (is_int_typ env v) locals)) in
+ E_aux (E_id id, (l, mk_tannot env (atom_typ nexp) no_effect))
| _ ->
let locals = Env.get_locals env in
let exps = Bindings.bindings locals
@@ -2288,15 +2303,18 @@ let rewrite_constraint =
| NC_set (kid, int :: ints) ->
let kid_eq kid int = nc_eq (nvar kid) (nconstant int) in
unaux_exp (rewrite_nc env (List.fold_left (fun nc int -> nc_or nc (kid_eq kid int)) (kid_eq kid int) ints))
+ | NC_app (f, [A_aux (A_bool nc, _)]) when string_of_id f = "not" ->
+ E_app (mk_id "not_bool", [rewrite_nc env nc])
| NC_app (f, args) ->
unaux_exp (rewrite_nc env (Env.expand_constraint_synonyms env (mk_nc (NC_app (f, args)))))
| NC_var v ->
- Reporting.unreachable l __POS__ "Cannot rewrite this constraint"
+ (* Would be better to translate change E_sizeof to take a kid, then rewrite to E_sizeof *)
+ E_id (id_of_kid v)
in
- let rewrite_e_aux (E_aux (e_aux, _) as exp) =
+ let rewrite_e_aux (E_aux (e_aux, (l, _)) as exp) =
match e_aux with
| E_constraint nc ->
- check_exp (env_of exp) (rewrite_nc (env_of exp) nc) bool_typ
+ locate (fun _ -> gen_loc l) (check_exp (env_of exp) (rewrite_nc (env_of exp) nc) (atom_bool_typ nc))
| _ -> exp
in
diff --git a/src/util.ml b/src/util.ml
index 5e5654d1..f9603f8e 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -465,3 +465,14 @@ let log_line str line msg =
"\n[" ^ (str ^ ":" ^ string_of_int line |> blue |> clear) ^ "] " ^ msg
let header str n = "\n" ^ str ^ "\n" ^ String.make (String.length str - 9 * n) '='
+
+let progress n total =
+ let len = truncate ((float n /. float total) *. 50.0) in
+ let percent = truncate ((float n /. float total) *. 100.0) in
+ let str = "[" ^ String.make len '=' ^ String.make (50 - len) ' ' ^ "] " ^ string_of_int percent ^ "%" in
+ prerr_string str;
+ if n = total then
+ prerr_char '\n'
+ else
+ prerr_string ("\x1B[" ^ string_of_int (String.length str) ^ "D");
+ flush stderr
diff --git a/src/util.mli b/src/util.mli
index fd0242a3..591cf47b 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -263,3 +263,5 @@ val file_encode_string : string -> string
val log_line : string -> int -> string -> string
val header : string -> int -> string
+
+val progress : int -> int -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 21:47:01 +0000