diff --git a/lustrec_tests/minimal_tests/config.json b/lustrec_tests/minimal_tests/config.json
index 75d2d8eadea04966a69bcc06d78cb74255c12ea7..3c542839328643eed70d14b768fb738634c547c7 100644
--- a/lustrec_tests/minimal_tests/config.json
+++ b/lustrec_tests/minimal_tests/config.json
@@ -1,5 +1,5 @@
{
- "initial_timeout": 240,
- "optimization_level": 1,
+ "initial_timeout": 500,
+ "optimization_level": 3,
"ignored_file": null
}
diff --git a/src/backends/Ada/ada_backend.ml b/src/backends/Ada/ada_backend.ml
index 5bdf64fdf2b9720d0b2c90d6157299f0019f5554..c155b9b1907b2744d74a7fe7e79cb4897bfa63d4 100644
--- a/src/backends/Ada/ada_backend.ml
+++ b/src/backends/Ada/ada_backend.ml
@@ -93,7 +93,7 @@ let extract_contract machines m =
let machine_spec = find_submachine_from_ident ident machines in
let guarantees =
match machine_spec.mspec.mnode_spec with
- | Some (Contract _ (*contract*) ) ->
+ | Some (Contract _ (*contract*)) ->
(* assert (contract.consts = []);
* assert (contract.locals = []);
* assert (contract.stmts = []);
diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index 731cc8be7a9e2e0dc4dcd582e7f6e939be7ec8fe..a19e01c4a845a7374e030ea43c4a6d329ac17cb2 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -1160,7 +1160,8 @@ module SrcMod = struct
fprintf fmt "%s_step_ghost" Arrow.arrow_id
(* let pp_arrow_reset_ghost mem fmt inst = *)
- (* fprintf fmt "%t(%a)" pp_contract_arrow_reset_name pp_indirect' (mem, inst) *)
+ (* fprintf fmt "%t(%a)" pp_contract_arrow_reset_name pp_indirect' (mem,
+ inst) *)
let pp_is_contract = pp_is_contract
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index 5e0fad4cdc1e3f8ad0516061a09d118f812cbe07..253bc08848f0a0d8c9fd2b8f0bf5b953f1f851a3 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -59,6 +59,7 @@ module EmptyMod = struct
module GhostProto = EmptyGhostProto
let pp_import_spec_prototype _ _ = ()
+
(* let pp_set_reset_spec _ _ _ _ _ = () *)
let pp_clear_reset_spec _ _ _ _ = ()
let pp_ghost_reset_spec _ _ _ _ = ()
diff --git a/src/causality.ml b/src/causality.ml
index a579e096c3973b389bd223d8078c6093925deb1d..a94519cc4c9189e19b73f6f2a613caba34488fe2 100644
--- a/src/causality.ml
+++ b/src/causality.ml
@@ -48,8 +48,7 @@ exception Error of error
to break cycle, then start afresh - insert g' into g - return g *)
(* Tests whether [v] is a root of graph [g], i.e. a source *)
-let is_graph_root v g =
- IdentDepGraph.in_degree g v = 0
+let is_graph_root v g = IdentDepGraph.in_degree g v = 0
(* Computes the set of graph roots, i.e. the sources of acyclic graph [g] *)
let graph_roots g =
diff --git a/src/checks/liveness.ml b/src/checks/liveness.ml
index 99ea71ae18638a9aa75f9684ad17263755225486..d381be596bd38b00ed4b8578ed1a1f271c7a6bc9 100644
--- a/src/checks/liveness.ml
+++ b/src/checks/liveness.ml
@@ -202,7 +202,8 @@ let update_dependencies heads ctx =
of the current heads (which contain [var]) - [v] is not currently in use *)
let eligible node ctx heads var v =
let is_another_head head v =
- head.var_id = v.var_id || try Hashtbl.find ctx.policy head.var_id = v with Not_found -> false
+ head.var_id = v.var_id
+ || try Hashtbl.find ctx.policy head.var_id = v with Not_found -> false
in
Hashtbl.find ctx.policy v.var_id == v
&& Typing.eq_ground
@@ -221,9 +222,9 @@ let compute_reuse node inputs ctx heads var =
let disjoint = Hashtbl.find ctx.disjoint var.var_id in
let locally_reusable v =
let v_id =
- if Disjunction.CISet.mem v inputs
- then ExprDep.mk_read_var v.var_id
- else v.var_id in
+ if Disjunction.CISet.mem v inputs then ExprDep.mk_read_var v.var_id
+ else v.var_id
+ in
IdentDepGraph.fold_pred
(fun p r ->
r && Disjunction.CISet.exists (fun d -> p = d.var_id) disjoint)
@@ -232,16 +233,15 @@ let compute_reuse node inputs ctx heads var =
true
in
let eligibles =
- if ISet.mem var.var_id (ExprDep.node_memory_variables node)
- then
+ if ISet.mem var.var_id (ExprDep.node_memory_variables node) then
Disjunction.CISet.empty
- else
- if ISet.mem var.var_id (ExprDep.node_output_variables node)
- then
- Disjunction.CISet.filter (fun v -> (not (Disjunction.CISet.mem v inputs))
- && eligible node ctx heads var v) ctx.evaluated
- else
- Disjunction.CISet.filter (eligible node ctx heads var) ctx.evaluated
+ else if ISet.mem var.var_id (ExprDep.node_output_variables node) then
+ Disjunction.CISet.filter
+ (fun v ->
+ (not (Disjunction.CISet.mem v inputs))
+ && eligible node ctx heads var v)
+ ctx.evaluated
+ else Disjunction.CISet.filter (eligible node ctx heads var) ctx.evaluated
in
let quasi_dead, live =
Disjunction.CISet.partition locally_reusable eligibles
@@ -249,7 +249,11 @@ let compute_reuse node inputs ctx heads var =
let disjoint_live = Disjunction.CISet.inter disjoint live in
let dead =
Disjunction.CISet.filter
- (fun v -> is_graph_root (if Disjunction.CISet.mem v inputs then ExprDep.mk_read_var v.var_id else v.var_id) ctx.dep_graph)
+ (fun v ->
+ is_graph_root
+ (if Disjunction.CISet.mem v inputs then ExprDep.mk_read_var v.var_id
+ else v.var_id)
+ ctx.dep_graph)
quasi_dead
in
Log.report ~level:7 (fun fmt ->
@@ -289,7 +293,9 @@ let remove_call_return_dependency g =
g
let add_input_dependency inputs g =
- Disjunction.CISet.iter (fun v -> IdentDepGraph.add_vertex g ExprDep.(mk_read_var v.var_id)) inputs
+ Disjunction.CISet.iter
+ (fun v -> IdentDepGraph.add_vertex g ExprDep.(mk_read_var v.var_id))
+ inputs
let compute_reuse_policy node schedule disjoint g =
let inputs =
@@ -297,20 +303,14 @@ let compute_reuse_policy node schedule disjoint g =
(fun inputs v -> Disjunction.CISet.add v inputs)
Disjunction.CISet.empty
(if node.node_iscontract then node.node_inputs @ node.node_outputs
- else node.node_inputs) in
+ else node.node_inputs)
+ in
(*let inputs = Disjunction.CISet.empty in*)
let policy = Hashtbl.create 23 in
Disjunction.CISet.iter (fun v -> Hashtbl.add policy v.var_id v) inputs;
remove_call_return_dependency g;
add_input_dependency inputs g;
- let ctx =
- {
- evaluated = inputs;
- dep_graph = g;
- disjoint;
- policy = policy;
- }
- in
+ let ctx = { evaluated = inputs; dep_graph = g; disjoint; policy } in
List.iter
(fun heads ->
let heads = List.map (fun v -> get_node_var v node) heads in
@@ -343,7 +343,11 @@ let compute_reuse_policy node schedule disjoint g =
"@[<v>@[<v 2>new context:@,%a@]@,COMPUTE_REUSE@,@]"
pp_context
ctx);
- List.iter (fun head -> update_dependencies [head] ctx; compute_reuse node inputs ctx heads head) heads;
+ List.iter
+ (fun head ->
+ update_dependencies [ head ] ctx;
+ compute_reuse node inputs ctx heads head)
+ heads;
(*compute_evaluated heads ctx;*)
Log.report ~level:6 (fun fmt ->
Format.(
diff --git a/src/machine_code_common.ml b/src/machine_code_common.ml
index 790dedb44e45811a1294e6149ef36846d25a0682..0234eab5d8016bdeb07426295e171f4dec42b83c 100644
--- a/src/machine_code_common.ml
+++ b/src/machine_code_common.ml
@@ -533,7 +533,7 @@ let empty_machine =
let new_instance =
let cpt = ref (-1) in
- fun callee _(*tag*) ->
+ fun callee _ (*tag*) ->
let o =
if Stateless.check_node callee then node_name callee
else
diff --git a/src/machine_code_common.mli b/src/machine_code_common.mli
index 920a2f0562518cb53b9cb563db0d02c3bd9a7b30..69468409b2e741d57c25ef18f52f991e982b48ed 100644
--- a/src/machine_code_common.mli
+++ b/src/machine_code_common.mli
@@ -33,7 +33,10 @@ val arrow_machine : machine_t
val new_instance : top_decl -> tag -> ident
val value_of_dimension : machine_t -> Dimension.t -> value_t
val dimension_of_value : value_t -> Dimension.t
-val pp_spec : machine_t -> Format.formatter -> (mc_formula_t * bool) list -> unit
+
+val pp_spec :
+ machine_t -> Format.formatter -> (mc_formula_t * bool) list -> unit
+
val pp_instr : machine_t -> Format.formatter -> instr_t -> unit
val pp_instrs : machine_t -> Format.formatter -> instr_t list -> unit
val pp_machines : Format.formatter -> machine_t list -> unit
diff --git a/src/machine_types.ml b/src/machine_types.ml
index a7dda7d8274dc5140188a58da083ab8e029d606e..0c545d2e4175db5016b01f5ad94863a2de7f7e9d 100644
--- a/src/machine_types.ml
+++ b/src/machine_types.ml
@@ -416,7 +416,7 @@ let register_node vars annots =
[]
annots
-let check_node _(*nd*) _(*vars*) =
+let check_node _ (*nd*) _ (*vars*) =
(* TODO check that all access to vars are valid *)
()
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index 61ec9946b03dfa84af9d2ed9b978a39951a7c6d3..bc7aeadf53f6fc60d8dc600e79fbebab1ef8b8ea 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -852,7 +852,8 @@ let predicate_spec_replace fvar = function
p
let rec instr_spec_replace m fvar t =
- (*Format.eprintf "instr_spec_replace %a@." (fun fmt t -> Machine_code_common.pp_spec m fmt [t, true]) t;*)
+ (*Format.eprintf "instr_spec_replace %a@." (fun fmt t ->
+ Machine_code_common.pp_spec m fmt [t, true]) t;*)
let aux t = instr_spec_replace m fvar t in
match t with
| Equal (e1, e2) ->
@@ -877,7 +878,7 @@ let rec instr_spec_replace m fvar t =
Predicate (predicate_spec_replace fvar p)
| ExistsMem (f, a, b) ->
ExistsMem (f, aux a, aux b)
- | f ->
+ | f ->
f
let rec instr_replace_var m fvar instrs instr =
@@ -917,7 +918,8 @@ and instrs_replace_var m fvar instrs =
List.rev instrs
let rec add_ghost_assign m fvar instr =
- (*Format.eprintf "add_ghost_assign %a @." (Machine_code_common.pp_instr m) instr;*)
+ (*Format.eprintf "add_ghost_assign %a @." (Machine_code_common.pp_instr m)
+ instr;*)
let aux spec i =
let v = fvar i in
if (fvar i).var_id = i.var_id then spec
@@ -939,14 +941,26 @@ let rec add_ghost_assign m fvar instr =
and add_ghost_assigns m fvar = List.map (add_ghost_assign m fvar)
let ghost_vd m =
- let used = List.fold_left (fun set v -> ISet.add v.var_id set) ISet.empty m.mstep.step_inputs in
- let used = List.fold_left (fun set v -> ISet.add v.var_id set) used m.mstep.step_outputs in
- let used = List.fold_left (fun set v -> ISet.add v.var_id set) used m.mstep.step_locals in
+ let used =
+ List.fold_left
+ (fun set v -> ISet.add v.var_id set)
+ ISet.empty
+ m.mstep.step_inputs
+ in
+ let used =
+ List.fold_left
+ (fun set v -> ISet.add v.var_id set)
+ used
+ m.mstep.step_outputs
+ in
+ let used =
+ List.fold_left (fun set v -> ISet.add v.var_id set) used m.mstep.step_locals
+ in
let used = ref used in
- (fun v ->
+ fun v ->
let ghost_name = mk_new_name (fun v -> ISet.mem v !used) ("_" ^ v.var_id) in
used := ISet.add v.var_id !used;
- { v with var_id = ghost_name })
+ { v with var_id = ghost_name }
module IntS = Set.Make (Int)
@@ -1014,16 +1028,19 @@ let add_ghost_assigns_reassigned m ghost_vd_m rasg instrs =
List.fold_left
(fun (n, instrs, fvar) instr ->
let n, instr, fvar = aux n instr fvar in
- (*Format.eprintf "instr_spec_replace %a@." (Machine_code_common.pp_instr m) instr;*)
+ (*Format.eprintf "instr_spec_replace %a@." (Machine_code_common.pp_instr
+ m) instr;*)
let instr_spec =
match instr.instr_desc, instr.instr_spec with
(* special case for early inlined assignment *)
| MComment _, (Predicate (GhostAssign (v, e)), b) :: spec ->
- (Predicate (GhostAssign (v, value_replace_var fvar e)), b) :: List.map (fun (t, b) -> instr_spec_replace m fvar t, b) spec
- | _ , spec ->
- List.map (fun (t, b) -> instr_spec_replace m fvar t, b) spec
+ (Predicate (GhostAssign (v, value_replace_var fvar e)), b)
+ :: List.map (fun (t, b) -> instr_spec_replace m fvar t, b) spec
+ | _, spec ->
+ List.map (fun (t, b) -> instr_spec_replace m fvar t, b) spec
in
- (*Format.eprintf "instr_spec_replace -> %a@." (Machine_code_common.pp_spec m) instr_spec;*)
+ (*Format.eprintf "instr_spec_replace -> %a@."
+ (Machine_code_common.pp_spec m) instr_spec;*)
n, { instr with instr_spec } :: instrs, fvar)
(0, [], fun v -> v)
instrs
@@ -1062,12 +1079,11 @@ let step_replace_var m reuse step =
List.fold_left
(fun res l ->
let l' = fvar l in
- if List.exists (fun o -> o.var_id = l'.var_id) step.step_outputs
- || List.exists (fun i -> i.var_id = l'.var_id) step.step_inputs
- then
- res
- else
- Utils.add_cons l' res)
+ if
+ List.exists (fun o -> o.var_id = l'.var_id) step.step_outputs
+ || List.exists (fun i -> i.var_id = l'.var_id) step.step_inputs
+ then res
+ else Utils.add_cons l' res)
[]
step.step_locals
in
@@ -1079,14 +1095,18 @@ let step_replace_var m reuse step =
* n: instruction index (absolute) *)
match instr.instr_desc with
| MLocalAssign (i, v) ->
- n + 1, if n >= rank_input && silly_asg i v then asg else add_assigned rasg n k i asg
+ ( n + 1,
+ if n >= rank_input && silly_asg i v then asg
+ else add_assigned rasg n k i asg )
| MStep (il, _, _) ->
n + 1, List.fold_right (add_assigned rasg n k) il asg
| MBranch (_, hl) ->
let n, asg =
List.fold_left
(fun (n, asg) (_, il) ->
- let n, asg = List.fold_left (asg_instr rank_input rasg k) (n, asg) il in
+ let n, asg =
+ List.fold_left (asg_instr rank_input rasg k) (n, asg) il
+ in
n, asg)
(n, asg)
hl
@@ -1105,21 +1125,18 @@ let step_replace_var m reuse step =
asg
in
(* SSA *)
- let input_instrs = List.map Machine_code_common.(fun v -> mk_assign v (vdecl_to_val v)) step.step_inputs in
+ let input_instrs =
+ List.map
+ Machine_code_common.(fun v -> mk_assign v (vdecl_to_val v))
+ step.step_inputs
+ in
let nb_inputs = List.length input_instrs in
- let step_instrs = input_instrs @ step.step_instrs in
+ let step_instrs = input_instrs @ step.step_instrs in
let step_instrs = add_ghost_assigns m fvar step_instrs in
(* register the locations of assignments *)
let asg = assigned nb_inputs false VMap.empty step_instrs in
- (* UNUSED
- let pp fmt (ns, k, b) =
- Format.(
- fprintf fmt "[%a]%n:%a"
- (pp_comma_list pp_print_int) (IntS.elements ns)
- k
- pp_print_bool b)
- in
- *)
+ (* UNUSED let pp fmt (ns, k, b) = Format.( fprintf fmt "[%a]%n:%a"
+ (pp_comma_list pp_print_int) (IntS.elements ns) k pp_print_bool b) in *)
(*Format.printf "AVANT %a@." (VMap.pp pp) asg;*)
(* SSA *)
let step_instrs = instrs_replace_var m fvar step_instrs in
@@ -1131,10 +1148,14 @@ let step_replace_var m reuse step =
in
(*Format.printf "APRES %a@." (VMap.pp pp) asg;*)
(* not SSA anymore *)
- (*Format.eprintf "step instrs before ghost reassign@.%a@." (pp_instrs m) step_instrs;*)
- let step_instrs = add_ghost_assigns_reassigned m ghost_vd_m rasg step_instrs in
+ (*Format.eprintf "step instrs before ghost reassign@.%a@." (pp_instrs m)
+ step_instrs;*)
+ let step_instrs =
+ add_ghost_assigns_reassigned m ghost_vd_m rasg step_instrs
+ in
(* not SSA anymore *)
- (*Format.eprintf "step instrs after ghost reassign@.%a@." (pp_instrs m) step_instrs;*)
+ (*Format.eprintf "step instrs after ghost reassign@.%a@." (pp_instrs m)
+ step_instrs;*)
let step_instrs = remove_skips_instrs step_instrs in
{ step with step_checks; step_locals; step_instrs }
@@ -1215,6 +1236,7 @@ let rec instr_constant_assign var instr =
match get_instr_desc instr with
| MLocalAssign (i, { value_desc = Cst (Const_tag _); _ })
| MStateAssign (i, { value_desc = Cst (Const_tag _); _ }) ->
+ (* c <> "true" && c <> "false" && *)
i = var
| MBranch (_, hl) ->
List.for_all (fun (_, b) -> instrs_constant_assign var b) hl
@@ -1230,32 +1252,31 @@ and instrs_constant_assign var instrs =
false
instrs
-let rec instr_reduce m v branches instr1 cont =
+let rec instr_reduce branches instr1 cont =
match get_instr_desc instr1 with
- | MLocalAssign (_, ({ value_desc = Cst (Const_tag c); _ } as t))
- | MStateAssign (_, ({ value_desc = Cst (Const_tag c); _ } as t)) ->
- mkinstr ~instr_spec:(add_ghost_assign_spec v t []) (assign_comment m v t)
- :: instr1
- :: (List.assoc c branches @ cont)
+ | MLocalAssign (_, { value_desc = Cst (Const_tag c); _ })
+ | MStateAssign (_, { value_desc = Cst (Const_tag c); _ }) ->
+ (* mkinstr ~instr_spec:(add_ghost_assign_spec v t []) (assign_comment m v
+ t) *)
+ instr1 :: (try List.assoc c branches @ cont with Not_found -> cont)
| MBranch (g, hl) ->
update_instr_desc
instr1
- (MBranch
- (g, List.map (fun (h, b) -> h, instrs_reduce m v branches b []) hl))
+ (MBranch (g, List.map (fun (h, b) -> h, instrs_reduce branches b []) hl))
:: cont
| _ ->
instr1 :: cont
-and instrs_reduce m v branches instrs cont =
+and instrs_reduce branches instrs cont =
match instrs with
| [] ->
cont
| [ i ] ->
- instr_reduce m v branches i cont
+ instr_reduce branches i cont
| i1 :: i2 :: q ->
- i1 :: instrs_reduce m v branches (i2 :: q) cont
+ i1 :: instrs_reduce branches (i2 :: q) cont
-let rec instrs_fusion m vars instrs =
+let rec instrs_fusion vars instrs =
match instrs with
| [] | [ _ ] ->
vars, instrs
@@ -1265,31 +1286,29 @@ let rec instrs_fusion m vars instrs =
let vars, branches =
List.fold_right
(fun (h, b) (vars, brs) ->
- let vars, instrs = instrs_fusion m vars b in
+ let vars, instrs = instrs_fusion vars b in
vars, (h, instrs) :: brs)
hl
(vars, [])
in
- let vars, q = instrs_fusion m vars q in
+ let vars, q = instrs_fusion vars q in
let instrs =
instr_reduce
- m
- v
branches
{ i1 with instr_spec = i1.instr_spec @ i2.instr_spec }
q
in
ISet.add v.var_id vars, instrs
| _ ->
- let vars, instrs = instrs_fusion m vars (i2 :: q) in
+ let vars, instrs = instrs_fusion vars (i2 :: q) in
vars, i1 :: instrs)
-let step_fusion m vars step =
- let vars, step_instrs = instrs_fusion m vars step.step_instrs in
+let step_fusion vars step =
+ let vars, step_instrs = instrs_fusion vars step.step_instrs in
vars, { step with step_instrs }
let machine_fusion m =
- let vars, mstep = step_fusion m ISet.empty m.mstep in
+ let vars, mstep = step_fusion ISet.empty m.mstep in
vars, { m with mstep }
let machines_fusion prog =
@@ -1349,8 +1368,13 @@ let machine_clean (vars, m) =
List.filter_map
(fun instr ->
match get_instr_desc instr with
- | MLocalAssign (v, _) ->
- if is_used v then Some instr else None
+ | MLocalAssign (v, t) ->
+ if is_used v then Some instr
+ else
+ Some
+ (mkinstr
+ ~instr_spec:(add_ghost_assign_spec v t [])
+ (assign_comment m v t))
| MStep (xs, _, _) when List.for_all is_unused xs ->
None
| MBranch (e, hl) ->
@@ -1463,7 +1487,7 @@ let machines_clean prog =
The function returns both the (possibly updated) prog as well as the
machines *)
-let optimize _(*params*) prog node_schs machine_code =
+let optimize _ (*params*) prog node_schs machine_code =
let machine_code =
if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then (
Log.report ~level:1 (fun fmt ->
diff --git a/src/scheduling.ml b/src/scheduling.ml
index f9081002faa56f132cfc17fc96b1ae96664ca9df..63baa3b38a6e41d0ffbad75dd0dc2cb94f5ab909 100644
--- a/src/scheduling.ml
+++ b/src/scheduling.ml
@@ -396,7 +396,7 @@ let pp_dep_graph fmt node_schs =
report.dep_graph)
node_schs
-let pp_warning_unused _(*fmt*) node_schs =
+let pp_warning_unused _ (*fmt*) node_schs =
IMap.iter
(fun nd report ->
let unused = report.unused_vars in
diff --git a/src/types.ml b/src/types.ml
index 8d4a0877c697e182f2af22b57639861870d54314..5a9d29701f43165ae0043303685e05d88ff8d057 100644
--- a/src/types.ml
+++ b/src/types.ml
@@ -119,7 +119,7 @@ module type S = sig
end
module Basic : BASIC_TYPES = struct
- type t = Tstring | Tint | Treal | Tbool
+ type t = Tstring | Tint | Treal | Tbool
let type_string_builder = Tstring
let type_int_builder = Tint