From 20a84fb5f42a6bd8fd0495c0d4eade8e7e693361 Mon Sep 17 00:00:00 2001 From: johndumbell Date: Fri, 11 Jan 2019 14:57:12 +0000 Subject: [PATCH] Adding additional symex documentation --- src/analyses/dirty.h | 3 ++ src/goto-symex/goto_symex.h | 5 ++ src/goto-symex/goto_symex_state.h | 60 ++++++++++++++++++++++-- src/goto-symex/symex_target_equation.cpp | 3 ++ 4 files changed, 68 insertions(+), 3 deletions(-) diff --git a/src/analyses/dirty.h b/src/analyses/dirty.h index 986b4334ed4..97aa404d5a7 100644 --- a/src/analyses/dirty.h +++ b/src/analyses/dirty.h @@ -20,6 +20,9 @@ Date: March 2013 #include #include +/// Dirty variables are ones which have their address taken so we can't +/// reliably work out where they may be assigned and are also considered shared +/// state in the presence of multi-threading. class dirtyt { private: diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 1706bfd7eaa..e50d0097bd2 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -473,6 +473,11 @@ class goto_symext } }; +/// Transition to the next instruction, which increments the internal program +/// counter and initializes the loop counter when it detects a loop (or +/// recursion) being entered. 'Next instruction' in this situation refers +/// to the next one in program order, so it ignores things like unconditional +/// GOTOs, and only goes until the end of the current function. void symex_transition(goto_symext::statet &state); void symex_transition( diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index c1b0e56e9e2..3eb88a4b88b 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -30,7 +30,14 @@ Author: Daniel Kroening, kroening@kroening.com #include "renaming_level.h" #include "symex_target_equation.h" -// central data structure: state +/// Central data structure: state. + +/// The state is a persistent data structure that symex maintains as it +/// executes. As we walk over each instruction, state will be updated reflecting +/// their effects until a branch occurs (such as an if), where parts of the +/// state will be copied into a \ref goto_statet, stored in a map for later +/// reference and then merged again (via merge_goto) once it reaches a +/// control-flow graph convergence. class goto_symex_statet final { public: @@ -54,6 +61,11 @@ class goto_symex_statet final /// distance from entry unsigned depth; + // A guard is a particular condition that has to pass for an instruction + // to be executed. The easiest example is an if/else: each instruction along + // 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{}}; symex_targett::sourcet source; symex_target_equationt *symex_target; @@ -65,13 +77,43 @@ class goto_symex_statet final symex_level1t level1; symex_level2t level2; - // Map L1 names to (L2) constants + // Map L1 names to (L2) constants. Values will be evicted from this map + // when they become non-constant. This is used to propagate values that have + // been worked out to only have one possible value. + // + // "constants" can include symbols, but only in the context of an address-of + // op (i.e. &x can be propagated), and an address-taken thing should only be + // L1. std::map propagation; void output_propagation_map(std::ostream &); + // Symex renaming levels. enum levelt { L0=0, L1=1, L2=2 }; - // performs renaming _up to_ the given level + /// Rewrites symbol expressions in \ref exprt, applying a suffix to each + /// symbol reflecting its most recent version, which differs depending on + /// which level you requested. Each level also updates its predecessors, so + /// a L1 rename will update L1 and L0. A L2 will update L2, L1 and L0. + /// + /// What happens at each level: + /// L0. Applies a suffix giving the current thread number. (Excludes + /// guards, dynamic objects and anything not considered thread-local) + /// L1. Applies a suffix giving the current loop iteration or recursive + /// function invocation. + /// L2. Applies a suffix giving the generation of this variable. + /// + /// Renaming will not increment any of these values, just update the + /// expression with them. Levels matter when reading a variable, for + /// example: reading the value of x really means reading the particular x + /// symbol for this thread (L0 renaming, if applicable), the most recent + /// instance of x (L1 renaming), and the most recent write to x (L2 renaming). + /// + /// The above example after being renamed could look like this: 'x!0@0#42'. + /// That states it's the 42nd generation of this variable, on the first + /// thread, in the first frame. + /// + /// A full explanation of SSA (which is why we do this renaming) is in + /// the SSA section of background-concepts.md. void rename(exprt &expr, const namespacet &ns, levelt level=L2); void rename( typet &type, @@ -93,8 +135,13 @@ class goto_symex_statet final protected: void rename_address(exprt &expr, const namespacet &ns, levelt level); + /// Update level 0 values. void set_l0_indices(ssa_exprt &expr, const namespacet &ns); + + /// Update level 0 and 1 values. void set_l1_indices(ssa_exprt &expr, const namespacet &ns); + + /// Update level 0, 1 and 2 values. void set_l2_indices(ssa_exprt &expr, const namespacet &ns); // this maps L1 names to (L2) types @@ -108,6 +155,10 @@ class goto_symex_statet final // do dereferencing value_sett value_set; + /// Container for data that varies per program point, e.g. the constant + /// propagator state, when state needs to branch. This is copied out of + /// goto_symex_statet at a control-flow fork and then back into it at a + /// control-flow merge. class goto_statet { public: @@ -266,6 +317,9 @@ class goto_symex_statet final bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns); bool record_events; + + // Local variables are considered 'dirty' if they've had an address taken and + // therefore may be referred to by a pointer. incremental_dirtyt dirty; goto_programt::const_targett saved_target; diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index cdb7dfc3d1c..7fdf8b6012a 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -659,6 +659,9 @@ void symex_target_equationt::convert_io( } } +/// Merging causes identical ireps to be shared. +/// This is only enabled if the definition SHARING is defined. +/// \param SSA_step The step you want to have shared values. void symex_target_equationt::merge_ireps(SSA_stept &SSA_step) { merge_irep(SSA_step.guard);