GUI: Show missing/added contracts in tab

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();
 }

gui/mainwindow.h

@@ -73,6 +73,9 @@ public:
 
 public slots:
 
+    /** Update "Contracts" tab */
+    void updateContractsTab();
+
     /** @brief Slot for analyze files menu item */
     void analyzeFiles();
 

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] "))
+        if (s.startsWith("[missing contract] ")) {
-            mUI.mListSafeFunctions->addItem(s.mid(s.lastIndexOf(":") + 1));
+            const QString functionName = s.mid(19);
+            if (!mContracts.contains(functionName)) {
+                mContracts.insert(functionName);
+                mUI.mListMissingContracts->addItem(functionName);
+            }
+        }
     }
 }
 

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<QString> mContracts;
 };
 /// @}
 #endif // RESULTSVIEW_H

gui/resultsview.ui

@@ -7,7 +7,7 @@
     <x>0</x>
     <y>0</y>
     <width>459</width>
-    <height>357</height>
+    <height>358</height>
    </rect>
   </property>
   <property name="sizePolicy">
@@ -153,25 +153,56 @@
         </item>
        </layout>
       </widget>
-      <widget class="QWidget" name="mTabSafeFunctions">
+      <widget class="QWidget" name="mTabContracts">
        <attribute name="title">
-        <string>Safe functions</string>
+        <string>Contracts</string>
        </attribute>
-       <layout class="QVBoxLayout" name="verticalLayout_4">
+       <layout class="QVBoxLayout" name="verticalLayout_6">
-        <property name="leftMargin">
-         <number>0</number>
-        </property>
-        <property name="topMargin">
-         <number>0</number>
-        </property>
-        <property name="rightMargin">
-         <number>0</number>
-        </property>
-        <property name="bottomMargin">
-         <number>0</number>
-        </property>
         <item>
-         <widget class="QListWidget" name="mListSafeFunctions"/>
+         <widget class="QSplitter" name="splitter">
+          <property name="orientation">
+           <enum>Qt::Vertical</enum>
+          </property>
+          <widget class="QWidget" name="layoutWidget">
+           <layout class="QVBoxLayout" name="verticalLayout_4">
+            <item>
+             <widget class="QLabel" name="label_2">
+              <property name="text">
+               <string>Configured contracts:</string>
+              </property>
+             </widget>
+            </item>
+            <item>
+             <widget class="QListWidget" name="mListAddedContracts">
+              <property name="editTriggers">
+               <set>QAbstractItemView::NoEditTriggers</set>
+              </property>
+             </widget>
+            </item>
+           </layout>
+          </widget>
+          <widget class="QWidget" name="layoutWidget">
+           <layout class="QVBoxLayout" name="verticalLayout_5">
+            <item>
+             <widget class="QLabel" name="label">
+              <property name="text">
+               <string>Missing contracts:</string>
+              </property>
+             </widget>
+            </item>
+            <item>
+             <widget class="QListWidget" name="mListMissingContracts">
+              <property name="editTriggers">
+               <set>QAbstractItemView::NoEditTriggers</set>
+              </property>
+              <property name="sortingEnabled">
+               <bool>true</bool>
+              </property>
+             </widget>
+            </item>
+           </layout>
+          </widget>
+         </widget>
         </item>
        </layout>
       </widget>

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<std::string> 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<std::string> mSymbols;
         std::set<int> mErrors;
+        std::set<std::string> 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<std::string> getMissingContracts() const {
+            return mTrackExecution->getMissingContracts();
+        }
+
         ExprEngine::ValuePtr notValue(ExprEngine::ValuePtr v) {
             auto b = std::dynamic_pointer_cast<ExprEngine::BinOpResult>(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<const Token*> 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());
+        const std::string &functionName = tok->astOperand1()->function()->fullName();
-        if (contractIt != data.settings->functionContracts.end())
+        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] "
+        for (const std::string &f: trackExecution.getMissingContracts())
-               << Path::stripDirectoryPart(tokenizer->list.getFiles().at(functionScope->bodyStart->fileIndex())) << ":"
+            report << "[missing contract] " << f << std::endl;
-               << functionScope->bodyStart->linenr() << ":"
-               << function->name()
-               << (trackExecution.isAllOk() ? " is safe" : " is not safe")
-               << std::endl;
     }
 }