Construct true_exprt, false_exprt exactly once

Should save 300 seconds.

Author: tautschnig

jbmc/src/java_bytecode/java_types.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 #include <util/ieee_float.h>
 #include <util/invariant.h>
+#include <util/singleton_factory.h>
 
 #include "java_types.h"
 #include "java_utils.h"
@@ -37,8 +38,7 @@ signedbv_typet java_int_type()
 
 empty_typet java_void_type()
 {
-  static const auto result = empty_typet();
-  return result;
+  return singleton_factory<empty_typet>();
 }
 
 signedbv_typet java_long_type()

src/analyses/goto_check.cpp

@@ -29,6 +29,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
 #include <util/simplify_expr.h>
+#include <util/singleton_factory.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
 
@@ -1275,7 +1276,7 @@ void goto_checkt::bounds_check(
     }
   }
 
-  exprt type_matches_size=true_exprt();
+  exprt type_matches_size = singleton_factory<true_exprt>();
 
   if(ode.root_object().id()==ID_dereference)
   {
@@ -1615,7 +1616,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
 
 void goto_checkt::check(const exprt &expr)
 {
-  guardt guard{true_exprt{}};
+  guardt guard{singleton_factory<true_exprt>()};
   check_rec(expr, guard, false);
 }
 
@@ -1747,7 +1748,7 @@ void goto_checkt::goto_check(
             "pointer dereference",
             i.source_location,
             pointer,
-            guardt(true_exprt()));
+            guardt(singleton_factory<true_exprt>()));
         }
       }
 
@@ -1785,7 +1786,7 @@ void goto_checkt::goto_check(
           "pointer dereference",
           i.source_location,
           pointer,
-          guardt(true_exprt()));
+          guardt(singleton_factory<true_exprt>()));
       }
 
       // this has no successor
@@ -1863,7 +1864,7 @@ void goto_checkt::goto_check(
           "memory-leak",
           source_location,
           eq,
-          guardt(true_exprt()));
+          guardt(singleton_factory<true_exprt>()));
       }
     }
 

src/goto-programs/goto_program.h

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/invariant.h>
 #include <util/namespace.h>
+#include <util/singleton_factory.h>
 #include <util/source_location.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
@@ -342,7 +343,7 @@ class goto_programt
     {
       type=_type;
       targets.clear();
-      guard=true_exprt();
+      guard = singleton_factory<true_exprt>();
       code.make_nil();
     }
 
@@ -478,7 +479,7 @@ class goto_programt
       : code(static_cast<const codet &>(get_nil_irep())),
         source_location(static_cast<const source_locationt &>(get_nil_irep())),
         type(_type),
-        guard(true_exprt())
+        guard(singleton_factory<true_exprt>())
     {
     }
 
@@ -965,7 +966,7 @@ class goto_programt
     const code_gotot &_code,
     const source_locationt &l = source_locationt::nil())
   {
-    return instructiont(_code, l, INCOMPLETE_GOTO, true_exprt(), {});
+    return instructiont(_code, l, INCOMPLETE_GOTO, singleton_factory<true_exprt>(), {});
   }
 
   static instructiont make_goto(
@@ -976,7 +977,7 @@ class goto_programt
       static_cast<const codet &>(get_nil_irep()),
       l,
       GOTO,
-      true_exprt(),
+      singleton_factory<true_exprt>(),
       {_target});
   }
 

src/goto-symex/goto_symex_state.h

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/invariant.h>
 #include <util/make_unique.h>
 #include <util/sharing_map.h>
+#include <util/singleton_factory.h>
 #include <util/ssa_expr.h>
 #include <util/std_expr.h>
 
@@ -51,7 +52,7 @@ class goto_statet
   // the if branch will be guarded by the condition of the if (and if there
   // is an else branch then instructions on it will be guarded by the negation
   // of the condition of the if).
-  guardt guard{true_exprt{}};
+  guardt guard{singleton_factory<true_exprt>()};
 
   symex_targett::sourcet source;
 
