From 12dfd8a5cab806d1f6f5b55ee25b73b2b73d3159 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= Date: Tue, 28 Apr 2020 22:09:01 +0200 Subject: [PATCH] GUI: Show missing/added contracts in tab --- gui/mainwindow.cpp | 16 +++++++++++ gui/mainwindow.h | 3 +++ gui/resultsview.cpp | 18 +++++++++++-- gui/resultsview.h | 4 +++ gui/resultsview.ui | 65 +++++++++++++++++++++++++++++++++------------ lib/exprengine.cpp | 56 ++++++++++++++++++++++++++++++-------- 6 files changed, 132 insertions(+), 30 deletions(-) diff --git a/gui/mainwindow.cpp b/gui/mainwindow.cpp index 7479fa8d5..31203acb8 100644 --- a/gui/mainwindow.cpp +++ b/gui/mainwindow.cpp @@ -346,6 +346,8 @@ void MainWindow::loadSettings() QDir::setCurrent(inf.absolutePath()); } } + + updateContractsTab(); } void MainWindow::saveSettings() const @@ -605,6 +607,17 @@ QStringList MainWindow::selectFilesToAnalyze(QFileDialog::FileMode mode) return selected; } +void MainWindow::updateContractsTab() +{ + QStringList addedContracts; + if (mProjectFile) { + for (const auto it: mProjectFile->getFunctionContracts()) { + addedContracts << QString::fromStdString(it.first); + } + } + mUI.mResults->setAddedContracts(addedContracts); +} + void MainWindow::analyzeFiles() { Settings::terminate(false); @@ -1462,6 +1475,7 @@ void MainWindow::loadProjectFile(const QString &filePath) mUI.mActionEditProjectFile->setEnabled(true); delete mProjectFile; mProjectFile = new ProjectFile(filePath, this); + updateContractsTab(); if (!loadLastResults()) analyzeProject(mProjectFile); } @@ -1813,4 +1827,6 @@ void MainWindow::editFunctionContract(QString function) mProjectFile->setFunctionContract(function, dlg.getExpects()); mProjectFile->write(); } + + updateContractsTab(); } diff --git a/gui/mainwindow.h b/gui/mainwindow.h index f2736bde9..ed10a6449 100644 --- a/gui/mainwindow.h +++ b/gui/mainwindow.h @@ -73,6 +73,9 @@ public: public slots: + /** Update "Contracts" tab */ + void updateContractsTab(); + /** @brief Slot for analyze files menu item */ void analyzeFiles(); diff --git a/gui/resultsview.cpp b/gui/resultsview.cpp index a44cd47b0..5d5806574 100644 --- a/gui/resultsview.cpp +++ b/gui/resultsview.cpp @@ -64,6 +64,9 @@ ResultsView::ResultsView(QWidget * parent) : connect(this, &ResultsView::showHiddenResults, mUI.mTree, &ResultsTree::showHiddenResults); mUI.mListLog->setContextMenuPolicy(Qt::CustomContextMenu); + + mUI.mListAddedContracts->setSortingEnabled(true); + mUI.mListMissingContracts->setSortingEnabled(true); } void ResultsView::initialize(QSettings *settings, ApplicationList *list, ThreadHandler *checkThreadHandler) @@ -86,6 +89,12 @@ ResultsView::~ResultsView() //dtor } +void ResultsView::setAddedContracts(const QStringList &addedContracts) +{ + mUI.mListAddedContracts->clear(); + mUI.mListAddedContracts->addItems(addedContracts); +} + void ResultsView::clear(bool results) { if (results) { @@ -439,8 +448,13 @@ void ResultsView::bughuntingReportLine(const QString& line) for (const QString& s: line.split("\n")) { if (s.isEmpty()) continue; - if (s.startsWith("[function-report] ")) - mUI.mListSafeFunctions->addItem(s.mid(s.lastIndexOf(":") + 1)); + if (s.startsWith("[missing contract] ")) { + const QString functionName = s.mid(19); + if (!mContracts.contains(functionName)) { + mContracts.insert(functionName); + mUI.mListMissingContracts->addItem(functionName); + } + } } } diff --git a/gui/resultsview.h b/gui/resultsview.h index 32dda3b3b..b3b14be92 100644 --- a/gui/resultsview.h +++ b/gui/resultsview.h @@ -54,6 +54,8 @@ public: mUI.mTree->setTags(tags); } + void setAddedContracts(const QStringList &addedContracts); + /** * @brief Clear results and statistics and reset progressinfo. * @param results Remove all the results from view? @@ -361,6 +363,8 @@ private slots: * @param pos Mouse click position */ void on_mListLog_customContextMenuRequested(const QPoint &pos); +private: + QSet mContracts; }; /// @} #endif // RESULTSVIEW_H diff --git a/gui/resultsview.ui b/gui/resultsview.ui index cb1c32b67..584c8a9ea 100644 --- a/gui/resultsview.ui +++ b/gui/resultsview.ui @@ -7,7 +7,7 @@ 0 0 459 - 357 + 358 @@ -153,25 +153,56 @@ - + - Safe functions + Contracts - - - 0 - - - 0 - - - 0 - - - 0 - + - + + + Qt::Vertical + + + + + + + Configured contracts: + + + + + + + QAbstractItemView::NoEditTriggers + + + + + + + + + + + Missing contracts: + + + + + + + QAbstractItemView::NoEditTriggers + + + true + + + + + + diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp index e8be95ca2..ff6786c5f 100644 --- a/lib/exprengine.cpp +++ b/lib/exprengine.cpp @@ -143,6 +143,14 @@ namespace { bool isAllOk() const { return mErrors.empty(); } + + void addMissingContract(const std::string &f) { + mMissingContracts.insert(f); + } + + const std::set getMissingContracts() const { + return mMissingContracts; + } private: const char *getStatus(int linenr) const { if (mErrors.find(linenr) != mErrors.end()) @@ -158,6 +166,7 @@ namespace { int mAbortLine; std::set mSymbols; std::set mErrors; + std::set mMissingContracts; }; class Data : public ExprEngine::DataBase { @@ -312,6 +321,14 @@ namespace { mTrackExecution->state(tok, s.str()); } + void addMissingContract(const std::string &f) { + mTrackExecution->addMissingContract(f); + } + + const std::set getMissingContracts() const { + return mTrackExecution->getMissingContracts(); + } + ExprEngine::ValuePtr notValue(ExprEngine::ValuePtr v) { auto b = std::dynamic_pointer_cast(v); if (b) { @@ -1289,15 +1306,28 @@ static void checkContract(Data &data, const Token *tok, const Function *function &data.tokenizer->list, Severity::SeverityType::error, id, - "Function '" + functionName + "' is called, can not determine that its contract '" + functionExpects + "' is always met.", + "Function '" + function->name() + "' is called, can not determine that its contract '" + functionExpects + "' is always met.", CWE(0), bailoutValue); - if (!bailoutValue) - errmsg.function = data.currentFunction; + + errmsg.function = functionName; data.errorLogger->reportErr(errmsg); } } catch (const z3::exception &exception) { std::cerr << "z3: " << exception << std::endl; + } catch (const VerifyException &e) { + std::list callstack{tok}; + const char * const id = "internalErrorInExprEngine"; + const auto contractIt = data.settings->functionContracts.find(function->fullName()); + const std::string functionExpects = contractIt->second; + ErrorLogger::ErrorMessage errmsg(callstack, + &data.tokenizer->list, + Severity::SeverityType::information, + id, + "ExprEngine failed to execute contract for function '" + function->name() + "'.", + CWE(0), + false); + data.errorLogger->reportErr(errmsg); } #endif } @@ -1339,9 +1369,17 @@ static ExprEngine::ValuePtr executeFunctionCall(const Token *tok, Data &data) throw VerifyException(tok, "Expression '" + tok->expressionString() + "' has unknown type!"); if (tok->astOperand1()->function()) { - const auto contractIt = data.settings->functionContracts.find(tok->astOperand1()->function()->fullName()); - if (contractIt != data.settings->functionContracts.end()) + const std::string &functionName = tok->astOperand1()->function()->fullName(); + const auto contractIt = data.settings->functionContracts.find(functionName); + if (contractIt != data.settings->functionContracts.end()) { checkContract(data, tok, tok->astOperand1()->function(), argValues); + } else if (!argValues.empty()) { + bool bailout = false; + for (const auto v: argValues) + bailout |= (v && v->type == ExprEngine::ValueType::BailoutValue); + if (!bailout) + data.addMissingContract(functionName); + } } auto val = getValueRangeFromValueType(data.getNewSymbolName(), tok->valueType(), *data.settings); @@ -1918,12 +1956,8 @@ void ExprEngine::executeFunction(const Scope *functionScope, ErrorLogger *errorL // Write a report if (bugHuntingReport) { - report << "[function-report] " - << Path::stripDirectoryPart(tokenizer->list.getFiles().at(functionScope->bodyStart->fileIndex())) << ":" - << functionScope->bodyStart->linenr() << ":" - << function->name() - << (trackExecution.isAllOk() ? " is safe" : " is not safe") - << std::endl; + for (const std::string &f: trackExecution.getMissingContracts()) + report << "[missing contract] " << f << std::endl; } }