(codethorn) rearranged header files and namespace to pass policies

* moved using directives to pass ROSE-core policies * restructured some of the header files for this purpose * removed z3-prover connection (obsolete) modified: tools/CodeThorn/src/CPAstAttribute.C modified: tools/CodeThorn/src/CPAstAttribute.h modified: tools/CodeThorn/src/CTAnalysis.C modified: tools/CodeThorn/src/CTAnalysis.h modified: tools/CodeThorn/src/CodeThornLib.h modified: tools/CodeThorn/src/CodeThornPasses.C modified: tools/CodeThorn/src/ConstantConditionAnalysis.C modified: tools/CodeThorn/src/ConstantConditionAnalysis.h modified: tools/CodeThorn/src/ContNodeAttribute.h modified: tools/CodeThorn/src/CtxUnfoldedAnalysis.C modified: tools/CodeThorn/src/EState.C modified: tools/CodeThorn/src/EState.h modified: tools/CodeThorn/src/EStatePriorityWorkList.C modified: tools/CodeThorn/src/ExecutionTrace.h modified: tools/CodeThorn/src/FIConstAnalysis.C modified: tools/CodeThorn/src/FIConstAnalysis.h modified: tools/CodeThorn/src/InternalChecks.C modified: tools/CodeThorn/src/LoopInfo.h modified: tools/CodeThorn/src/Makefile.am modified: tools/CodeThorn/src/Normalization.h modified: tools/CodeThorn/src/NormalizationInliner.h modified: tools/CodeThorn/src/PredefinedSemanticFunctions.C modified: tools/CodeThorn/src/PredefinedSemanticFunctions.h modified: tools/CodeThorn/src/PropertyValueTable.h modified: tools/CodeThorn/src/RERS_empty_specialization.C modified: tools/CodeThorn/src/ReachabilityAnalysis.C modified: tools/CodeThorn/src/ReachabilityAnalysis.h modified: tools/CodeThorn/src/ReadWriteData.h modified: tools/CodeThorn/src/RoseCompatibility.C modified: tools/CodeThorn/src/Specialization.h modified: tools/CodeThorn/src/Thorn4CommandLineParser.C modified: tools/CodeThorn/src/TransitionGraph.C modified: tools/CodeThorn/src/TransitionGraph.h modified: tools/CodeThorn/src/Visualizer.C modified: tools/CodeThorn/src/Visualizer.h modified: tools/CodeThorn/src/defUseQuery.C modified: tools/CodeThorn/src/defUseQuery.h modified: tools/CodeThorn/src/ltlthorn-lib/CounterexampleAnalyzer.C modified: tools/CodeThorn/src/ltlthorn-lib/CounterexampleAnalyzer.h modified: tools/CodeThorn/src/ltlthorn-lib/LtsminConnection.C modified: tools/CodeThorn/src/ltlthorn-lib/LtsminConnection.h modified: tools/CodeThorn/src/ltlthorn-lib/ParProAnalyzer.C modified: tools/CodeThorn/src/ltlthorn-lib/ParProAnalyzer.h modified: tools/CodeThorn/src/ltlthorn-lib/ParProAutomata.C modified: tools/CodeThorn/src/ltlthorn-lib/ParProExplorer.C modified: tools/CodeThorn/src/ltlthorn-lib/ParProExplorer.h modified: tools/CodeThorn/src/ltlthorn-lib/ParProLtlMiner.h modified: tools/CodeThorn/src/ltlthorn-lib/ParProSpotState.C modified: tools/CodeThorn/src/ltlthorn-lib/ParProSpotState.h modified: tools/CodeThorn/src/ltlthorn-lib/ParProSpotSuccIter.C modified: tools/CodeThorn/src/ltlthorn-lib/ParProSpotSuccIter.h modified: tools/CodeThorn/src/ltlthorn-lib/ParProSpotTgba.C modified: tools/CodeThorn/src/ltlthorn-lib/ParProSpotTgba.h modified: tools/CodeThorn/src/ltlthorn-lib/ParProTransitionGraph.h modified: tools/CodeThorn/src/ltlthorn-lib/SpotConnection.C modified: tools/CodeThorn/src/ltlthorn-lib/SpotConnection.h modified: tools/CodeThorn/src/ltlthorn-lib/SpotMiscellaneous.C modified: tools/CodeThorn/src/ltlthorn-lib/SpotMiscellaneous.h modified: tools/CodeThorn/src/ltlthorn-lib/SpotRenameVisitor.C modified: tools/CodeThorn/src/ltlthorn-lib/SpotRenameVisitor.h modified: tools/CodeThorn/src/ltlthorn-lib/SpotState.C modified: tools/CodeThorn/src/ltlthorn-lib/SpotState.h modified: tools/CodeThorn/src/ltlthorn-lib/SpotSuccIter.C modified: tools/CodeThorn/src/ltlthorn-lib/SpotSuccIter.h modified: tools/CodeThorn/src/ltlthorn-lib/SpotTgba.C modified: tools/CodeThorn/src/ltlthorn-lib/SpotTgba.h modified: tools/CodeThorn/src/spotconnection/spotdriver.C modified: tools/CodeThorn/src/spotconnection/spotdriver.h modified: tools/CodeThorn/src/thorn2.C modified: tools/CodeThorn/src/thorn3.C modified: tools/CodeThorn/src/thorn4.C modified: tools/CodeThorn/src/woodpecker-src/DeadCodeElimination.C modified: tools/CodeThorn/src/woodpecker-src/DeadCodeElimination.h deleted: tools/CodeThorn/src/z3-prover-connection/PhiAttribute.C deleted: tools/CodeThorn/src/z3-prover-connection/PhiAttribute.h deleted: tools/CodeThorn/src/z3-prover-connection/PhiStatement.C deleted: tools/CodeThorn/src/z3-prover-connection/PhiStatement.h deleted: tools/CodeThorn/src/z3-prover-connection/ReachabilityAnalyzerZ3.C deleted: tools/CodeThorn/src/z3-prover-connection/ReachabilityAnalyzerZ3.h deleted: tools/CodeThorn/src/z3-prover-connection/SSAGenerator.C deleted: tools/CodeThorn/src/z3-prover-connection/SSAGenerator.h CODETHORN-70
SNSerHello · Oct 7, 2022 · e7ed029 · e7ed029
1 parent 5b37219
commit e7ed029
Show file tree

