Skip to content

Commit

Permalink
Merge pull request #33 from sillydan1/patch/bug-hunting
Browse files Browse the repository at this point in the history 
Patch/bug hunting
  • Loading branch information
@sillydan1
sillydan1 authored Mar 13, 2022
2 parents a791f06 + a2d6d4a commit b23b920
Show file tree
Hide file tree
Showing 10 changed files with 504 additions and 75 deletions.
96 changes: 61 additions & 35 deletions src/runtime/TTA.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,34 @@ TTA operator<<(const TTA& aa, const TTA::StateChange& b) {
return a;
}

#define FUNC_IMPL(a, func, b, res) std::visit(overload{[&b,&res](auto&& x){std::visit(overload{[&x,&res](auto&& y){res = func(x,y);}}, static_cast<TTASymbol_t>(b));}}, static_cast<TTASymbol_t>(a))
template<typename T1, typename T2>
auto t_ee(const T1&, const T2&) {
return false;
}
auto t_ee(const bool& a, const bool& b) {return a == b;}
auto t_ee(const int& a, const int& b) {return a == b;}
auto t_ee(const long& a, const long& b) {return a == b;}
auto t_ee(const int& a, const long& b) {return a == b;}
auto t_ee(const long& a, const int& b) {return a == b;}
auto t_ee(const int& a, const float& b) {return a == b;}
auto t_ee(const long& a, const float& b) {return a == b;}
auto t_ee(const float& a, const int& b) {return a == b;}
auto t_ee(const float& a, const long& b) {return a == b;}
auto t_ee(const float& a, const float& b) {return a == b;}
auto t_ee(const TTATimerSymbol& a, const TTATimerSymbol& b) {return a.current_value == b.current_value;}
auto t_ee(const std::string& a, const std::string& b) {return a == b;}
bool operator==(const TTASymbol_t& a, const TTASymbol_t& b) {
bool retVal = a.index() == b.index();
if(!retVal)
return false;
FUNC_IMPL(a, t_ee, b, retVal);
return retVal;
}
bool operator!=(const TTASymbol_t& a, const TTASymbol_t& b) {
return !(a == b);
}