@@ -270,7 +271,7 @@ class goto_symex_statet final : public goto_statet
   struct threadt
   {
     goto_programt::const_targett pc;
-    guardt guard{true_exprt{}};
+    guardt guard{singleton_factory<true_exprt>()};
     call_stackt call_stack;
     std::map<irep_idt, unsigned> function_frame;
     unsigned atomic_section_id = 0;

src/goto-symex/symex_assign.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/cprover_prefix.h>
 #include <util/exception_utils.h>
 #include <util/pointer_offset_size.h>
+#include <util/singleton_factory.h>
 
 #include "goto_symex_state.h"
 
@@ -74,7 +75,7 @@ void goto_symext::symex_assign(
     if(state.source.pc->source_location.get_hide())
       assignment_type=symex_targett::assignment_typet::HIDDEN;
 
-    guardt guard{true_exprt{}}; // NOT the state guard!
+    guardt guard{singleton_factory<true_exprt>()}; // NOT the state guard!
     symex_assign_rec(state, lhs, nil_exprt(), rhs, guard, assignment_type);
   }
 }

src/goto-symex/symex_function_call.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/c_types.h>
 #include <util/exception_utils.h>
 #include <util/invariant.h>
+#include <util/singleton_factory.h>
 
 static void locality(
   const irep_idt &function_identifier,
@@ -145,7 +146,7 @@ void goto_symext::parameter_assignments(
       clean_expr(lhs, state, true);
       clean_expr(rhs, state, false);
 
-      guardt guard{true_exprt{}};
+      guardt guard{singleton_factory<true_exprt>()};
       symex_assign_rec(state, lhs, nil_exprt(), rhs, guard, assignment_type);
     }
 

src/goto-symex/symex_goto.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/expr_util.h>
 #include <util/invariant.h>
 #include <util/pointer_offset_size.h>
+#include <util/singleton_factory.h>
 #include <util/std_expr.h>
 
 #include <util/simplify_expr.h>
@@ -75,7 +76,7 @@ void goto_symext::symex_goto(statet &state)
       // generate assume(false) or a suitable negation if this
       // instruction is a conditional goto
       if(new_guard.is_true())
-        symex_assume(state, false_exprt());
+        symex_assume(state, singleton_factory<false_exprt>());
       else
         symex_assume(state, not_exprt(new_guard));
 
@@ -227,7 +228,7 @@ void goto_symext::symex_goto(statet &state)
   // adjust guards
   if(new_guard.is_true())
   {
-    state.guard = guardt(false_exprt());
+    state.guard = guardt(singleton_factory<false_exprt>());
   }
   else
   {
@@ -251,8 +252,6 @@ void goto_symext::symex_goto(statet &state)
       state.rename(new_lhs, ns, goto_symex_statet::L1);
       state.assignment(new_lhs, new_rhs, ns, true, false);
 
-      guardt guard{true_exprt{}};
-
       log.conditional_output(
         log.debug(),
         [this, &new_lhs](messaget::mstreamt &mstream) {
@@ -262,7 +261,7 @@ void goto_symext::symex_goto(statet &state)
         });
 
       target.assignment(
-        guard.as_expr(),
+        singleton_factory<true_exprt>(),
         new_lhs, new_lhs, guard_symbol_expr,
         new_rhs,
         original_source,
@@ -501,7 +500,7 @@ static void merge_names(
     });
 
   target.assignment(
-    true_exprt(),
+    singleton_factory<true_exprt>(),
     new_lhs,
     new_lhs,
     new_lhs.get_original_expr(),
@@ -551,7 +550,7 @@ void goto_symext::loop_bound_exceeded(
   exprt negated_cond;
 
   if(guard.is_true())
-    negated_cond=false_exprt();
+    negated_cond = singleton_factory<false_exprt>();
   else
     negated_cond=not_exprt(guard);
 

src/util/c_types.cpp

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 #include "std_types.h"
 #include "config.h"
 #include "invariant.h"
+#include "singleton_factory.h"
 
 #include "c_types.h"
 
@@ -252,8 +253,7 @@ reference_typet reference_type(const typet &subtype)
 
 empty_typet void_type()
 {
-  static const auto result = empty_typet();
-  return result;
+  return singleton_factory<empty_typet>();
 }
 
 std::string c_type_as_string(const irep_idt &c_type)

src/util/guard.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include "expr_util.h"
 #include "invariant.h"
 #include "simplify_utils.h"
+#include "singleton_factory.h"
 #include "std_expr.h"
 
 void guardt::guard_expr(exprt &dest) const
@@ -110,7 +111,7 @@ guardt &operator |= (guardt &g1, const guardt &g2)
     exprt tmp(boolean_negate(g2.as_expr()));
 
     if(tmp == g1.as_expr())
-      g1.expr = true_exprt();
+      g1.expr = singleton_factory<true_exprt>();
     else
       g1.expr = or_exprt(g1.as_expr(), g2.as_expr());
 

src/util/simplify_expr_boolean.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include "invariant.h"
 #include "mathematical_expr.h"
 #include "namespace.h"
+#include "singleton_factory.h"
 #include "std_expr.h"
 
 bool simplify_exprt::simplify_boolean(exprt &expr)
@@ -106,12 +107,12 @@ bool simplify_exprt::simplify_boolean(exprt &expr)
 
       if(expr.id()==ID_and && is_false)
       {
-        expr=false_exprt();
+        expr = singleton_factory<false_exprt>();
         return false;
       }
       else if(expr.id()==ID_or && is_true)
       {
-        expr=true_exprt();
+        expr = singleton_factory<true_exprt>();
         return false;
       }
 
@@ -182,12 +183,12 @@ bool simplify_exprt::simplify_not(exprt &expr)
   }
   else if(op.is_false())
   {
-    expr=true_exprt();
+    expr = singleton_factory<true_exprt>();
     return false;
   }
   else if(op.is_true())
   {
-    expr=false_exprt();
+    expr = singleton_factory<false_exprt>();
     return false;
   }
   else if(op.id()==ID_and ||
@@ -263,12 +264,12 @@ bool simplify_exprt::simplify_not_preorder(exprt &expr)
   }
   else if(op.is_false())
   {
-    expr = true_exprt();
+    expr = singleton_factory<true_exprt>();
     return false;
   }
   else if(op.is_true())
   {
-    expr = false_exprt();
+    expr = singleton_factory<false_exprt>();
     return false;
   }
   else if(op.id() == ID_and || op.id() == ID_or)

src/util/singleton_factory.h

@@ -0,0 +1,21 @@
+/*******************************************************************\
+
+Module: Factory to ensure sharing between default-constructible objects
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_SINGLETON_FACTORY_H
+#define CPROVER_UTIL_SINGLETON_FACTORY_H
+
+/// Return a reference to an object of type T constructed just once. This avoids
+/// repeated construction, e.g., of expressions such as \ref true_exprt.
+template<typename T>
+inline const T &singleton_factory()
+{
+  static T object;
+  return object;
+}
+
+#endif // CPROVER_UTIL_SINGLETON_FACTORY_H

src/util/std_expr.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include "mathematical_types.h"
 #include "pointer_offset_size.h"
 #include "simplify_expr.h"
+#include "singleton_factory.h"
 
 bool constant_exprt::value_is_zero_string() const
 {
@@ -27,7 +28,7 @@ bool constant_exprt::value_is_zero_string() const
 exprt disjunction(const exprt::operandst &op)
 {
   if(op.empty())
-    return false_exprt();
+    return singleton_factory<false_exprt>();
   else if(op.size()==1)
     return op.front();
   else
@@ -49,7 +50,7 @@ unsigned int dynamic_object_exprt::get_instance() const
 exprt conjunction(const exprt::operandst &op)
 {
   if(op.empty())
-    return true_exprt();
+    return singleton_factory<true_exprt>();
   else if(op.size()==1)
     return op.front();
   else