Hide file tree

Showing 81 changed files with 1,564 additions and 3,453 deletions.
diff --git a/tools/CodeThorn/src/CPAstAttribute.C b/tools/CodeThorn/src/CPAstAttribute.C
@@ -6,40 +6,46 @@
 #include "AstUtility.h"
 #include "FIConstAnalysis.h"
 
+using namespace std;
 using namespace AstUtility;
+using namespace CodeThorn;
 
-bool CPAstAttribute::isConstantInteger(VariableId varId) {
- ROSE_ASSERT(_elem);
- return _elem->isUniqueConst(varId);
-}
+namespace CodeThorn {
+
+ bool CPAstAttribute::isConstantInteger(VariableId varId) {
+ ROSE_ASSERT(_elem);
+ return _elem->isUniqueConst(varId);
+ }
 
-CPAstAttributeInterface::ConstantInteger CPAstAttribute::getConstantInteger(VariableId varId) {
- ROSE_ASSERT(_elem);
- return _elem->uniqueConst(varId);
-}
+ CPAstAttributeInterface::ConstantInteger CPAstAttribute::getConstantInteger(VariableId varId) {
+  ROSE_ASSERT(_elem);
+  return _elem->uniqueConst(varId);
+ }
 
-void CPAstAttribute::toStream(ostream& os, VariableIdMapping* vim) {
-}
+ void CPAstAttribute::toStream(ostream& os, VariableIdMapping* vim) {
+ }
 
-string CPAstAttribute::toString(){
- stringstream ss;
- VariableIdSet vset=_variableIdMapping->variableIdsOfAstSubTree(_node);
- for(VariableIdSet::iterator i=vset.begin();i!=vset.end();++i) {
- ss<<"("
- <<_variableIdMapping->uniqueVariableName(*i)
- <<",";
- if(isConstantInteger(*i)) {
- ss<<getConstantInteger(*i);
- } else {
- ss<<"any";
+ string CPAstAttribute::toString(){
+ stringstream ss;
+ VariableIdSet vset=_variableIdMapping->variableIdsOfAstSubTree(_node);
+ for(VariableIdSet::iterator i=vset.begin();i!=vset.end();++i) {
+ ss<<"("
+ <<_variableIdMapping->uniqueVariableName(*i)
+ <<",";
+ if(isConstantInteger(*i)) {
+ ss<<getConstantInteger(*i);
+ } else {
+ ss<<"any";
+ }
+ ss<<")";
  }
- ss<<")";
+ ss<<endl;
+ return ss.str();
+ }
+
+ CPAstAttribute::CPAstAttribute(CodeThorn::VariableConstInfo* elem, SgNode* node, VariableIdMapping* vid):_elem(elem),_node(node),_variableIdMapping(vid) {
  }
- ss<<endl;
- return ss.str();
-}
 
-CPAstAttribute::CPAstAttribute(VariableConstInfo* elem, SgNode* node, VariableIdMapping* vid):_elem(elem),_node(node),_variableIdMapping(vid) {
 }
 
 //CPAstAttribute::~CPAstAttribute() {

diff --git a/tools/CodeThorn/src/CPAstAttribute.h b/tools/CodeThorn/src/CPAstAttribute.h
@@ -5,33 +5,24 @@
 #include "VariableIdMapping.h"
 #include "CPAstAttributeInterface.h"
 #include "AbstractValue.h"
+#include "FIConstAnalysis.h"
 
-using namespace CodeThorn;
-
-class VariableConstInfo;
-
-/*! 
- * \author Markus Schordan
- * \date 2013.
- */
 class SgNode;
 
-class CPAstAttribute : public CPAstAttributeInterface {
- public:
- //virtual VariableIdSet allVariableIds();
- virtual bool isConstantInteger(VariableId varId);
- virtual CPAstAttributeInterface::ConstantInteger getConstantInteger(VariableId varId);
- //virtual iterator begin();
- //virtual iterator end();
- //virtual ~CPAstAttribute();
- public:
- CPAstAttribute(VariableConstInfo* elem, SgNode* node, VariableIdMapping* variableIdMapping);
- void toStream(ostream& os, VariableIdMapping* vim);
- string toString();
- private:
- VariableConstInfo* _elem;
- SgNode* _node;
- VariableIdMapping* _variableIdMapping;
-};
+namespace CodeThorn {
+ class CPAstAttribute : public CodeThorn::CPAstAttributeInterface {
+ public:
+ virtual bool isConstantInteger(CodeThorn::VariableId varId);
+ virtual CPAstAttributeInterface::ConstantInteger getConstantInteger(CodeThorn::VariableId varId);
+ //virtual ~CPAstAttribute();
+ CPAstAttribute(CodeThorn::VariableConstInfo* elem, SgNode* node, CodeThorn::VariableIdMapping* variableIdMapping);
+ void toStream(std::ostream& os, CodeThorn::VariableIdMapping* vim);
+ std::string toString();
+ private:
+ CodeThorn::VariableConstInfo* _elem;
+ SgNode* _node;
+ CodeThorn::VariableIdMapping* _variableIdMapping;
+ };
+}
 
 #endif
diff --git a/tools/CodeThorn/src/CTAnalysis.C b/tools/CodeThorn/src/CTAnalysis.C
@@ -1,4 +1,3 @@
-
 #include "sage3basic.h"
 #include "Labeler.h"
 #include "ClassHierarchyGraph.h"
@@ -27,6 +26,7 @@
 
 using namespace std;
 using namespace Sawyer::Message;
+using namespace CodeThorn;
 
 Sawyer::Message::Facility CodeThorn::CTAnalysis::logger;
 

diff --git a/tools/CodeThorn/src/CTAnalysis.h b/tools/CodeThorn/src/CTAnalysis.h
@@ -1,10 +1,6 @@
 #ifndef ANALYZER_H
 #define ANALYZER_H
 
-/*************************************************************
- * Author : Markus Schordan *
- *************************************************************/
-
 #include <iostream>
 #include <fstream>
 #include <set>
@@ -15,7 +11,6 @@
 #include <utility>
 
 #include <omp.h>
-
 #include <unordered_set>
 #include <unordered_map>
 
@@ -69,20 +64,13 @@ namespace CodeThorn {
 
  struct hash_pair {
  template <class T1, class T2>
- size_t operator()(const pair<T1, T2>& p) const
- {
- auto hash1 = hash<T1>{}(p.first);
- auto hash2 = hash<T2>{}(p.second);
+ size_t operator()(const std::pair<T1, T2>& p) const {
+ auto hash1 = std::hash<T1>{}(p.first);
+ auto hash2 = std::hash<T2>{}(p.second);
  return hash1 ^ hash2;
  }
  };
 
- /*!
- * \author Markus Schordan
- * \date 2012.
- */
-
-
  class CTAnalysis {
  friend class Solver12;
  friend class Visualizer;
@@ -133,8 +121,8 @@ namespace CodeThorn {
 
  // thread save; only prints if option status messages is enabled.
  void printStatusMessage(bool);
- void printStatusMessage(string s);
- void printStatusMessageLine(string s);
+ void printStatusMessage(std::string s);
+ void printStatusMessageLine(std::string s);
 
  // adds attributes for dot generation of AST with labels
  void generateAstNodeInfo(SgNode* node);
@@ -208,8 +196,8 @@ namespace CodeThorn {
  int getAbstractionMode() { return _abstractionMode; }
  void setInterpreterMode(CodeThorn::InterpreterMode mode);
  CodeThorn::InterpreterMode getInterpreterMode();
- void setInterpreterModeOutputFileName(string);
- string getInterpreterModeOutputFileName();
+ void setInterpreterModeOutputFileName(std::string);
+ std::string getInterpreterModeOutputFileName();
 
  bool getPrintDetectedViolations();
  void setPrintDetectedViolations(bool flag);
@@ -228,9 +216,9 @@ namespace CodeThorn {
  void setNumberOfThreadsToUse(int n) { _numberOfThreadsToUse=n; }
  int getNumberOfThreadsToUse() { return _numberOfThreadsToUse; }
  void setTreatStdErrLikeFailedAssert(bool x) { _treatStdErrLikeFailedAssert=x; }
- void setCompoundIncVarsSet(set<AbstractValue> ciVars);
- void setSmallActivityVarsSet(set<AbstractValue> ciVars);
- void setAssertCondVarsSet(set<AbstractValue> acVars);
+ void setCompoundIncVarsSet(std::set<AbstractValue> ciVars);
+ void setSmallActivityVarsSet(std::set<AbstractValue> ciVars);
+ void setAssertCondVarsSet(std::set<AbstractValue> acVars);
  /** allows to enable context sensitive analysis. Currently only
  call strings of arbitrary length are supported (recursion is
  not supported yet) */
@@ -255,8 +243,8 @@ namespace CodeThorn {
  /* command line options provided to analyzed application
  if set they are used to initialize the initial state with argv and argc domain abstractions
  */
- void setCommandLineOptions(vector<string> clOptions);
- vector<string> getCommandLineOptions();
+ void setCommandLineOptions(std::vector<std::string> clOptions);
+ std::vector<std::string> getCommandLineOptions();
  SgNode* getStartFunRoot();
  // exists with error message if any violation is detected
  void ensureToplogicSortFlowConsistency();
@@ -285,7 +273,7 @@ namespace CodeThorn {
  bool isIncompleteSTGReady();
  bool isPrecise();
 
- void reduceStg(function<bool(EStatePtr)> predicate);
+ void reduceStg(std::function<bool(EStatePtr)> predicate);
 
  void initializeAbstractStates(PStatePtr initialPStateStored);
  EStatePtr getAbstractState(CodeThorn::Label lab, CallString cs);
@@ -297,7 +285,7 @@ namespace CodeThorn {
  bool getOptionOutputWarnings();
 
  // first: list of new states (worklist), second: set of found existing states
- typedef pair<EStateWorkList,std::set<EStatePtr> > SubSolverResultType;
+ typedef std::pair<EStateWorkList,std::set<EStatePtr> > SubSolverResultType;
  SubSolverResultType subSolver(EStatePtr currentEStatePtr);
  std::string typeSizeMappingToString();
  void setModeLTLDriven(bool ltlDriven) { transitionGraph.setModeLTLDriven(ltlDriven); }
@@ -400,10 +388,10 @@ namespace CodeThorn {
  // to be moved to IOAnalyzer
  std::list<std::pair<SgLabelStatement*,SgNode*> > _assertNodes;
  GlobalTopifyMode _globalTopifyMode;
- set<AbstractValue> _compoundIncVarsSet;
- set<AbstractValue> _smallActivityVarsSet;
- set<AbstractValue> _assertCondVarsSet;
- set<int> _inputVarValues;
+ std::set<AbstractValue> _compoundIncVarsSet;
+ std::set<AbstractValue> _smallActivityVarsSet;
+ std::set<AbstractValue> _assertCondVarsSet;
+ std::set<int> _inputVarValues;
  LtlRersMapping _ltlRersMapping; // only used for LTL verification
  std::list<int> _inputSequence;
  std::list<int>::iterator _inputSequenceIterator;
@@ -461,15 +449,15 @@ namespace CodeThorn {
  bool _stdFunctionSemantics=true;
 
  bool _svCompFunctionSemantics;
- string _externalErrorFunctionName; // the call of this function causes termination of analysis
- string _externalNonDetIntFunctionName;
- string _externalNonDetLongFunctionName;
- string _externalExitFunctionName;
+ std::string _externalErrorFunctionName; // the call of this function causes termination of analysis
+ std::string _externalNonDetIntFunctionName;
+ std::string _externalNonDetLongFunctionName;
+ std::string _externalExitFunctionName;
 
  TimeMeasurement _analysisTimer;
  bool _timerRunning = false;
 
- std::vector<string> _commandLineOptions;
+ std::vector<std::string> _commandLineOptions;
  bool _contextSensitiveAnalysis;
  // this is used in abstract mode to hold a pointer to the
  // *current* summary state (more than one may be created to allow

diff --git a/tools/CodeThorn/src/CodeThornLib.h b/tools/CodeThorn/src/CodeThornLib.h
@@ -28,7 +28,7 @@ namespace CodeThorn {
  /* reads and parses LTL rers mapping file into the alphabet
  sets. Returns false if reading fails. Exits with error message if
  format is wrong. */
- bool readAndParseLTLRersMappingFile(string ltlRersMappingFileName, LtlRersMapping& ltlRersMapping);
+ bool readAndParseLTLRersMappingFile(std::string ltlRersMappingFileName, LtlRersMapping& ltlRersMapping);
  void processCtOptGenerateAssertions(CodeThornOptions& ctOpt, CTAnalysis* analyzer, SgProject* root);
  void optionallyRunInternalChecks(CodeThornOptions& ctOpt, int argc, char * argv[]);
  void optionallyRunInliner(CodeThornOptions& ctOpt, Normalization& normalization, SgProject* sageProject);
@@ -61,7 +61,7 @@ namespace CodeThorn {
  void optionallyGenerateCallGraphDotFile(CodeThornOptions& ctOpt,CTAnalysis* analyzer);
 
  SgProject* runRoseFrontEnd(int argc, char * argv[], CodeThornOptions& ctOpt, TimingCollector& timingCollector);
- SgProject* runRoseFrontEnd(vector<string>& argvList, CodeThornOptions& ctOpt, TimingCollector& timingCollector);
+ SgProject* runRoseFrontEnd(std::vector<std::string>& argvList, CodeThornOptions& ctOpt, TimingCollector& timingCollector);
  void normalizationPass(CodeThornOptions& ctOpt, SgProject* sageProject);
  Labeler* createLabeler(SgProject* sageProject, VariableIdMappingExtended* variableIdMapping, bool withCplusplus = false);
  VariableIdMappingExtended* createVariableIdMapping(CodeThornOptions& ctOpt, SgProject* sageProject);

diff --git a/tools/CodeThorn/src/CodeThornPasses.C b/tools/CodeThorn/src/CodeThornPasses.C
@@ -2,6 +2,9 @@
 #include "sage3basic.h"
 #include "CodeThornPasses.h"
 #include <iostream>
+
+using namespace std;
+using namespace CodeThorn;
 using namespace CodeThorn::CodeThornLib;
 
 namespace CodeThorn {

diff --git a/tools/CodeThorn/src/ConstantConditionAnalysis.C b/tools/CodeThorn/src/ConstantConditionAnalysis.C
@@ -2,6 +2,8 @@
 #include "sage3basic.h"
 #include "ConstantConditionAnalysis.h"
 
+using namespace CodeThorn;
+
 void ConstantConditionAnalysis::trueFalseEdgeEvaluation(Edge edge, SingleEvalResult& evalResult , EStatePtr estate) {
  BoolLattice newVal;
  if(evalResult.isTrue())

diff --git a/tools/CodeThorn/src/ConstantConditionAnalysis.h b/tools/CodeThorn/src/ConstantConditionAnalysis.h
@@ -7,10 +7,10 @@
 #include "ReadWriteListener.h"
 #include "BoolLattice.h"
 
-class ConstantConditionAnalysis : public ReadWriteListener {
+class ConstantConditionAnalysis : public CodeThorn::ReadWriteListener {
  public:
- void trueFalseEdgeEvaluation(Edge edge, SingleEvalResult& evalResult , EStatePtr estate) override;
- typedef std::map <Label,BoolLattice> ConstConditionsMap;
+ void trueFalseEdgeEvaluation(CodeThorn::Edge edge, CodeThorn::SingleEvalResult& evalResult , CodeThorn::EStatePtr estate) override;
+ typedef std::map <CodeThorn::Label,CodeThorn::BoolLattice> ConstConditionsMap;
  ConstConditionsMap* getResultMapPtr();
  private:
  ConstConditionsMap constConditions;

diff --git a/tools/CodeThorn/src/ContNodeAttribute.h b/tools/CodeThorn/src/ContNodeAttribute.h
@@ -6,22 +6,14 @@
 #include"CTAnalysis.h"
 #include"Flow.h"
 
-using namespace std;
-
 enum BranchReturns {NO, MAYBE, YES};
 
-class ContNodeAttribute: public AstAttribute
-{
- public: 
- Label contLabel; 
- BranchReturns trueBranchReturns, falseBranchReturns;
- ContNodeAttribute(Label contLabel, BranchReturns trueBranchReturns, BranchReturns falseBranchReturns): contLabel(contLabel), trueBranchReturns(trueBranchReturns), falseBranchReturns(falseBranchReturns){} 
- virtual string toString();
-
-
+class ContNodeAttribute: public AstAttribute {
+public: 
+ CodeThorn::Label contLabel; 
+ BranchReturns trueBranchReturns, falseBranchReturns;
+ ContNodeAttribute(CodeThorn::Label contLabel, BranchReturns trueBranchReturns, BranchReturns falseBranchReturns): contLabel(contLabel), trueBranchReturns(trueBranchReturns), falseBranchReturns(falseBranchReturns){} 
+ virtual std::string toString();
 };
 
-
-
-
 #endif
diff --git a/tools/CodeThorn/src/CtxUnfoldedAnalysis.C b/tools/CodeThorn/src/CtxUnfoldedAnalysis.C
@@ -16,6 +16,7 @@
 #include "CtxAnalysis.h"
 #include "CtxReachabilityLattice.h"
 
+using namespace CodeThorn;
 
 namespace
 {

diff --git a/tools/CodeThorn/src/EState.C b/tools/CodeThorn/src/EState.C
@@ -1,4 +1,3 @@
-
 #include "sage3basic.h"
 #include "EState.h"