TTASymbol_t TTASymbolValueFromTypeAndValueStrings(const std::string& typestr, const std::string& valuestr) {
return PopulateValueFromString(TTASymbolTypeFromString(typestr), valuestr);
}
Expand Down Expand Up @@ -178,6 +206,8 @@ std::optional<StateMultiChoice> TTA::GetChangesFromEdge(const TTA::Edge& choice,
changes.component = currentComponent;
bool DoesUpdateInfluenceOverlap = AccumulateUpdateInfluences(choice, changes.symbolsToChange, overlappingComponents, currentComponent);
outInfluenceOverlap |= DoesUpdateInfluenceOverlap;
if(DoesUpdateInfluenceOverlap)
return {};

for(auto& symbolChange : changes.symbolsToChange)
changes.symbolChanges.push_back(symbolChange.second);
Expand All @@ -186,13 +216,23 @@ std::optional<StateMultiChoice> TTA::GetChangesFromEdge(const TTA::Edge& choice,
}

void TTA::WarnAboutComponentOverlap(component_overlap_t& overlappingComponents) const {
spdlog::debug("Overlapping Components: (Tick#: {0})", tickCount);
for (auto& componentCollection : overlappingComponents) {
if (componentCollection.second.updates.size() > 1) {
for (auto& compname : componentCollection.second.updates)
spdlog::debug("{0}", compname.first);
}
std::vector<std::string> overlapping_errors{};
for(auto it = overlappingComponents.begin(), end = overlappingComponents.end(); it != end; it = overlappingComponents.equal_range(it->first).second) {
auto iter = overlappingComponents.equal_range(it->first);
const std::string& compName = iter.first->second.componentName;
for(auto& x = iter.first; x != iter.second; x++) {
if(x->second.componentName != compName) {
overlapping_errors.emplace_back(x->second.componentName + " and " + compName + " disagree on: " + it->first);
break;
}
}
}
if(overlapping_errors.empty())
return;

spdlog::trace("Overlapping Updates:");
for(auto& err : overlapping_errors)
spdlog::trace(err);
}

TokenMap TTA::GetSymbolChangesAsMap(std::vector<UpdateExpression> &symbolChanges) const {
Expand Down Expand Up @@ -226,29 +266,11 @@ std::vector<TTA::StateChange> TTA::GetNextTickStates(const nondeterminism_strate
auto enabledEdges = component.second.GetEnabledEdges(symbols); // TODO: Take Interesting variables into account
if(!enabledEdges.empty()) {
bool hasNondeterminism = WarnIfNondeterminism(enabledEdges, component.first);
if(!hasNondeterminism) {
// Simply pick the edge and apply it to the shared changes
if(strategy != nondeterminism_strategy_t::VERIFICATION) {
auto &pickedEdge = PickEdge(enabledEdges, strategy);
auto changes = GetChangesFromEdge(pickedEdge, updateInfluenceOverlapGlobal, overlappingComponents, component.first);
if (changes.has_value()) sharedChanges.Merge(changes.value());
ApplyComponentLocation(sharedChanges.currentLocations, component, pickedEdge);
} else {
for(auto& edge : enabledEdges) {
auto changes = GetChangesFromEdge(edge, updateInfluenceOverlapGlobal, overlappingComponents, component.first);
if(changes.has_value()) {
sharedChanges.Merge(changes.value());
ApplyComponentLocation(sharedChanges.currentLocations, component, edge);
}
}
}
} else {
for(auto& edge : enabledEdges) {
auto changes = GetChangesFromEdge(edge, updateInfluenceOverlapGlobal, overlappingComponents, component.first);
if(changes.has_value()) {
ApplyComponentLocation(changes->currentLocations, component, edge);
choiceChanges.push_back(changes.value());
}
for(auto& edge : enabledEdges) {
auto changes = GetChangesFromEdge(edge, updateInfluenceOverlapGlobal, overlappingComponents, component.first);
if(changes.has_value()) {
ApplyComponentLocation(changes->currentLocations, component, edge);
choiceChanges.push_back(changes.value());
}
}
}
Expand Down Expand Up @@ -281,8 +303,10 @@ bool TTA::WarnIfNondeterminism(const std::vector<Edge>& edges, const std::string

std::string TTA::GetCurrentStateString() const {
std::stringstream ss{}; ss << "{";
for(auto& component : components) ss<<"\""<<component.first<<"\""<<": "<<"\""<<component.second.currentLocation.identifier<<"\",";
for(auto& symbol : symbols.map()) ss<<"\""<<symbol.first<<"\""<<": "<<"\""<<symbol.second.str()<<"\",";
for(auto& component : components)
ss<<"\""<<component.first<<"\""<<": "<<"\""<<component.second.currentLocation.identifier<<"\",";
for(auto& symbol : symbols.map())
ss<<"\""<<symbol.first<<"\""<<": "<<"\""<<symbol.second.str()<<"\",";
ss << R"("OBJECT_END":"true"})"; // This is just a bad way of ending a json object.
return ss.str();
}
Expand Down Expand Up @@ -385,21 +409,21 @@ bool AreRightHandSidesIndempotent(const std::map<std::string, std::vector<std::p
bool TTA::AccumulateUpdateInfluences(const TTA::Edge& pickedEdge, std::multimap<std::string, UpdateExpression>& symbolsToChange, component_overlap_t& overlappingComponents, const std::string& currentComponent) const {
bool updateInfluenceOverlap = false;
for(auto& expr : pickedEdge.updateExpressions) {
bool overlap_in_this_expr = false;
auto it = overlappingComponents.find(expr.lhs);
if(it != overlappingComponents.end()) {
auto range = overlappingComponents.equal_range(expr.lhs);
for(auto iter = range.first; iter != range.second; iter++) {
if(iter->second.componentName == currentComponent) {
symbolsToChange.insert({ expr.lhs, expr });
if(iter->second.componentName == currentComponent)
continue;
}
// TODO: Check for Indempotence!
// TODO: Check for Idempotence!
spdlog::debug("Overlapping update influence on evaluation of update on edge {0} --> {1}. "
"Variable '{2}' is already being written to in this tick! - For more info, run with higher verbosity",
TTAResugarizer::Resugar(pickedEdge.sourceLocation.identifier),
TTAResugarizer::Resugar(pickedEdge.targetLocation.identifier),
TTAResugarizer::Resugar(expr.lhs)); // TODO: Idempotent variable assignment
updateInfluenceOverlap = true;
overlap_in_this_expr = true;
}
}
component_overlap c{
Expand All @@ -410,6 +434,8 @@ bool TTA::AccumulateUpdateInfluences(const TTA::Edge& pickedEdge, std::multimap<
pickedEdge.targetLocation.identifier), expr.rhs)}
};
overlappingComponents.emplace(expr.lhs, std::move(c));
if(overlap_in_this_expr)
continue;
symbolsToChange.insert({ expr.lhs, expr });
}
return updateInfluenceOverlap;
Expand Down
5 changes: 5 additions & 0 deletions src/runtime/TTA.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,12 @@ struct TTA {

std::vector<Edge> GetEnabledEdges(const SymbolMap& symbolMap) const;
};

#ifndef NDEBUG
using ComponentMap = std::map<std::string, Component>;
#else
using ComponentMap = std::unordered_map<std::string, Component>;
#endif
using ComponentLocationMap = std::unordered_map<std::string, Location>;
struct StateChange {
ComponentLocationMap componentLocations;
Expand Down
4 changes: 4 additions & 0 deletions src/runtime/TTASymbol.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@
#ifndef AALTITOAD_TTASYMBOL_H
#define AALTITOAD_TTASYMBOL_H
#include <aaltitoadpch.h>
#include "extensions/overload"

struct TTATimerSymbol {
float current_value;
Expand All @@ -39,6 +40,9 @@ using TTASymbol_t = std::variant<
std::string
>;

bool operator==(const TTASymbol_t&, const TTASymbol_t&);
bool operator!=(const TTASymbol_t&, const TTASymbol_t&);

TTASymbol_t TTASymbolValueFromTypeAndValueStrings(const std::string& typestr, const std::string& valuestr);
TTASymbol_t TTASymbolTypeFromString(const std::string& typestr);
TTASymbol_t PopulateValueFromString(const TTASymbol_t& type, const std::string& valuestr);
Expand Down
89 changes: 63 additions & 26 deletions src/verifier/ReachabilitySearcher.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,13 +39,11 @@ bool IsQuerySatisfiedHelper(const Query& query, const TTA& state) {
case NodeType_t::CompEq:
case NodeType_t::CompGreater:
case NodeType_t::CompGreaterEq: {
std::string exprstring{}; // This string can technically be precompiled.
query.children[0].tree_apply([&exprstring]( const ASTNode& node ){ exprstring += node.token; });
exprstring += query.root.token;
query.children[1].tree_apply([&exprstring]( const ASTNode& node ){ exprstring += node.token; });
spdlog::debug("Assembled expression '{0}'", exprstring);
calculator c(exprstring.c_str());
return c.eval(state.GetSymbols()).asBool();
std::stringstream exprstring{}; // This string can technically be precompiled.
query.children[0].tree_apply([&exprstring]( const ASTNode& node ){ exprstring << node.token; });
exprstring << query.root.token;
query.children[1].tree_apply([&exprstring]( const ASTNode& node ){ exprstring << node.token; });
return calculator(exprstring.str().c_str()).eval(state.GetSymbols()).asBool();
}
case NodeType_t::SubExpr:
case NodeType_t::Finally:
Expand All @@ -66,9 +64,7 @@ bool IsQuerySatisfiedHelper(const Query& query, const TTA& state) {

bool ReachabilitySearcher::IsQuerySatisfied(const Query& query, const TTA &state) {
if(query.root.type == NodeType_t::Forall && query.children.begin()->root.type == NodeType_t::Globally) {
auto invertedQ = Query(ASTNode{NodeType_t::Negation, "!"});
invertedQ.insert(query);
return IsQuerySatisfiedHelper(invertedQ, state);
return !IsQuerySatisfiedHelper(query, state);
}
if(query.root.type != NodeType_t::Exists) {
spdlog::critical("Only reachability queries are supported right now, sorry.");
Expand Down Expand Up @@ -96,17 +92,22 @@ void ReachabilitySearcher::OutputResults(const std::vector<QueryResultPair>& res
if(CLIConfig::getInstance()["output"]) {
std::ofstream outputFile{CLIConfig::getInstance()["output"].as_string(), std::ofstream::trunc};
for(auto& r : results) {
outputFile << ConvertASTToString(*r.query) << " : " << std::boolalpha << r.answer << "\n";
auto answer = r.query->root.type == NodeType_t::Forall && r.query->children[0].root.type == NodeType_t::Globally ? !r.answer : r.answer;
outputFile << ConvertASTToString(*r.query) << " : " << std::boolalpha << answer << "\n";
}
}
}

void ReachabilitySearcher::PrintResults(const std::vector<QueryResultPair>& results) {
auto ReachabilitySearcher::PrintResults(const std::vector<QueryResultPair>& results) -> int {
OutputResults(results);
auto acceptedResults = 0;
spdlog::info("==== QUERY RESULTS ====");
for(const auto& r : results) {
spdlog::info("===================="); // Delimiter to make it easier to read
spdlog::info("{0} : {1}", ConvertASTToString(*r.query), r.answer);
auto answer = r.query->root.type == NodeType_t::Forall && r.query->children[0].root.type == NodeType_t::Globally ? !r.answer : r.answer;
if(answer)
acceptedResults++;
spdlog::info("{0} : {1}", ConvertASTToString(*r.query), answer);
auto stateHash = r.acceptingStateHash;
auto state = r.acceptingState;
std::vector<std::string> trace{};
Expand Down Expand Up @@ -135,13 +136,18 @@ void ReachabilitySearcher::PrintResults(const std::vector<QueryResultPair>& resu
break;
}
}
if(trace.empty()) {
spdlog::info("No trace available");
continue;
}
spdlog::info("Trace:");
std::reverse(trace.begin(), trace.end());
printf("[");
printf("[\n");
for(auto& stateStr : trace)
printf("%s,\n", stateStr.c_str());
printf("]\n");
}
return acceptedResults;
}

auto debug_int_as_hex_str(size_t v) {
Expand All @@ -150,17 +156,32 @@ auto debug_int_as_hex_str(size_t v) {
return std::string(buffer);
}

std::string debug_get_current_state_string_human(const TTA& tta) {
std::stringstream ss{};
for(auto& c : tta.components)
ss << c.second.currentLocation.identifier << ", ";
return ss.str();
}

void debug_print_passed_list(const ReachabilitySearcher& r) {
spdlog::trace("==== PASSED LIST ====");
for(auto& e : r.Passed) {
spdlog::trace("Hash:{0} Prev:{1}",
if(e.first == e.second.prevStateHash) {
spdlog::warn("Hash:{0} Prev:{1} \tState:{2}",
debug_int_as_hex_str(e.first),
debug_int_as_hex_str(e.second.prevStateHash),
debug_get_current_state_string_human(e.second.tta));
continue;
}
spdlog::trace("Hash:{0} Prev:{1} \tState:{2}",
debug_int_as_hex_str(e.first),
debug_int_as_hex_str(e.second.prevStateHash));
debug_int_as_hex_str(e.second.prevStateHash),
debug_get_current_state_string_human(e.second.tta));
}
spdlog::trace("====/PASSED LIST ====");
}

void debug_cleanup_waiting_list(ReachabilitySearcher& s, size_t curstatehash, const SearchState& state) {
void cleanup_waiting_list(ReachabilitySearcher& s, size_t curstatehash, const SearchState& state) {
bool found;
do {
found = false;
Expand All @@ -175,6 +196,13 @@ void debug_cleanup_waiting_list(ReachabilitySearcher& s, size_t curstatehash, co
} while(found);
}

std::string debug_get_symbol_map_string_representation(const TTA::SymbolMap& map) {
std::ostringstream ss{};
for(auto& symbol : map.map())
ss << symbol.first << " :-> " << symbol.second << ", ";
return ss.str();
}

bool ReachabilitySearcher::ForwardReachabilitySearch(const nondeterminism_strategy_t& strategy) {
auto stateit = Waiting.begin();
while(stateit != Waiting.end()) {
Expand All @@ -183,9 +211,11 @@ bool ReachabilitySearcher::ForwardReachabilitySearch(const nondeterminism_strate
AreQueriesSatisfied(query_results, state.tta, curstatehash);
if(AreQueriesAnswered(query_results)) {
Passed.emplace(std::make_pair(curstatehash, state));
if(!CLIConfig::getInstance()["notrace"])
PrintResults(query_results);
if(CLIConfig::getInstance()["verbosity"] && CLIConfig::getInstance()["verbosity"].as_integer() >= 6)
debug_print_passed_list(*this);
spdlog::info("Found a positive result after searching: {0} states", Passed.size());
if(!CLIConfig::getInstance()["notrace"])
return query_results.size() - PrintResults(query_results) == 0;
return true; // All the queries has been reached
}
// If the state is interesting, apply tock changes
Expand All @@ -198,14 +228,15 @@ bool ReachabilitySearcher::ForwardReachabilitySearch(const nondeterminism_strate
AddToWaitingList(state.tta, allTickStateChanges, false, curstatehash);

Passed.emplace(std::make_pair(curstatehash, state));
debug_cleanup_waiting_list(*this, curstatehash, state);

cleanup_waiting_list(*this, curstatehash, state);
stateit = PickStateFromWaitingList(strategy);
}
if(!CLIConfig::getInstance()["notrace"])
PrintResults(query_results);
spdlog::info("Found a negative result after searching: {0} states", Passed.size());
if(CLIConfig::getInstance()["verbosity"].as_integer() >= 6)
debug_print_passed_list(*this);
if(!CLIConfig::getInstance()["notrace"])
return query_results.size() - PrintResults(query_results) == 0;
return false;
}

Expand All @@ -228,8 +259,10 @@ void ReachabilitySearcher::AddToWaitingList(const TTA &state, const std::vector<
auto nstate = state << change;
auto nstatehash = nstate.GetCurrentStateHash();
if (Passed.find(nstatehash) == Passed.end()) {
if (nstatehash == state_hash)
spdlog::warn("Colliding state hashes!");
if (nstatehash == state_hash) {
spdlog::warn("Recursive state hashes!");
continue;
}
Waiting.emplace(std::make_pair(nstatehash, SearchState{nstate, state_hash, justTocked}));
}
}
Expand All @@ -238,12 +271,16 @@ void ReachabilitySearcher::AddToWaitingList(const TTA &state, const std::vector<
if(statechanges.size() > 1) {
auto baseChanges = state << *statechanges.begin();
for (auto it = statechanges.begin() + 1; it != statechanges.end(); ++it) {
if(it->IsEmpty())
continue;
/// This is a lot of copying large data objects... Figure something out with maybe std::move
auto nstate = baseChanges << *it;
auto nstatehash = nstate.GetCurrentStateHash();
if (Passed.find(nstatehash) == Passed.end()) {
if (nstatehash == state_hash)
spdlog::warn("Colliding state hashes!");
if (nstatehash == state_hash) {
spdlog::warn("Recursive state hashes!");
continue;
}
Waiting.emplace(std::make_pair(nstatehash, SearchState{nstate, state_hash, justTocked}));
}
}
Expand Down
2 changes: 1 addition & 1 deletion src/verifier/ReachabilitySearcher.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ struct ReachabilitySearcher {
bool IsQuerySatisfied(const Query& query, const TTA& state);
void AreQueriesSatisfied(std::vector<QueryResultPair>& queries, const TTA& state, size_t state_hash);
bool ForwardReachabilitySearch(const nondeterminism_strategy_t& strategy);
void PrintResults(const std::vector<QueryResultPair>& results);
auto PrintResults(const std::vector<QueryResultPair>& results) -> int;
void OutputResults(const std::vector<QueryResultPair>& results);
StateList::iterator PickStateFromWaitingList(const nondeterminism_strategy_t& strategy);
};
Expand Down
Loading

0 comments on commit b23b920

Please sign in to comment.