From bff5bf4819b8533633a9a204fe94f24f767ab50c Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Tue, 13 Nov 2018 15:20:35 +0000 Subject: [PATCH] Class and function documentation for goto-symex/symex_target 1) Document the symex_target interface. 2) Document the symex_target_equation -- Mostly SSA_stept and the transformations into it. --- src/goto-symex/goto_symex.h | 6 + src/goto-symex/symex_target.h | 155 +++++++++++++++++++---- src/goto-symex/symex_target_equation.cpp | 37 +----- src/goto-symex/symex_target_equation.h | 110 +++++++++++++--- 4 files changed, 229 insertions(+), 79 deletions(-) diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index d9678aa4096..0921be1c5d5 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -397,6 +397,12 @@ class goto_symext guardt &, assignment_typet); + /// Store the \p what expression by recursively descending into the operands + /// of \p lhs until the first operand \c op0 is _nil_: this _nil_ operand + /// is then replaced with \p what. + /// \param lhs: Non-symbol pointed-to expression + /// \param what: The expression to be added to the \p lhs + /// \return The resulting expression static exprt add_to_lhs(const exprt &lhs, const exprt &what); virtual void symex_gcc_builtin_va_arg_next( diff --git a/src/goto-symex/symex_target.h b/src/goto-symex/symex_target.h index 93161c43a0e..ba8b8af4157 100644 --- a/src/goto-symex/symex_target.h +++ b/src/goto-symex/symex_target.h @@ -17,6 +17,9 @@ Author: Daniel Kroening, kroening@kroening.com class ssa_exprt; class symbol_exprt; +/// The interface of the target _container_ for symbolic execution to record its +/// symbolic steps into. Presently, \ref symex_target_equationt is the only +/// implementation of this interface. class symex_targett { public: @@ -26,6 +29,9 @@ class symex_targett virtual ~symex_targett() { } + /// Identifies source in the context of symbolic execution. Thread number + /// `thread_nr` is zero by default and the program counter `pc` points to the + /// first instruction of the input GOTO program. struct sourcet { unsigned thread_nr; @@ -65,21 +71,45 @@ class symex_targett GUARD, }; - // read event + /// Read from a shared variable \p ssa_object (which is both the left- and the + /// right--hand side of assignment): we effectively assign the value stored in + /// \p ssa_object by another thread to \p ssa_object in the memory scope of + /// this thread. + /// \param guard: Precondition for this read event + /// \param ssa_object: Variable to be read from + /// \param atomic_section_id: ID of the atomic section in which this read + /// takes place (if any) + /// \param source: Pointer to location in the input GOTO program of this read virtual void shared_read( const exprt &guard, - const ssa_exprt &ssa_rhs, + const ssa_exprt &ssa_object, unsigned atomic_section_id, - const sourcet &source)=0; - - // write event + const sourcet &source) = 0; + + /// Write to a shared variable \p ssa_object: we effectively assign a value + /// from this thread to be visible by other threads. + /// \param guard: Precondition for this write event + /// \param ssa_object: Variable to be written to + /// \param atomic_section_id: ID of the atomic section in which this write + /// takes place (if any) + /// \param source: Pointer to location in the input GOTO program of this write virtual void shared_write( const exprt &guard, - const ssa_exprt &ssa_rhs, + const ssa_exprt &ssa_object, unsigned atomic_section_id, - const sourcet &source)=0; - - // write event - lhs must be symbol + const sourcet &source) = 0; + + /// Write to a local variable. The `cond_expr` is _lhs==rhs_. + /// \param guard: Precondition for this read event + /// \param ssa_lhs: Variable to be written to, must be a symbol (and not nil) + /// \param ssa_full_lhs: Full left-hand side with symex level annotations + /// \param original_full_lhs: Full left-hand side without symex level + /// annotations + /// \param ssa_rhs: Right-hand side of the assignment + /// \param source: Pointer to location in the input GOTO program of this + /// assignment + /// \param assignment_type: To distinguish between different types of + /// assignments (some may be hidden for the further analysis) virtual void assignment( const exprt &guard, const ssa_exprt &ssa_lhs, @@ -89,20 +119,36 @@ class symex_targett const sourcet &source, assignment_typet assignment_type)=0; - // declare fresh variable - lhs must be symbol + /// Declare a fresh variable. The `cond_expr` is _lhs==lhs_. + /// \param guard: Precondition for a declaration of this variable + /// \param ssa_lhs: Variable to be declared, must be symbol (and not nil) + /// \param source: Pointer to location in the input GOTO program of this + /// declaration + /// \param assignment_type: To distinguish between different types of + /// assignments (some may be hidden for the further analysis) virtual void decl( const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source, assignment_typet assignment_type)=0; - // note the death of a variable - lhs must be symbol + /// Remove a variable from the scope. + /// \param guard: Precondition for removal of this variable + /// \param ssa_lhs: Variable to be removed, must be symbol + /// \param source: Pointer to location in the input GOTO program of this + /// removal virtual void dead( const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)=0; - // record a function call + /// Record a function call. + /// \param guard: Precondition for calling a function + /// \param function_identifier: Name of the function + /// \param ssa_function_arguments: Vector of arguments in SSA form + /// \param source: To location in the input GOTO program of this + /// \param hidden: Should this step be recorded as hidden? + /// function call virtual void function_call( const exprt &guard, const irep_idt &function_identifier, @@ -110,23 +156,41 @@ class symex_targett const sourcet &source, bool hidden) = 0; - // record return from a function + /// Record return from a function. + /// \param guard: Precondition for returning from a function + /// \param source: Pointer to location in the input GOTO program of this + /// \param hidden: Should this step be recorded as hidden? + /// function return virtual void function_return(const exprt &guard, const sourcet &source, bool hidden) = 0; - // just record a location + /// Record a location. + /// \param guard: Precondition for reaching this location + /// \param source: Pointer to location in the input GOTO program to be + /// recorded virtual void location( const exprt &guard, const sourcet &source)=0; - // record output + /// Record an output. + /// \param guard: Precondition for writing to the output + /// \param source: Pointer to location in the input GOTO program of this + /// output + /// \param output_id: Name of the output + /// \param args: A list of IO arguments virtual void output( const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list &args)=0; - // record formatted output + /// Record formatted output. + /// \param guard: Precondition for writing to the output + /// \param source: Pointer to location in the input GOTO program of this + /// output + /// \param output_id: Name of the output + /// \param fmt: Formatting string + /// \param args: A list of IO arguments virtual void output_fmt( const exprt &guard, const sourcet &source, @@ -134,59 +198,102 @@ class symex_targett const irep_idt &fmt, const std::list &args)=0; - // record input + /// Record an input. + /// \param guard: Precondition for reading from the input + /// \param source: Pointer to location in the input GOTO program of this + /// input + /// \param input_id: Name of the input + /// \param args: A list of IO arguments virtual void input( const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list &args)=0; - // record an assumption + /// Record an assumption. + /// \param guard: Precondition for reaching this assumption + /// \param cond: Condition this assumption represents + /// \param source: Pointer to location in the input GOTO program of this + /// assumption virtual void assumption( const exprt &guard, const exprt &cond, const sourcet &source)=0; - // record an assertion + /// Record an assertion. + /// \param guard: Precondition for reaching this assertion + /// \param cond: Condition this assertion represents + /// \param msg: The message associated with this assertion + /// \param source: Pointer to location in the input GOTO program of this + /// assertion virtual void assertion( const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)=0; - // record a goto + /// Record a goto instruction. + /// \param guard: Precondition for reaching this goto instruction + /// \param cond: Condition under which this goto should be taken + /// \param source: Pointer to location in the input GOTO program of this + /// goto instruction virtual void goto_instruction( const exprt &guard, const exprt &cond, const sourcet &source)=0; - // record a constraint + /// Record a _global_ constraint: there is no guard limiting its scope. + /// \param cond: Condition represented by this constraint + /// \param msg: The message associated with this constraint + /// \param source: Pointer to location in the input GOTO program of this + /// constraint virtual void constraint( const exprt &cond, const std::string &msg, const sourcet &source)=0; - // record thread spawn + /// Record spawning a new thread + /// \param guard: Precondition for reaching spawning a new thread + /// \param source: Pointer to location in the input GOTO program where a new + /// thread is to be spawned virtual void spawn( const exprt &guard, const sourcet &source)=0; - // record memory barrier + /// Record creating a memory barrier + /// \param guard: Precondition for reaching this barrier + /// \param source: Pointer to location in the input GOTO program where a new + /// barrier is created virtual void memory_barrier( const exprt &guard, const sourcet &source)=0; - // record atomic section + /// Record a beginning of an atomic section + /// \param guard: Precondition for reaching this atomic section + /// \param atomic_section_id: Identifier for this atomic section + /// \param source: Pointer to location in the input GOTO program where an + /// atomic section begins virtual void atomic_begin( const exprt &guard, unsigned atomic_section_id, const sourcet &source)=0; + + /// Record ending an atomic section + /// \param guard: Precondition for reaching the end of this atomic section + /// \param atomic_section_id: Identifier for this atomic section + /// \param source: Pointer to location in the input GOTO program where an + /// atomic section ends virtual void atomic_end( const exprt &guard, unsigned atomic_section_id, const sourcet &source)=0; }; +/// Base class comparison operator for symbolic execution targets. Order first +/// by thread numbers and then by program counters. +/// \param a: Left-hand target +/// \param b: Right-hand target +/// \return _True_ if `a` precedes `b`. bool operator < ( const symex_targett::sourcet &a, const symex_targett::sourcet &b); diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 2198c08641c..6daf2fbfa67 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// Symbolic Execution +/// Implementation of functions to build SSA equation. #include "symex_target_equation.h" @@ -27,7 +28,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "equation_conversion_exceptions.h" #include "goto_symex_state.h" -/// read from a shared variable void symex_target_equationt::shared_read( const exprt &guard, const ssa_exprt &ssa_object, @@ -46,7 +46,6 @@ void symex_target_equationt::shared_read( merge_ireps(SSA_step); } -/// write to a sharedvariable void symex_target_equationt::shared_write( const exprt &guard, const ssa_exprt &ssa_object, @@ -124,7 +123,6 @@ void symex_target_equationt::atomic_end( merge_ireps(SSA_step); } -/// write to a variable void symex_target_equationt::assignment( const exprt &guard, const ssa_exprt &ssa_lhs, @@ -155,7 +153,6 @@ void symex_target_equationt::assignment( merge_ireps(SSA_step); } -/// declare a fresh variable void symex_target_equationt::decl( const exprt &guard, const ssa_exprt &ssa_lhs, @@ -191,7 +188,6 @@ void symex_target_equationt::dead( // we currently don't record these } -/// just record a location void symex_target_equationt::location( const exprt &guard, const sourcet &source) @@ -206,7 +202,6 @@ void symex_target_equationt::location( merge_ireps(SSA_step); } -/// just record a location void symex_target_equationt::function_call( const exprt &guard, const irep_idt &function_identifier, @@ -227,7 +222,6 @@ void symex_target_equationt::function_call( merge_ireps(SSA_step); } -/// just record a location void symex_target_equationt::function_return( const exprt &guard, const sourcet &source, @@ -244,7 +238,6 @@ void symex_target_equationt::function_return( merge_ireps(SSA_step); } -/// just record output void symex_target_equationt::output( const exprt &guard, const sourcet &source, @@ -263,7 +256,6 @@ void symex_target_equationt::output( merge_ireps(SSA_step); } -/// just record formatted output void symex_target_equationt::output_fmt( const exprt &guard, const sourcet &source, @@ -285,7 +277,6 @@ void symex_target_equationt::output_fmt( merge_ireps(SSA_step); } -/// just record input void symex_target_equationt::input( const exprt &guard, const sourcet &source, @@ -304,7 +295,6 @@ void symex_target_equationt::input( merge_ireps(SSA_step); } -/// record an assumption void symex_target_equationt::assumption( const exprt &guard, const exprt &cond, @@ -321,7 +311,6 @@ void symex_target_equationt::assumption( merge_ireps(SSA_step); } -/// record an assertion void symex_target_equationt::assertion( const exprt &guard, const exprt &cond, @@ -340,7 +329,6 @@ void symex_target_equationt::assertion( merge_ireps(SSA_step); } -/// record a goto instruction void symex_target_equationt::goto_instruction( const exprt &guard, const exprt &cond, @@ -357,7 +345,6 @@ void symex_target_equationt::goto_instruction( merge_ireps(SSA_step); } -/// record a constraint void symex_target_equationt::constraint( const exprt &cond, const std::string &msg, @@ -399,9 +386,6 @@ void symex_target_equationt::convert( } } -/// converts assignments -/// \par parameters: decision procedure -/// \return - void symex_target_equationt::convert_assignments( decision_proceduret &decision_procedure) const { @@ -421,8 +405,6 @@ void symex_target_equationt::convert_assignments( } } -/// converts declarations -/// \return - void symex_target_equationt::convert_decls( prop_convt &prop_conv) const { @@ -446,8 +428,6 @@ void symex_target_equationt::convert_decls( } } -/// converts guards -/// \return - void symex_target_equationt::convert_guards( prop_convt &prop_conv) { @@ -478,8 +458,6 @@ void symex_target_equationt::convert_guards( } } -/// converts assumptions -/// \return - void symex_target_equationt::convert_assumptions( prop_convt &prop_conv) { @@ -513,8 +491,6 @@ void symex_target_equationt::convert_assumptions( } } -/// converts goto instructions -/// \return - void symex_target_equationt::convert_goto_instructions( prop_convt &prop_conv) { @@ -548,9 +524,6 @@ void symex_target_equationt::convert_goto_instructions( } } -/// converts constraints -/// \par parameters: decision procedure -/// \return - void symex_target_equationt::convert_constraints( decision_proceduret &decision_procedure) const { @@ -582,8 +555,6 @@ void symex_target_equationt::convert_constraints( } } -/// converts assertions -/// \return - void symex_target_equationt::convert_assertions( prop_convt &prop_conv) { @@ -665,9 +636,6 @@ void symex_target_equationt::convert_assertions( prop_conv.set_to_true(disjunction(disjuncts)); } -/// converts function calls -/// \par parameters: decision procedure -/// \return - void symex_target_equationt::convert_function_calls( decision_proceduret &dec_proc) { @@ -698,9 +666,6 @@ void symex_target_equationt::convert_function_calls( } } -/// converts I/O -/// \par parameters: decision procedure -/// \return - void symex_target_equationt::convert_io( decision_proceduret &dec_proc) { diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h index 34d5058c8f6..d5c7f4ac2a6 100644 --- a/src/goto-symex/symex_target_equation.h +++ b/src/goto-symex/symex_target_equation.h @@ -29,26 +29,29 @@ class decision_proceduret; class namespacet; class prop_convt; +/// Inheriting the interface of symex_targett this class represents the SSA +/// form of the input program as a list of \ref SSA_stept. It further extends +/// the base class by providing a conversion interface for decision procedures. class symex_target_equationt:public symex_targett { public: virtual ~symex_target_equationt() = default; - // read event + /// \copydoc symex_targett::shared_read() virtual void shared_read( const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source); - // write event + /// \copydoc symex_targett::shared_write() virtual void shared_write( const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source); - // assignment to a variable - lhs must be symbol + /// \copydoc symex_targett::assignment() virtual void assignment( const exprt &guard, const ssa_exprt &ssa_lhs, @@ -58,20 +61,20 @@ class symex_target_equationt:public symex_targett const sourcet &source, assignment_typet assignment_type); - // declare fresh variable - lhs must be symbol + /// \copydoc symex_targett::decl() virtual void decl( const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source, assignment_typet assignment_type); - // note the death of a variable - lhs must be symbol + /// \copydoc symex_targett::dead() virtual void dead( const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source); - // record a function call + /// \copydoc symex_targett::function_call() virtual void function_call( const exprt &guard, const irep_idt &function_identifier, @@ -79,23 +82,23 @@ class symex_target_equationt:public symex_targett const sourcet &source, bool hidden); - // record return from a function + /// \copydoc symex_targett::function_return() virtual void function_return(const exprt &guard, const sourcet &source, bool hidden); - // just record a location + /// \copydoc symex_targett::location() virtual void location( const exprt &guard, const sourcet &source); - // output + /// \copydoc symex_targett::output() virtual void output( const exprt &guard, const sourcet &source, - const irep_idt &fmt, + const irep_idt &output_id, const std::list &args); - // output, formatted + /// \copydoc symex_targett::output_fmt() virtual void output_fmt( const exprt &guard, const sourcet &source, @@ -103,71 +106,140 @@ class symex_target_equationt:public symex_targett const irep_idt &fmt, const std::list &args); - // input + /// \copydoc symex_targett::input() virtual void input( const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list &args); - // record an assumption + /// \copydoc symex_targett::assumption() virtual void assumption( const exprt &guard, const exprt &cond, const sourcet &source); - // record an assertion + /// \copydoc symex_targett::assertion() virtual void assertion( const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source); - // record a goto + /// \copydoc symex_targett::goto_instruction() virtual void goto_instruction( const exprt &guard, const exprt &cond, const sourcet &source); - // record a (global) constraint + /// \copydoc symex_targett::constraint() virtual void constraint( const exprt &cond, const std::string &msg, const sourcet &source); - // record thread spawn + /// \copydoc symex_targett::spawn() virtual void spawn( const exprt &guard, const sourcet &source); - // record memory barrier + /// \copydoc symex_targett::memory_barrier() virtual void memory_barrier( const exprt &guard, const sourcet &source); - // record atomic section + /// \copydoc symex_targett::atomic_begin() virtual void atomic_begin( const exprt &guard, unsigned atomic_section_id, const sourcet &source); + + /// \copydoc symex_targett::atomic_end() virtual void atomic_end( const exprt &guard, unsigned atomic_section_id, const sourcet &source); + /// Interface method to initiate the conversion into a decision procedure + /// format. The method iterates over the equation, i.e. over the SSA steps and + /// converts each type of step separately. + /// \param prop_conv: A handle to a particular decision procedure interface void convert(prop_convt &prop_conv); + + /// Converts assignments: set the equality _lhs==rhs_ to _True_. + /// \param decision_procedure: A handle to a particular decision procedure + /// interface void convert_assignments(decision_proceduret &decision_procedure) const; + + /// Converts declarations: these are effectively ignored by the decision + /// procedure. + /// \param prop_conv: A handle to a particular decision procedure interface void convert_decls(prop_convt &prop_conv) const; + + /// Converts assumptions: convert the expression the assumption represents. + /// \param prop_conv: A handle to a particular decision procedure interface void convert_assumptions(prop_convt &prop_conv); + + /// Converts assertions: build a disjunction of negated assertions. + /// \param prop_conv: A handle to a particular decision procedure interface void convert_assertions(prop_convt &prop_conv); + + /// Converts constraints: set the represented condition to _True_. + /// \param decision_procedure: A handle to a particular decision procedure + /// interface void convert_constraints(decision_proceduret &decision_procedure) const; + + /// Converts goto instructions: convert the expression representing the + /// condition of this goto. + /// \param prop_conv: A handle to a particular decision procedure interface void convert_goto_instructions(prop_convt &prop_conv); + + /// Converts guards: convert the expression the guard represents. + /// \param prop_conv: A handle to a particular decision procedure interface void convert_guards(prop_convt &prop_conv); + + /// Converts function calls: for each argument build an equality between its + /// symbol and the argument itself. + /// \param decision_procedure: A handle to a particular 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 particular decision procedure + /// interface void convert_io(decision_proceduret &decision_procedure); exprt make_expression() const; + /// Single SSA step in the equation. Its `type` is defined as + /// goto_trace_stept::typet. Every SSA step has a `source` to identify its + /// origin in the input GOTO program and a `guard` expression which holds + /// the path condition required to reach this step: they limit the scope of + /// this step. + /// + /// SSA steps that represent assignments and declarations also store the + /// left- and right-hand sides of the assignment. The left-hand side + /// `ssa_lhs` is required to be of type ssa_exprt: in SSA form, variables + /// are only assigned once, see \ref static-single-assignment. To achieve + /// that, we annotate the original name with 3 types of levels, see + /// ssa_exprt. The assignment step also represents the left-hand side in two + /// other _full_ forms: `ssa_full_lhs` and `original_full_lhs`, which store + /// the original expressions from the input GOTO program before removing + /// array indexes, pointers, etc. The `ssa_full_lhs` uses the level-annotated + /// names. + /// + /// Assumptions, assertions, goto steps, and constraints have `cond_expr` + /// which represent the condition guarding this step, i.e. what must hold for + /// this step to be taken. Both `guard` and `cond_expr` will later be + /// translated into verification condition for the SAT/SMT solver (or some + /// other decision procedure), to be referred by their respective literals. + /// Constraints usually arise from external conditions, such as memory models + /// or partial orders: they represent assumptions with global effect. + /// + /// Function calls store `called_function` name as well as a vector of + /// arguments `ssa_function_arguments`. The `converted` version of a + /// variable will contain its version for the SAT/SMT conversion. class SSA_stept { public: