From 2aad3d8ef2e86a2bc277d63c5296deb3e5d5ec4c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 22 Aug 2024 14:56:23 +0000 Subject: [PATCH] Cleanup `symex_target_equationt` API Remove methods that were never used (and one that wasn't even implemented), mark `protected` what doesn't need to be part of the public API, and remove an unnecessary case of a default parameter. --- src/goto-symex/symex_target_equation.cpp | 2 +- src/goto-symex/symex_target_equation.h | 100 ++++++++++------------- 2 files changed, 42 insertions(+), 60 deletions(-) diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 0bb35155e01..b785acc6b07 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -349,7 +349,7 @@ void symex_target_equationt::convert(decision_proceduret &decision_procedure) const auto convert_SSA_start = std::chrono::steady_clock::now(); convert_without_assertions(decision_procedure); - convert_assertions(decision_procedure); + convert_assertions(decision_procedure, true); const auto convert_SSA_stop = std::chrono::steady_clock::now(); std::chrono::duration convert_SSA_runtime = diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h index b10a922b113..8d1ab192f7a 100644 --- a/src/goto-symex/symex_target_equation.h +++ b/src/goto-symex/symex_target_equation.h @@ -183,53 +183,16 @@ class symex_target_equationt:public symex_targett /// interface void convert_without_assertions(decision_proceduret &decision_procedure); - /// Converts assignments: set the equality _lhs==rhs_ to _True_. - /// \param decision_procedure: A handle to a decision procedure - /// interface - void convert_assignments(decision_proceduret &decision_procedure); - - /// Converts declarations: these are effectively ignored by the decision - /// procedure. - /// \param decision_procedure: A handle to a decision procedure - /// interface - void convert_decls(decision_proceduret &decision_procedure); - - /// Converts assumptions: convert the expression the assumption represents. - /// \param decision_procedure: A handle to a decision procedure interface - void convert_assumptions(decision_proceduret &decision_procedure); - /// Converts assertions: build a disjunction of negated assertions. /// \param decision_procedure: A handle to a decision procedure interface /// \param optimized_for_single_assertions: Use an optimized encoding for /// single assertions (unsound for incremental conversions) void convert_assertions( decision_proceduret &decision_procedure, - bool optimized_for_single_assertions = true); - - /// Converts constraints: set the represented condition to _True_. - /// \param decision_procedure: A handle to a decision procedure interface - void convert_constraints(decision_proceduret &decision_procedure); - - /// Converts goto instructions: convert the expression representing the - /// condition of this goto. - /// \param decision_procedure: A handle to a decision procedure interface - void convert_goto_instructions(decision_proceduret &decision_procedure); - - /// Converts guards: convert the expression the guard represents. - /// \param decision_procedure: A handle to a decision procedure interface - void convert_guards(decision_proceduret &decision_procedure); - - /// Converts function calls: for each argument build an equality between its - /// symbol and the argument itself. - /// \param decision_procedure: A handle to a decision procedure interface - void convert_function_calls(decision_proceduret &decision_procedure); + bool optimized_for_single_assertions); - /// Converts I/O: for each argument build an equality between its - /// symbol and the argument itself. - /// \param decision_procedure: A handle to a decision procedure interface - void convert_io(decision_proceduret &decision_procedure); - - exprt make_expression() const; + typedef std::list SSA_stepst; + SSA_stepst SSA_steps; std::size_t count_assertions() const { @@ -247,27 +210,8 @@ class symex_target_equationt:public symex_targett })); } - typedef std::list SSA_stepst; - SSA_stepst SSA_steps; - - SSA_stepst::iterator get_SSA_step(std::size_t s) - { - SSA_stepst::iterator it=SSA_steps.begin(); - for(; s!=0; s--) - { - PRECONDITION(it != SSA_steps.end()); - it++; - } - return it; - } - void output(std::ostream &out) const; - void clear() - { - SSA_steps.clear(); - } - bool has_threads() const { return std::any_of( @@ -283,6 +227,44 @@ class symex_target_equationt:public symex_targett } protected: + /// Converts assignments: set the equality _lhs==rhs_ to _True_. + /// \param decision_procedure: A handle to a decision procedure + /// interface + void convert_assignments(decision_proceduret &decision_procedure); + + /// Converts declarations: these are effectively ignored by the decision + /// procedure. + /// \param decision_procedure: A handle to a decision procedure + /// interface + void convert_decls(decision_proceduret &decision_procedure); + + /// Converts assumptions: convert the expression the assumption represents. + /// \param decision_procedure: A handle to a decision procedure interface + void convert_assumptions(decision_proceduret &decision_procedure); + + /// Converts constraints: set the represented condition to _True_. + /// \param decision_procedure: A handle to a decision procedure interface + void convert_constraints(decision_proceduret &decision_procedure); + + /// Converts goto instructions: convert the expression representing the + /// condition of this goto. + /// \param decision_procedure: A handle to a decision procedure interface + void convert_goto_instructions(decision_proceduret &decision_procedure); + + /// Converts guards: convert the expression the guard represents. + /// \param decision_procedure: A handle to a decision procedure interface + void convert_guards(decision_proceduret &decision_procedure); + + /// Converts function calls: for each argument build an equality between its + /// symbol and the argument itself. + /// \param decision_procedure: A handle to a decision procedure interface + void convert_function_calls(decision_proceduret &decision_procedure); + + /// Converts I/O: for each argument build an equality between its + /// symbol and the argument itself. + /// \param decision_procedure: A handle to a decision procedure interface + void convert_io(decision_proceduret &decision_procedure); + messaget log; // for enforcing sharing in the expressions stored