Merge pull request #3371 from romainbrenguier/refactor/symex-part1

Refactor in symex

Author: romainbrenguier

src/cbmc/symex_bmc.cpp

@@ -105,7 +105,7 @@ void symex_bmct::merge_goto(
     symex_coverage.covered(prev_pc, state.source.pc);
 }
 
-bool symex_bmct::get_unwind(
+bool symex_bmct::should_stop_unwind(
   const symex_targett::sourcet &source,
   const goto_symex_statet::call_stackt &context,
   unsigned unwind)

src/cbmc/symex_bmc.h

@@ -92,29 +92,23 @@ class symex_bmct: public goto_symext
   /// recursive call
   std::vector<recursion_unwind_handlert> recursion_unwind_handlers;
 
-  //
-  // overloaded from goto_symext
-  //
-  virtual void symex_step(
-    const get_goto_functiont &get_goto_function,
-    statet &state);
-
-  virtual void merge_goto(
-    const statet::goto_statet &goto_state,
-    statet &state);
-
-  // for loop unwinding
-  virtual bool get_unwind(
+  void symex_step(const get_goto_functiont &get_goto_function, statet &state)
+    override;
+
+  void
+  merge_goto(const statet::goto_statet &goto_state, statet &state) override;
+
+  bool should_stop_unwind(
     const symex_targett::sourcet &source,
     const goto_symex_statet::call_stackt &context,
-    unsigned unwind);
+    unsigned unwind) override;
 
-  virtual bool get_unwind_recursion(
+  bool get_unwind_recursion(
     const irep_idt &identifier,
     const unsigned thread_nr,
-    unsigned unwind);
+    unsigned unwind) override;
 
-  virtual void no_body(const irep_idt &identifier);
+  void no_body(const irep_idt &identifier) override;
 
   std::unordered_set<irep_idt> body_warnings;
 

src/goto-symex/goto_symex.h

@@ -80,24 +80,12 @@ class goto_symext
   {
   }
 
-  virtual ~goto_symext()
-  {
-  }
+  virtual ~goto_symext() = default;
 
   typedef
     std::function<const goto_functionst::goto_functiont &(const irep_idt &)>
     get_goto_functiont;
 
-  /// \brief symex entire program starting from entry point
-  ///
-  /// The state that goto_symext maintains has a large memory footprint.
-  /// This method deallocates the state as soon as symbolic execution
-  /// has completed, so use it if you don't care about having the state
-  /// around afterwards.
-  virtual void symex_from_entry_point_of(
-    const goto_functionst &goto_functions,
-    symbol_tablet &new_symbol_table);
-
   /// \brief symex entire program starting from entry point
   ///
   /// The state that goto_symext maintains has a large memory footprint.
@@ -115,7 +103,7 @@ class goto_symext
   virtual void resume_symex_from_saved_state(
     const get_goto_functiont &get_goto_function,
     const statet &saved_state,
-    symex_target_equationt *const saved_equation,
+    symex_target_equationt *saved_equation,
     symbol_tablet &new_symbol_table);
 
   //// \brief symex entire program starting from entry point
@@ -142,38 +130,6 @@ class goto_symext
     const get_goto_functiont &,
     symbol_tablet &);
 
-  /// Symexes from the first instruction and the given state, terminating as
-  /// soon as the last instruction is reached.  This is useful to explicitly
-  /// symex certain ranges of a program, e.g. in an incremental decision
-  /// procedure.
-  /// \param state Symex state to start with.
-  /// \param goto_functions GOTO model to symex.
-  /// \param function_identifier The function with the instruction range
-  /// \param first Entry point in form of a first instruction.
-  /// \param limit Final instruction, which itself will not be symexed.
-  virtual void symex_instruction_range(
-    statet &,
-    const goto_functionst &,
-    const irep_idt &function_identifier,
-    goto_programt::const_targett first,
-    goto_programt::const_targett limit);
-
-  /// Symexes from the first instruction and the given state, terminating as
-  /// soon as the last instruction is reached.  This is useful to explicitly
-  /// symex certain ranges of a program, e.g. in an incremental decision
-  /// procedure.
-  /// \param state Symex state to start with.
-  /// \param get_goto_function retrieves a function body
-  /// \param function_identifier The function with the instruction range
-  /// \param first Entry point in form of a first instruction.
-  /// \param limit Final instruction, which itself will not be symexed.
-  virtual void symex_instruction_range(
-    statet &state,
-    const get_goto_functiont &get_goto_function,
-    const irep_idt &function_identifier,
-    goto_programt::const_targett first,
-    goto_programt::const_targett limit);
-
   /// \brief Have states been pushed onto the workqueue?
   ///
   /// If this flag is set at the end of a symbolic execution run, it means that
@@ -215,8 +171,6 @@ class goto_symext
   const bool allow_pointer_unsoundness;
 
 public:
-  // these bypass the target maps
-  virtual void symex_step_goto(statet &, bool taken);
 
   /// language_mode: ID_java, ID_C or another language identifier
   /// if we know the source language in use, irep_idt() otherwise.
