fix a bug where enum elim produced unwanted results on booleans

formatting

lustrec_tests/minimal_tests/config.json

 {
-    "initial_timeout": 240,
-    "optimization_level": 1,
+    "initial_timeout": 500,
+    "optimization_level": 3,
     "ignored_file": null
 }

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 = []);

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
 

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 _ _ _ _ = ()

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 =

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.(

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

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

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 *)
   ()
 

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 ->

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

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