Merge pull request #4703 from hannes-steffenhagen-diffblue/feature/goto-analyzer-usability

Preparation to make goto-analyzer work with the goto_verifiert framework

Author: tautschnig

src/analyses/ai.h

@@ -68,12 +68,12 @@ class ai_baset
   }
 
   /// Run abstract interpretation on a whole program
-  void operator()(const goto_modelt &goto_model)
+  void operator()(const abstract_goto_modelt &goto_model)
   {
-    const namespacet ns(goto_model.symbol_table);
-    initialize(goto_model.goto_functions);
-    entry_state(goto_model.goto_functions);
-    fixedpoint(goto_model.goto_functions, ns);
+    const namespacet ns(goto_model.get_symbol_table());
+    initialize(goto_model.get_goto_functions());
+    entry_state(goto_model.get_goto_functions());
+    fixedpoint(goto_model.get_goto_functions(), ns);
     finalize();
   }
 
@@ -374,7 +374,7 @@ class ai_baset
 ///    \ref ai_baset#operator()(const irep_idt&,const goto_programt&, <!--
 ///    --> const namespacet&),
 ///    \ref ai_baset#operator()(const goto_functionst&,const namespacet&)
-///    and \ref ai_baset#operator()(const goto_modelt&)
+///    and \ref ai_baset#operator()(const abstract_goto_modelt&)
 /// 2. Accessing the results of an analysis, by looking up the result
 ///    for a given location \p l using
 ///    \ref ait#operator[](goto_programt::const_targett).

src/goto-analyzer/CMakeLists.txt

@@ -12,6 +12,7 @@ target_link_libraries(goto-analyzer-lib
     cpp
     linking
     big-int
+    goto-checker
     goto-programs
     analyses
     pointer-analysis

src/goto-analyzer/Makefile

@@ -13,6 +13,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../cpp/cpp$(LIBEXT) \
       ../linking/linking$(LIBEXT) \
       ../big-int/big-int$(LIBEXT) \
+      ../goto-checker/goto-checker$(LIBEXT) \
       ../goto-programs/goto-programs$(LIBEXT) \
       ../analyses/analyses$(LIBEXT) \
       ../pointer-analysis/pointer-analysis$(LIBEXT) \

src/goto-analyzer/module_dependencies.txt

@@ -3,6 +3,7 @@ analyses
 assembler
 cpp
 goto-analyzer
+goto-checker
 goto-programs
 java_bytecode # will go away
 langapi # should go away

src/goto-analyzer/static_verifier.cpp

@@ -27,6 +27,49 @@ struct static_verifier_resultt
   irep_idt function_id;
 };
 
+void static_verifier(
+  const abstract_goto_modelt &abstract_goto_model,
+  const ai_baset &ai,
+  propertiest &properties)
+{
+  const namespacet ns{abstract_goto_model.get_symbol_table()};
+  // this is mutable because we want to change the property status
+  // in this loop
+  for(auto &property : properties)
+  {
+    auto &property_status = property.second.status;
+    const goto_programt::const_targett &property_location = property.second.pc;
+    exprt condition = property_location->get_condition();
+    const std::unique_ptr<ai_baset::statet> predecessor_state_copy =
+      ai.abstract_state_before(property_location);
+    // simplify the condition given the domain information we have
+    // about the state right before the assertion is evaluated
+    predecessor_state_copy->ai_simplify(condition, ns);
+    // if the condition simplifies to true the assertion always succeeds
+    if(condition.is_true())
+    {
+      property_status = property_statust::PASS;
+    }
+    // if the condition simplifies to false the assertion always fails
+    else if(condition.is_false())
+    {
+      property_status = property_statust::FAIL;
+    }
+    // if the domain state is bottom then the assertion is definitely
+    // unreachable
+    else if(predecessor_state_copy->is_bottom())
+    {
+      property_status = property_statust::NOT_REACHABLE;
+    }
+    // if the condition isn't definitely true, false or unreachable
+    // we don't know whether or not it may fail
+    else
+    {
+      property_status = property_statust::UNKNOWN;
+    }
+  }
+}
+
 /// Makes a status message string from a status.
 static const char *message(const static_verifier_resultt::statust &status)
 {

src/goto-analyzer/static_verifier.h

@@ -9,8 +9,10 @@ Author: Martin Brain, [email protected]
 #ifndef CPROVER_GOTO_ANALYZER_STATIC_VERIFIER_H
 #define CPROVER_GOTO_ANALYZER_STATIC_VERIFIER_H
 
+#include <goto-checker/properties.h>
 #include <iosfwd>
 
+class abstract_goto_modelt;
 class ai_baset;
 class goto_modelt;
 class message_handlert;
@@ -23,4 +25,15 @@ bool static_verifier(
   message_handlert &,
   std::ostream &);
 
+/// Use the information from the abstract interpreter to fill out the statuses
+/// of the passed properties
+/// \param abstract_goto_model The goto program to verify
+/// \param ai The abstract interpreter (should be run to fixpoint
+///           before calling this function)
+/// \param properties The properties to fill out
+void static_verifier(
+  const abstract_goto_modelt &abstract_goto_model,
+  const ai_baset &ai,
+  propertiest &properties);
+
 #endif // CPROVER_GOTO_ANALYZER_STATIC_VERIFIER_H