@@ -263,13 +217,9 @@ class goto_symext
   void initialize_auto_object(const exprt &, statet &);
   void process_array_expr(exprt &);
   exprt make_auto_object(const typet &, statet &);
-  virtual void dereference(exprt &, statet &, const bool write);
+  virtual void dereference(exprt &, statet &, bool write);
 
-  void dereference_rec(
-    exprt &,
-    statet &,
-    guardt &,
-    const bool write);
+  void dereference_rec(exprt &, statet &, guardt &, bool write);
 
   void dereference_rec_address_of(
     exprt &,
@@ -292,13 +242,13 @@ class goto_symext
   virtual void symex_transition(
     statet &,
     goto_programt::const_targett to,
-    bool is_backwards_goto=false);
+    bool is_backwards_goto);
 
   virtual void symex_transition(statet &state)
   {
     goto_programt::const_targett next=state.source.pc;
     ++next;
-    symex_transition(state, next);
+    symex_transition(state, next, false);
   }
 
   virtual void symex_goto(statet &);
@@ -334,7 +284,7 @@ class goto_symext
 
   // determine whether to unwind a loop -- true indicates abort,
   // with false we continue.
-  virtual bool get_unwind(
+  virtual bool should_stop_unwind(
     const symex_targett::sourcet &source,
     const goto_symex_statet::call_stackt &context,
     unsigned unwind);
@@ -369,24 +319,20 @@ class goto_symext
 
   virtual bool get_unwind_recursion(
     const irep_idt &identifier,
-    const unsigned thread_nr,
+    unsigned thread_nr,
     unsigned unwind);
 
   void parameter_assignments(
-    const irep_idt function_identifier,
+    const irep_idt &function_identifier,
     const goto_functionst::goto_functiont &,
     statet &,
     const exprt::operandst &arguments);
 
   void locality(
-    const irep_idt function_identifier,
+    const irep_idt &function_identifier,
     statet &,
     const goto_functionst::goto_functiont &);
 
-  void add_end_of_function(
-    exprt &code,
-    const irep_idt &identifier);
-
   nondet_symbol_exprt build_symex_nondet(typet &type);
 
   // exceptions
@@ -471,7 +417,6 @@ class goto_symext
   static unsigned nondet_count;
   static unsigned dynamic_counter;
 
-  void read(exprt &);
   void replace_nondet(exprt &);
   void rewrite_quantifiers(exprt &, statet &);
 

src/goto-symex/symex_builtin_functions.cpp

@@ -177,8 +177,8 @@ void goto_symext::symex_allocate(
   }
   else
   {
-    exprt nondet = build_symex_nondet(object_type);
-    code_assignt assignment(value_symbol.symbol_expr(), nondet);
+    const exprt nondet = build_symex_nondet(object_type);
+    const code_assignt assignment(value_symbol.symbol_expr(), nondet);
     symex_assign(state, assignment);
   }
 

src/goto-symex/symex_dereference_state.h

@@ -32,13 +32,10 @@ class symex_dereference_statet:
   goto_symext &goto_symex;
   goto_symext::statet &state;
 
-  virtual void get_value_set(
-    const exprt &expr,
-    value_setst::valuest &value_set);
+  void
+  get_value_set(const exprt &expr, value_setst::valuest &value_set) override;
 
-  virtual bool has_failed_symbol(
-    const exprt &expr,
-    const symbolt *&symbol);
+  bool has_failed_symbol(const exprt &expr, const symbolt *&symbol) override;
 };
 
 #endif // CPROVER_GOTO_SYMEX_SYMEX_DEREFERENCE_STATE_H

src/goto-symex/symex_function_call.cpp

@@ -27,7 +27,7 @@ bool goto_symext::get_unwind_recursion(
 }
 
 void goto_symext::parameter_assignments(
-  const irep_idt function_identifier,
+  const irep_idt &function_identifier,
   const goto_functionst::goto_functiont &goto_function,
   statet &state,
   const exprt::operandst &arguments)
@@ -311,7 +311,7 @@ void goto_symext::symex_function_call_code(
 
   state.source.is_set=true;
   state.source.function = identifier;
-  symex_transition(state, goto_function.body.instructions.begin());
+  symex_transition(state, goto_function.body.instructions.begin(), false);
 }
 
 /// pop one call frame
@@ -323,7 +323,7 @@ void goto_symext::pop_frame(statet &state)
     statet::framet &frame=state.top();
 
     // restore program counter
-    symex_transition(state, frame.calling_location.pc);
+    symex_transition(state, frame.calling_location.pc, false);
     state.source.function = frame.calling_location.function;
 
     // restore L1 renaming
@@ -368,7 +368,7 @@ void goto_symext::symex_end_of_function(statet &state)
 /// preserves locality of local variables of a given function by applying L1
 /// renaming to the local identifiers
 void goto_symext::locality(
-  const irep_idt function_identifier,
+  const irep_idt &function_identifier,
   statet &state,
   const goto_functionst::goto_functiont &goto_function)
 {