diff --git a/test/theta/cfa/Expected/counter.theta b/test/theta/cfa/Expected/counter.theta index 139f30b1..c7a36450 100644 --- a/test/theta/cfa/Expected/counter.theta +++ b/test/theta/cfa/Expected/counter.theta @@ -1,6 +1,6 @@ main process __gazer_main_process { var main_RET_VAL : int - var main_tmp : int + var main_call : int var main___gazer_error_field : int init loc loc0 final loc loc1 @@ -15,15 +15,15 @@ main process __gazer_main_process { } loc2 -> loc3 { - havoc main_tmp + havoc main_call } loc3 -> loc6 { - assume (not (1 <= main_tmp)) + assume (not (1 <= main_call)) } loc3 -> loc4 { - assume (not (not (1 <= main_tmp))) + assume (not (not (1 <= main_call))) } loc4 -> loc5 { @@ -44,4 +44,4 @@ main process __gazer_main_process { main___gazer_error_field := 2 } -} +} \ No newline at end of file diff --git a/test/theta/cfa/Output/counter.c.tmp b/test/theta/cfa/Output/counter.c.tmp deleted file mode 100644 index 139f30b1..00000000 --- a/test/theta/cfa/Output/counter.c.tmp +++ /dev/null @@ -1,47 +0,0 @@ -main process __gazer_main_process { - var main_RET_VAL : int - var main_tmp : int - var main___gazer_error_field : int - init loc loc0 - final loc loc1 - loc loc2 - loc loc3 - loc loc4 - loc loc5 - loc loc6 - loc loc7 - error loc loc8 - loc0 -> loc2 { - } - - loc2 -> loc3 { - havoc main_tmp - } - - loc3 -> loc6 { - assume (not (1 <= main_tmp)) - } - - loc3 -> loc4 { - assume (not (not (1 <= main_tmp))) - } - - loc4 -> loc5 { - } - - loc5 -> loc1 { - main_RET_VAL := 0 - } - - loc6 -> loc7 { - } - - loc7 -> loc1 { - assume false - } - - loc7 -> loc8 { - main___gazer_error_field := 2 - } - -} diff --git a/tools/gazer-theta/CMakeLists.txt b/tools/gazer-theta/CMakeLists.txt index c88d2b04..53206a42 100644 --- a/tools/gazer-theta/CMakeLists.txt +++ b/tools/gazer-theta/CMakeLists.txt @@ -2,7 +2,9 @@ set(LIB_SOURCE_FILES lib/ThetaCfaGenerator.cpp lib/ThetaExpr.cpp lib/ThetaVerifier.cpp - lib/ThetaCfaWriterPass.cpp) + lib/ThetaCfaWriterPass.cpp + lib/ThetaCfaProcedureGenerator.cpp + lib/ThetaCommon.cpp) set(TOOL_SOURCE_FILES gazer-theta.cpp diff --git a/tools/gazer-theta/lib/ThetaCfaGenerator.cpp b/tools/gazer-theta/lib/ThetaCfaGenerator.cpp index e18d6ec6..8b3fe1a1 100644 --- a/tools/gazer-theta/lib/ThetaCfaGenerator.cpp +++ b/tools/gazer-theta/lib/ThetaCfaGenerator.cpp @@ -15,354 +15,29 @@ // limitations under the License. // //===----------------------------------------------------------------------===// -#include "ThetaCfaGenerator.h" -#include "gazer/Core/LiteralExpr.h" -#include "gazer/Automaton/CfaTransforms.h" -#include -#include - -#include -#include - -#include -#include -#include +#include "ThetaCfaProcedureGenerator.h" +#include "ThetaCommon.h" using namespace gazer; using namespace gazer::theta; using llvm::dyn_cast; -namespace -{ - -constexpr std::array ThetaKeywords = { - "main", "process", "var", "loc", - "assume", "init", "final", "error", - "return", "havoc", "bool", "int", "rat", - "if", "then", "else", "iff", "imply", - "forall", "exists", "or", "and", "not", - "mod", "rem", "true", "false" -}; - -struct ThetaAst -{ - virtual void print(llvm::raw_ostream& os) const = 0; - - virtual ~ThetaAst() = default; -}; - -struct ThetaLocDecl : ThetaAst -{ - enum Flag - { - Loc_State, - Loc_Init, - Loc_Final, - Loc_Error, - }; - - ThetaLocDecl(std::string name, Flag flag = Loc_State) - : mName(name), mFlag(flag) - {} - - void print(llvm::raw_ostream& os) const override - { - switch (mFlag) { - case Loc_Init: os << "init "; break; - case Loc_Final: os << "final "; break; - case Loc_Error: os << "error "; break; - default: - break; - } - - os << "loc " << mName; - } - - std::string mName; - Flag mFlag; -}; - -struct ThetaStmt : ThetaAst -{ - using VariantTy = std::variant, std::string>; - - /* implicit */ ThetaStmt(VariantTy content) - : mContent(content) - {} - - static ThetaStmt Assume(ExprPtr expr) - { - assert(expr->getType().isBoolType()); - - return VariantTy{expr}; - } - - static ThetaStmt Assign(std::string variableName, ExprPtr value) - { - assert(!llvm::isa(value) - && "Cannot assign an undef value to a variable." - "Use ::Havoc() to represent a nondetermistic value assignment." - ); - - std::pair pair = { variableName, value }; - - return VariantTy{pair}; - } - - static ThetaStmt Havoc(std::string variable) - { - return VariantTy{variable}; - } - - void print(llvm::raw_ostream& os) const override; - - VariantTy mContent; -}; - -struct ThetaEdgeDecl : ThetaAst -{ - ThetaEdgeDecl(ThetaLocDecl& source, ThetaLocDecl& target, std::vector stmts) - : mSource(source), mTarget(target), mStmts(std::move(stmts)) - {} - - void print(llvm::raw_ostream& os) const override; - - ThetaLocDecl& mSource; - ThetaLocDecl& mTarget; - std::vector mStmts; -}; - -class ThetaVarDecl : ThetaAst -{ -public: - ThetaVarDecl(std::string name, std::string type) - : mName(name), mType(type) - {} - - llvm::StringRef getName() { return mName; } - - void print(llvm::raw_ostream& os) const override - { - os << "var " << mName << " : " << mType; - } - -private: - std::string mName; - std::string mType; -}; - -class PrintVisitor -{ - llvm::raw_ostream& mOS; - std::function mCanonizeName; - - void printExpr(const ExprPtr& expr) { - if (mCanonizeName == nullptr) { - mOS << theta::printThetaExpr(expr); - } else { - mOS << theta::printThetaExpr(expr, mCanonizeName); - } - } - -public: - PrintVisitor(llvm::raw_ostream& os, std::function canonizeName) - : mOS(os), mCanonizeName(canonizeName) - {} - - void operator()(const ExprPtr& expr) { - mOS << "assume "; - printExpr(expr); - } - - void operator()(const std::pair& assign) { - mOS << assign.first << " := "; - printExpr(assign.second); - } - - void operator()(const std::string& variable) { - mOS << "havoc " << variable; - } -}; - -} // end anonymous namespace - - -void ThetaStmt::print(llvm::raw_ostream& os) const -{ - PrintVisitor visitor(os, nullptr); - - std::visit(visitor, mContent); -} - -void ThetaEdgeDecl::print(llvm::raw_ostream& os) const -{ - os << mSource.mName << " -> " << mTarget.mName << " {\n"; - for (auto& stmt : mStmts) { - os << " "; - stmt.print(os); - os << "\n"; - } - os << "}\n"; -} - -static std::string typeName(Type& type) -{ - switch (type.getTypeID()) { - case Type::IntTypeID: - return "int"; - case Type::RealTypeID: - return "rat"; - case Type::BoolTypeID: - return "bool"; - case Type::ArrayTypeID: { - auto& arrTy = llvm::cast(type); - return "[" + typeName(arrTy.getIndexType()) + "] -> " + typeName(arrTy.getElementType()); - } - default: - llvm_unreachable("Types which are unsupported by theta should have been eliminated earlier!"); - } -} - void ThetaCfaGenerator::write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace) { - Cfa* main = mSystem.getMainAutomaton(); - auto recursiveToCyclicResult = TransformRecursiveToCyclic(main); - - nameTrace.errorLocation = recursiveToCyclicResult.errorLocation; - nameTrace.errorFieldVariable = recursiveToCyclicResult.errorFieldVariable; - nameTrace.inlinedLocations = std::move(recursiveToCyclicResult.inlinedLocations); - nameTrace.inlinedVariables = std::move(recursiveToCyclicResult.inlinedVariables); - - llvm::DenseMap> locs; - llvm::DenseMap> vars; - std::vector> edges; - // Create a closure to test variable names - auto isValidVarName = [&vars](const std::string& name) -> bool { - // The variable name should not be present in the variable list. - return std::find_if(vars.begin(), vars.end(), [name](auto& v1) { - return name == v1.second->getName(); - }) == vars.end(); + auto isValidVarName = [&nameTrace](const std::string& name) -> bool { + // The variable name should not be present in the variable list. + return std::find_if(nameTrace.variables.begin(), nameTrace.variables.end(), [name](auto& v1) { + return name == v1.second->getName(); + }) == nameTrace.variables.end(); }; - // Add variables - for (auto& variable : main->locals()) { - auto name = validName(variable.getName(), isValidVarName); - auto type = typeName(variable.getType()); - - nameTrace.variables[name] = &variable; - vars.try_emplace(&variable, std::make_unique(name, type)); - } - - for (auto& variable : main->inputs()) { - auto name = validName(variable.getName(), isValidVarName); - auto type = typeName(variable.getType()); - - nameTrace.variables[name] = &variable; - vars.try_emplace(&variable, std::make_unique(name, type)); - } - - // Add locations - for (Location* loc : main->nodes()) { - ThetaLocDecl::Flag flag = ThetaLocDecl::Loc_State; - if (loc == recursiveToCyclicResult.errorLocation) { - flag = ThetaLocDecl::Loc_Error; - } else if (main->getEntry() == loc) { - flag = ThetaLocDecl::Loc_Init; - } else if (main->getExit() == loc) { - flag = ThetaLocDecl::Loc_Final; - } - - auto locName = "loc" + std::to_string(loc->getId()); - - nameTrace.locations[locName] = loc; - locs.try_emplace(loc, std::make_unique(locName, flag)); - } - - // Add edges - for (Transition* edge : main->edges()) { - ThetaLocDecl& source = *locs[edge->getSource()]; - ThetaLocDecl& target = *locs[edge->getTarget()]; - - std::vector stmts; - - if (edge->getGuard() != BoolLiteralExpr::True(edge->getGuard()->getContext())) { - stmts.push_back(ThetaStmt::Assume(edge->getGuard())); - } - - if (auto assignEdge = dyn_cast(edge)) { - for (auto& assignment : *assignEdge) { - auto lhsName = vars[assignment.getVariable()]->getName(); - - if (llvm::isa(assignment.getValue())) { - stmts.push_back(ThetaStmt::Havoc(lhsName)); - } else { - stmts.push_back(ThetaStmt::Assign(lhsName, assignment.getValue())); - } - } - } else if (auto callEdge = dyn_cast(edge)) { - llvm_unreachable("CallTransitions are not supported in theta CFAs!"); - } - - edges.emplace_back(std::make_unique(source, target, std::move(stmts))); - } - - auto INDENT = " "; - auto INDENT2 = " "; - - auto canonizeName = [&vars](Variable* variable) -> std::string { - if (vars.count(variable) == 0) { - return variable->getName(); - } - - return vars[variable]->getName(); - }; + llvm::DenseMap> globalVars; os << "main process __gazer_main_process {\n"; - - for (auto& variable : llvm::concat(main->inputs(), main->locals())) { - os << INDENT; - vars[&variable]->print(os); - os << "\n"; - } - - for (Location* loc : main->nodes()) { - os << INDENT; - locs[loc]->print(os); - os << "\n"; - } - - for (auto& edge : edges) { - os << INDENT << edge->mSource.mName << " -> " << edge->mTarget.mName << " {\n"; - for (auto& stmt : edge->mStmts) { - os << INDENT2; - - PrintVisitor visitor(os, canonizeName); - std::visit(visitor, stmt.mContent); - os << "\n"; - } - os << INDENT << "}\n"; - os << "\n"; - } - - os << "}\n"; + ThetaCfaProcedureGenerator(mSystem.getMainAutomaton(), isValidVarName, globalVars).write(os, nameTrace); + os << "}"; os.flush(); } - -std::string ThetaCfaGenerator::validName(std::string name, std::function isUnique) -{ - name = std::regex_replace(name, std::regex("[^a-zA-Z0-9_]"), "_"); - - if (std::find(ThetaKeywords.begin(), ThetaKeywords.end(), name) != ThetaKeywords.end()) { - name += "_gazer"; - } - - while (!isUnique(name)) { - llvm::Twine nextTry = name + llvm::Twine(mTmpCount++); - name = nextTry.str(); - } - - return name; -} diff --git a/tools/gazer-theta/lib/ThetaCfaGenerator.h b/tools/gazer-theta/lib/ThetaCfaGenerator.h index 942d93d3..5ee2ea66 100644 --- a/tools/gazer-theta/lib/ThetaCfaGenerator.h +++ b/tools/gazer-theta/lib/ThetaCfaGenerator.h @@ -31,10 +31,6 @@ namespace llvm namespace gazer::theta { -std::string printThetaExpr(const ExprPtr& expr); - -std::string printThetaExpr(const ExprPtr& expr, std::function variableNames); - /// \brief Perform pre-processing steps required by theta on the input CFA. /// /// This pass does the following transformations: @@ -61,13 +57,9 @@ class ThetaCfaGenerator void write(llvm::raw_ostream& os, ThetaNameMapping& names); -private: - std::string validName(std::string name, std::function isUnique); - private: AutomataSystem& mSystem; CallGraph mCallGraph; - unsigned mTmpCount = 0; }; llvm::Pass* createThetaCfaWriterPass(llvm::raw_ostream& os); diff --git a/tools/gazer-theta/lib/ThetaCfaProcedureGenerator.cpp b/tools/gazer-theta/lib/ThetaCfaProcedureGenerator.cpp new file mode 100644 index 00000000..8f60d365 --- /dev/null +++ b/tools/gazer-theta/lib/ThetaCfaProcedureGenerator.cpp @@ -0,0 +1,155 @@ +//==-------------------------------------------------------------*- C++ -*--==// +// +// Copyright 2020 Contributors to the Gazer project +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// +//===----------------------------------------------------------------------===// +#include "ThetaCfaProcedureGenerator.h" +#include "ThetaCommon.h" + +#include "gazer/Automaton/CfaTransforms.h" + +#include +#include + +#include + +using namespace gazer::theta; +using namespace llvm; + +void ThetaCfaProcedureGenerator::write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace) { + auto recursiveToCyclicResult = TransformRecursiveToCyclic(mCfa); + + nameTrace.errorLocation = recursiveToCyclicResult.errorLocation; + nameTrace.errorFieldVariable = recursiveToCyclicResult.errorFieldVariable; + nameTrace.inlinedLocations = std::move(recursiveToCyclicResult.inlinedLocations); + nameTrace.inlinedVariables = std::move(recursiveToCyclicResult.inlinedVariables); + + llvm::DenseMap> locs; + llvm::DenseMap> vars; + std::vector> edges; + + // Add variables + for (auto& variable : mCfa->locals()) { + auto name = validName(variable.getName(), isValidVarName); + auto type = typeName(variable.getType()); + + nameTrace.variables[name] = &variable; + vars.try_emplace(&variable, std::make_unique(name, type)); + } + + for (auto& variable : mCfa->inputs()) { + auto name = validName(variable.getName(), isValidVarName); + auto type = typeName(variable.getType()); + + nameTrace.variables[name] = &variable; + vars.try_emplace(&variable, std::make_unique(name, type)); + } + + // Add locations + for (Location* loc : mCfa->nodes()) { + ThetaLocDecl::Flag flag = ThetaLocDecl::Loc_State; + if (loc == recursiveToCyclicResult.errorLocation) { + flag = ThetaLocDecl::Loc_Error; + } else if (mCfa->getEntry() == loc) { + flag = ThetaLocDecl::Loc_Init; + } else if (mCfa->getExit() == loc) { + flag = ThetaLocDecl::Loc_Final; + } + + auto locName = "loc" + std::to_string(loc->getId()); + + nameTrace.locations[locName] = loc; + locs.try_emplace(loc, std::make_unique(locName, flag)); + } + + // Add edges + for (Transition* edge : mCfa->edges()) { + ThetaLocDecl& source = *locs[edge->getSource()]; + ThetaLocDecl& target = *locs[edge->getTarget()]; + + std::vector stmts; + + if (edge->getGuard() != BoolLiteralExpr::True(edge->getGuard()->getContext())) { + stmts.push_back(ThetaStmt::Assume(edge->getGuard())); + } + + if (auto assignEdge = dyn_cast(edge)) { + for (auto& assignment : *assignEdge) { + auto lhsName = vars[assignment.getVariable()]->getName(); + + if (llvm::isa(assignment.getValue())) { + stmts.push_back(ThetaStmt::Havoc(lhsName)); + } else { + stmts.push_back(ThetaStmt::Assign(lhsName, assignment.getValue())); + } + } + } else if (auto* callEdge = dyn_cast(edge)) { + ThetaStmt::CallData data; + assert(callEdge->getNumOutputs() <= 1 && "Only one output is supported for calls"); + data.functionName = callEdge->getCalledAutomaton()->getName(); // TODO mangling? + for (const auto& input : callEdge->inputs()) { + auto param = vars[input.getVariable()]->getName(); + data.parameters.push_back(param); + } + if (callEdge->getNumOutputs() == 1) { + auto output = vars[callEdge->output_begin()->getVariable()]->getName(); + data.resultVar = output; + } else { + data.resultVar = ""; + } + + stmts.push_back(ThetaStmt::Call(data)); + } + + edges.emplace_back(std::make_unique(source, target, std::move(stmts))); + } + + auto INDENT = " "; + auto INDENT2 = " "; + + auto canonizeName = [&vars](Variable* variable) -> std::string { + if (vars.count(variable) == 0) { + return variable->getName(); + } + + return vars[variable]->getName(); + }; + + for (auto& variable : llvm::concat(mCfa->inputs(), mCfa->locals())) { + os << INDENT; + vars[&variable]->print(os); + os << "\n"; + } + + for (Location* loc : mCfa->nodes()) { + os << INDENT; + locs[loc]->print(os); + os << "\n"; + } + + for (auto& edge : edges) { + os << INDENT << edge->mSource.mName << " -> " << edge->mTarget.mName << " {\n"; + for (auto& stmt : edge->mStmts) { + os << INDENT2; + + PrintVisitor visitor(os, canonizeName); + std::visit(visitor, stmt.mContent); + os << "\n"; + } + os << INDENT << "}\n"; + os << "\n"; + } +} + diff --git a/tools/gazer-theta/lib/ThetaCfaProcedureGenerator.h b/tools/gazer-theta/lib/ThetaCfaProcedureGenerator.h new file mode 100644 index 00000000..fb019846 --- /dev/null +++ b/tools/gazer-theta/lib/ThetaCfaProcedureGenerator.h @@ -0,0 +1,47 @@ +//==-------------------------------------------------------------*- C++ -*--==// +// +// Copyright 2020 Contributors to the Gazer project +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// +//===----------------------------------------------------------------------===// +#ifndef GAZER_THETACFAPROCEDUREGENERATOR_H +#define GAZER_THETACFAPROCEDUREGENERATOR_H + +#include "gazer/Automaton/Cfa.h" +#include "ThetaCfaGenerator.h" +#include "ThetaCommon.h" + +using namespace gazer; + +namespace gazer::theta { + +class ThetaCfaProcedureGenerator +{ +public: + ThetaCfaProcedureGenerator(Cfa* cfa, std::function isValidVarName, + llvm::DenseMap>& globals) + : mCfa(cfa), isValidVarName(isValidVarName), globals(globals) + {} + + void write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace); + +private: + Cfa* mCfa; + llvm::DenseMap>& globals; + std::function isValidVarName; +}; + +} // namespace gazer::theta + +#endif // GAZER_THETACFAPROCEDUREGENERATOR_H diff --git a/tools/gazer-theta/lib/ThetaCommon.cpp b/tools/gazer-theta/lib/ThetaCommon.cpp new file mode 100644 index 00000000..dcde6390 --- /dev/null +++ b/tools/gazer-theta/lib/ThetaCommon.cpp @@ -0,0 +1,86 @@ +//==-------------------------------------------------------------*- C++ -*--==// +// +// Copyright 2020 Contributors to the Gazer project +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// +//===----------------------------------------------------------------------===// + +#include "ThetaCommon.h" + +namespace { + +constexpr std::array ThetaKeywords = { + "main", "process", "var", "loc", + "assume", "init", "final", "error", + "return", "havoc", "bool", "int", "rat", + "if", "then", "else", "iff", "imply", + "forall", "exists", "or", "and", "not", + "mod", "rem", "true", "false" +}; + +int tmpCount = 0; + +} // namespace + +std::string gazer::theta::validName(std::string name, std::function isUnique) { + name = std::regex_replace(name, std::regex("[^a-zA-Z0-9_]"), "_"); + + if (std::find(ThetaKeywords.begin(), ThetaKeywords.end(), name) != ThetaKeywords.end()) { + name += "_gazer"; + } + + while (!isUnique(name)) { + llvm::Twine nextTry = name + llvm::Twine(tmpCount++); + name = nextTry.str(); + } + + return name; +} + +void gazer::theta::ThetaStmt::print(llvm::raw_ostream& os) const +{ + PrintVisitor visitor(os, nullptr); + + std::visit(visitor, mContent); +} + +void gazer::theta::ThetaEdgeDecl::print(llvm::raw_ostream& os) const +{ + os << mSource.mName << " -> " << mTarget.mName << " {\n"; + for (auto& stmt : mStmts) { + os << " "; + stmt.print(os); + os << "\n"; + } + os << "}\n"; +} + +std::string gazer::theta::typeName(Type& type) +{ + switch (type.getTypeID()) { + case Type::IntTypeID: + return "int"; + case Type::RealTypeID: + return "rat"; + case Type::BoolTypeID: + return "bool"; + case Type::ArrayTypeID: { + auto& arrTy = llvm::cast(type); + return "[" + typeName(arrTy.getIndexType()) + "] -> " + typeName(arrTy.getElementType()); + } + default: + llvm_unreachable("Types which are unsupported by theta should have been eliminated earlier!"); + } +} + diff --git a/tools/gazer-theta/lib/ThetaCommon.h b/tools/gazer-theta/lib/ThetaCommon.h new file mode 100644 index 00000000..5044534c --- /dev/null +++ b/tools/gazer-theta/lib/ThetaCommon.h @@ -0,0 +1,206 @@ +//==-------------------------------------------------------------*- C++ -*--==// +// +// Copyright 2020 Contributors to the Gazer project +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// +//===----------------------------------------------------------------------===// +#ifndef GAZER_THETACOMMON_H +#define GAZER_THETACOMMON_H + +#include "gazer/Core/LiteralExpr.h" + +#include + +#include +#include + +namespace gazer::theta { + +std::string printThetaExpr(const ExprPtr& expr); + +std::string printThetaExpr(const ExprPtr& expr, std::function variableNames); + +std::string validName(std::string name, std::function isUnique); + +std::string typeName(Type& type); + +struct ThetaAst +{ + virtual void print(llvm::raw_ostream& os) const = 0; + + virtual ~ThetaAst() = default; +}; + +struct ThetaLocDecl : ThetaAst +{ + enum Flag + { + Loc_State, + Loc_Init, + Loc_Final, + Loc_Error, + }; + + ThetaLocDecl(std::string name, Flag flag = Loc_State) + : mName(name), mFlag(flag) + {} + + void print(llvm::raw_ostream& os) const override + { + switch (mFlag) { + case Loc_Init: os << "init "; break; + case Loc_Final: os << "final "; break; + case Loc_Error: os << "error "; break; + default: + break; + } + + os << "loc " << mName; + } + + std::string mName; + Flag mFlag; +}; + +struct ThetaStmt : ThetaAst +{ + struct CallData { + std::string resultVar; + std::string functionName; + std::vector parameters; + }; + using VariantTy = std::variant, std::string, CallData>; + + /* implicit */ ThetaStmt(VariantTy content) + : mContent(content) + {} + + static ThetaStmt Assume(ExprPtr expr) + { + assert(expr->getType().isBoolType()); + + return VariantTy{expr}; + } + + static ThetaStmt Assign(std::string variableName, ExprPtr value) + { + assert(!llvm::isa(value) + && "Cannot assign an undef value to a variable." + "Use ::Havoc() to represent a nondetermistic value assignment." + ); + + std::pair pair = { variableName, value }; + + return VariantTy{pair}; + } + + static ThetaStmt Havoc(std::string variable) + { + return VariantTy{variable}; + } + + static ThetaStmt Call(CallData callData) + { + return VariantTy{callData}; + } + + void print(llvm::raw_ostream& os) const override; + + VariantTy mContent; +}; + +struct ThetaEdgeDecl : ThetaAst +{ + ThetaEdgeDecl(ThetaLocDecl& source, ThetaLocDecl& target, std::vector stmts) + : mSource(source), mTarget(target), mStmts(std::move(stmts)) + {} + + void print(llvm::raw_ostream& os) const override; + + ThetaLocDecl& mSource; + ThetaLocDecl& mTarget; + std::vector mStmts; +}; + +class ThetaVarDecl : ThetaAst +{ +public: + ThetaVarDecl(std::string name, std::string type) + : mName(name), mType(type) + {} + + llvm::StringRef getName() { return mName; } + + void print(llvm::raw_ostream& os) const override + { + os << "var " << mName << " : " << mType; + } + +private: + std::string mName; + std::string mType; +}; + +class PrintVisitor +{ + llvm::raw_ostream& mOS; + std::function mCanonizeName; + + void printExpr(const ExprPtr& expr) { + if (mCanonizeName == nullptr) { + mOS << printThetaExpr(expr); + } else { + mOS << printThetaExpr(expr, mCanonizeName); + } + } + +public: + PrintVisitor(llvm::raw_ostream& os, std::function canonizeName) + : mOS(os), mCanonizeName(canonizeName) + {} + + void operator()(const ExprPtr& expr) { + mOS << "assume "; + printExpr(expr); + } + + void operator()(const std::pair& assign) { + mOS << assign.first << " := "; + printExpr(assign.second); + } + + void operator()(const std::string& variable) { + mOS << "havoc " << variable; + } + + void operator()(const ThetaStmt::CallData& function) { + if (function.resultVar != "") { + mOS << function.resultVar << " "; + } + mOS << "call " << function.functionName << "("; + bool first = true; + for (const std::string& param : function.parameters) { + if (!first) { + mOS << ", "; + } else { + first = false; + } + mOS << param; + } + } +}; + +} // namespace gazer::theta + +#endif // GAZER_THETACOMMON_H diff --git a/tools/gazer-theta/lib/ThetaExpr.cpp b/tools/gazer-theta/lib/ThetaExpr.cpp index d12b4bcf..df217bc2 100644 --- a/tools/gazer-theta/lib/ThetaExpr.cpp +++ b/tools/gazer-theta/lib/ThetaExpr.cpp @@ -15,7 +15,8 @@ // limitations under the License. // //===----------------------------------------------------------------------===// -#include "ThetaCfaGenerator.h" +#include "ThetaCommon.h" + #include "gazer/Core/Expr/ExprWalker.h" #include "gazer/ADT/StringUtils.h" diff --git a/unittest/tools/gazer-theta/ThetaExprPrinterTest.cpp b/unittest/tools/gazer-theta/ThetaExprPrinterTest.cpp index f98234a5..e6484574 100644 --- a/unittest/tools/gazer-theta/ThetaExprPrinterTest.cpp +++ b/unittest/tools/gazer-theta/ThetaExprPrinterTest.cpp @@ -15,7 +15,7 @@ // limitations under the License. // //===----------------------------------------------------------------------===// -#include "../../../tools/gazer-theta/lib/ThetaCfaGenerator.h" +#include "../../../tools/gazer-theta/lib/ThetaCommon.h" #include "gazer/Core/Expr/ExprBuilder.h"