Types for ebpf

.github/workflows/codeql-analysis.yml

@@ -13,10 +13,10 @@ name: "CodeQL"
 
 on:
   push:
-    branches: [ master ]
+    branches: [ master, type-proofs ]
   pull_request:
     # The branches below must be a subset of the branches above
-    branches: [ master ]
+    branches: [ master, type-proofs ]
   schedule:
     - cron: '43 12 * * 2'
 

.gitignore

@@ -19,3 +19,4 @@ CMakeSettings.json
 cmake-build-debug/
 cmake-build-release/
 cmake-build-sanitize/
+.tags

CMakeLists.txt

@@ -10,7 +10,8 @@ if (IS_DIRECTORY "${PROJECT_SOURCE_DIR}/.git")
 endif ()
 
 if ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU" OR
-    "${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")
+    "${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
+    "${CMAKE_CXX_COMPILER_ID}" STREQUAL "AppleClang")
   find_package(yaml-cpp REQUIRED)
   find_package(Boost REQUIRED)
   set(CMAKE_CXX_STANDARD 17)
@@ -68,10 +69,11 @@ file(GLOB ALL_TEST
         )
 
 if ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU" OR
-    "${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang")
+    "${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
+    "${CMAKE_CXX_COMPILER_ID}" STREQUAL "AppleClang")
   set(COMMON_FLAGS -Wall -Wfatal-errors -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8)
 
-  set(RELEASE_FLAGS -O2 -flto -ffat-lto-objects)
+  set(RELEASE_FLAGS -O2 -flto)
 
   set(DEBUG_FLAGS -O0 -g3 -fno-omit-frame-pointer)
 

src/config.hpp

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: MIT
 #pragma once
 
-enum class abstract_domain_kind { EBPF_DOMAIN, TYPE_DOMAIN };
+enum class abstract_domain_kind { EBPF_DOMAIN, TYPE_DOMAIN, OFFSET_DOMAIN, REGION_DOMAIN, INTERVAL_PROP_DOMAIN };
 
 struct ebpf_verifier_options_t {
     bool check_termination;

src/crab/abstract_domain.cpp

@@ -1,5 +1,12 @@
+// Copyright (c) Prevail Verifier contributors.
+// SPDX-License-Identifier: MIT
+
 #include "abstract_domain.hpp"
 #include "ebpf_domain.hpp"
+#include "type_domain.hpp"
+#include "region_domain.hpp"
+#include "interval_prop_domain.hpp"
+#include "offset_domain.hpp"
 
 template <typename Domain>
 abstract_domain_t::abstract_domain_model<Domain>::abstract_domain_model(Domain abs_val)
@@ -104,68 +111,68 @@ abstract_domain_t::abstract_domain_model<Domain>::narrow(const abstract_domain_t
 }
 
 template <typename Domain>
-void abstract_domain_t::abstract_domain_model<Domain>::operator()(const basic_block_t& bb, bool check_termination) {
-    m_abs_val.operator()(bb, check_termination);
+void abstract_domain_t::abstract_domain_model<Domain>::operator()(const basic_block_t& bb, bool check_termination, int print) {
+    m_abs_val.operator()(bb, check_termination, print);
 }
 
 template <typename Domain>
-void abstract_domain_t::abstract_domain_model<Domain>::operator()(const Undefined& s) {
-    m_abs_val.operator()(s);
+void abstract_domain_t::abstract_domain_model<Domain>::operator()(const Undefined& s, location_t loc, int print) {
+    m_abs_val.operator()(s, loc, print);
 }
 
 template <typename Domain>
-void abstract_domain_t::abstract_domain_model<Domain>::operator()(const Bin& s) {
-    m_abs_val.operator()(s);
+void abstract_domain_t::abstract_domain_model<Domain>::operator()(const Bin& s, location_t loc, int print) {
+    m_abs_val.operator()(s, loc, print);
 }
 
 template <typename Domain>
-void abstract_domain_t::abstract_domain_model<Domain>::operator()(const Un& s) {
-    m_abs_val.operator()(s);
+void abstract_domain_t::abstract_domain_model<Domain>::operator()(const Un& s, location_t loc, int print) {
+    m_abs_val.operator()(s, loc, print);
 }
 
 template <typename Domain>
-void abstract_domain_t::abstract_domain_model<Domain>::operator()(const LoadMapFd& s) {
-    m_abs_val.operator()(s);
+void abstract_domain_t::abstract_domain_model<Domain>::operator()(const LoadMapFd& s, location_t loc, int print) {
+    m_abs_val.operator()(s, loc, print);
 }
 
 template <typename Domain>
-void abstract_domain_t::abstract_domain_model<Domain>::operator()(const Call& s) {
-    m_abs_val.operator()(s);
+void abstract_domain_t::abstract_domain_model<Domain>::operator()(const Call& s, location_t loc, int print) {
+    m_abs_val.operator()(s, loc, print);
 }
 
 template <typename Domain>
-void abstract_domain_t::abstract_domain_model<Domain>::operator()(const Exit& s) {
-    m_abs_val.operator()(s);
+void abstract_domain_t::abstract_domain_model<Domain>::operator()(const Exit& s, location_t loc, int print) {
+    m_abs_val.operator()(s, loc, print);
 }
 
 template <typename Domain>
-void abstract_domain_t::abstract_domain_model<Domain>::operator()(const Jmp& s) {
-    m_abs_val.operator()(s);
+void abstract_domain_t::abstract_domain_model<Domain>::operator()(const Jmp& s, location_t loc, int print) {
+    m_abs_val.operator()(s, loc, print);
 }
 
 template <typename Domain>
-void abstract_domain_t::abstract_domain_model<Domain>::operator()(const Mem& s) {
-    m_abs_val.operator()(s);
+void abstract_domain_t::abstract_domain_model<Domain>::operator()(const Mem& s, location_t loc, int print) {
+    m_abs_val.operator()(s, loc, print);
 }
 
 template <typename Domain>
-void abstract_domain_t::abstract_domain_model<Domain>::operator()(const Packet& s) {
-    m_abs_val.operator()(s);
+void abstract_domain_t::abstract_domain_model<Domain>::operator()(const Packet& s, location_t loc, int print) {
+    m_abs_val.operator()(s, loc, print);
 }
 
 template <typename Domain>
-void abstract_domain_t::abstract_domain_model<Domain>::operator()(const LockAdd& s) {
-    m_abs_val.operator()(s);
+void abstract_domain_t::abstract_domain_model<Domain>::operator()(const LockAdd& s, location_t loc, int print) {
+    m_abs_val.operator()(s, loc, print);
 }
 
 template <typename Domain>
-void abstract_domain_t::abstract_domain_model<Domain>::operator()(const Assume& s) {
-    m_abs_val.operator()(s);
+void abstract_domain_t::abstract_domain_model<Domain>::operator()(const Assume& s, location_t loc, int print) {
+    m_abs_val.operator()(s, loc, print);
 }
 
 template <typename Domain>
-void abstract_domain_t::abstract_domain_model<Domain>::operator()(const Assert& s) {
-    m_abs_val.operator()(s);
+void abstract_domain_t::abstract_domain_model<Domain>::operator()(const Assert& s, location_t loc, int print) {
+    m_abs_val.operator()(s, loc, print);
 }
 
 template <typename Domain>
@@ -245,33 +252,33 @@ abstract_domain_t abstract_domain_t::narrow(const abstract_domain_t& abs) const
     return abstract_domain_t(std::move(m_concept->narrow(*(abs.m_concept))));
 }
 
-void abstract_domain_t::operator()(const basic_block_t& bb, bool check_termination) {
-    m_concept->operator()(bb, check_termination);
+void abstract_domain_t::operator()(const basic_block_t& bb, bool check_termination, int print) {
+    m_concept->operator()(bb, check_termination, print);
 }
 
-void abstract_domain_t::operator()(const Undefined& s) { m_concept->operator()(s); }
+void abstract_domain_t::operator()(const Undefined& s, location_t loc, int print) { m_concept->operator()(s, loc, print); }
 
-void abstract_domain_t::operator()(const Bin& s) { m_concept->operator()(s); }
+void abstract_domain_t::operator()(const Bin& s, location_t loc, int print) { m_concept->operator()(s, loc, print); }
 
-void abstract_domain_t::operator()(const Un& s) { m_concept->operator()(s); }
+void abstract_domain_t::operator()(const Un& s, location_t loc, int print) { m_concept->operator()(s, loc, print); }
 
-void abstract_domain_t::operator()(const LoadMapFd& s) { m_concept->operator()(s); }
+void abstract_domain_t::operator()(const LoadMapFd& s, location_t loc, int print) { m_concept->operator()(s, loc, print); }
 
-void abstract_domain_t::operator()(const Call& s) { m_concept->operator()(s); }
+void abstract_domain_t::operator()(const Call& s, location_t loc, int print) { m_concept->operator()(s, loc, print); }
 
-void abstract_domain_t::operator()(const Exit& s) { m_concept->operator()(s); }
+void abstract_domain_t::operator()(const Exit& s, location_t loc, int print) { m_concept->operator()(s, loc, print); }
 
-void abstract_domain_t::operator()(const Jmp& s) { m_concept->operator()(s); }
+void abstract_domain_t::operator()(const Jmp& s, location_t loc, int print) { m_concept->operator()(s, loc, print); }
 
-void abstract_domain_t::operator()(const Mem& s) { m_concept->operator()(s); }
+void abstract_domain_t::operator()(const Mem& s, location_t loc, int print) { m_concept->operator()(s, loc, print); }
 
-void abstract_domain_t::operator()(const Packet& s) { m_concept->operator()(s); }
+void abstract_domain_t::operator()(const Packet& s, location_t loc, int print) { m_concept->operator()(s, loc, print); }
 
-void abstract_domain_t::operator()(const LockAdd& s) { m_concept->operator()(s); }
+void abstract_domain_t::operator()(const LockAdd& s, location_t loc, int print) { m_concept->operator()(s, loc, print); }
 
-void abstract_domain_t::operator()(const Assume& s) { m_concept->operator()(s); }
+void abstract_domain_t::operator()(const Assume& s, location_t loc, int print) { m_concept->operator()(s, loc, print); }
 
-void abstract_domain_t::operator()(const Assert& s) { m_concept->operator()(s); }
+void abstract_domain_t::operator()(const Assert& s, location_t loc, int print) { m_concept->operator()(s, loc, print); }
 
 void abstract_domain_t::write(std::ostream& os) const { m_concept->write(os); }
 
@@ -290,3 +297,7 @@ std::ostream& operator<<(std::ostream& o, const abstract_domain_t& dom) {
 
 // REQUIRED: instantiation for supported domains
 template abstract_domain_t::abstract_domain_t(ebpf_domain_t);
+template abstract_domain_t::abstract_domain_t(type_domain_t);
+template abstract_domain_t::abstract_domain_t(offset_domain_t);
+template abstract_domain_t::abstract_domain_t(region_domain_t);
+template abstract_domain_t::abstract_domain_t(interval_prop_domain_t);

src/crab/abstract_domain.hpp

@@ -1,11 +1,13 @@
 #pragma once
 
+#include <boost/optional/optional.hpp>
 #include "cfg.hpp"
 #include "linear_constraint.hpp"
 #include "string_constraints.hpp"
 
 #include "array_domain.hpp"
 using check_require_func_t = std::function<bool(crab::domains::NumAbsDomain&, const linear_constraint_t&, std::string)>;
+using location_t = boost::optional<std::pair<label_t, uint32_t>>;
 class abstract_domain_t {
   private:
     class abstract_domain_concept {
@@ -29,19 +31,19 @@ class abstract_domain_t {
         virtual std::unique_ptr<abstract_domain_concept> operator&(const abstract_domain_concept& abs) const = 0;
         virtual std::unique_ptr<abstract_domain_concept> widen(const abstract_domain_concept& abs) const = 0;
         virtual std::unique_ptr<abstract_domain_concept> narrow(const abstract_domain_concept& abs) const = 0;
-        virtual void operator()(const basic_block_t&, bool) = 0;
-        virtual void operator()(const Undefined&) = 0;
-        virtual void operator()(const Bin&) = 0;
-        virtual void operator()(const Un&) = 0;
-        virtual void operator()(const LoadMapFd&) = 0;
-        virtual void operator()(const Call&) = 0;
-        virtual void operator()(const Exit&) = 0;
-        virtual void operator()(const Jmp&) = 0;
-        virtual void operator()(const Mem&) = 0;
-        virtual void operator()(const Packet&) = 0;
-        virtual void operator()(const LockAdd&) = 0;
-        virtual void operator()(const Assume&) = 0;
-        virtual void operator()(const Assert&) = 0;
+        virtual void operator()(const basic_block_t&, bool, int) = 0;
+        virtual void operator()(const Undefined&, location_t, int) = 0;
+        virtual void operator()(const Bin&, location_t, int) = 0;
+        virtual void operator()(const Un&, location_t, int) = 0;
+        virtual void operator()(const LoadMapFd&, location_t, int) = 0;
+        virtual void operator()(const Call&, location_t, int) = 0;
+        virtual void operator()(const Exit&, location_t, int) = 0;
+        virtual void operator()(const Jmp&, location_t, int) = 0;
+        virtual void operator()(const Mem&, location_t, int) = 0;
+        virtual void operator()(const Packet&, location_t, int) = 0;
+        virtual void operator()(const LockAdd&, location_t, int) = 0;
+        virtual void operator()(const Assume&, location_t, int) = 0;
+        virtual void operator()(const Assert&, location_t, int) = 0;
         virtual void write(std::ostream& os) const = 0;
         virtual std::string domain_name() const = 0;
 
@@ -72,19 +74,19 @@ class abstract_domain_t {
         std::unique_ptr<abstract_domain_concept> operator&(const abstract_domain_concept& abs) const override;
         std::unique_ptr<abstract_domain_concept> widen(const abstract_domain_concept& abs) const override;
         std::unique_ptr<abstract_domain_concept> narrow(const abstract_domain_concept& abs) const override;
-        void operator()(const basic_block_t& bb, bool check_termination) override;
-        void operator()(const Undefined& s) override;
-        void operator()(const Bin& s) override;
-        void operator()(const Un& s) override;
-        void operator()(const LoadMapFd& s) override;
-        void operator()(const Call& s) override;
-        void operator()(const Exit& s) override;
-        void operator()(const Jmp& s) override;
-        void operator()(const Mem& s) override;
-        void operator()(const Packet& s) override;
-        void operator()(const LockAdd& s) override;
-        void operator()(const Assume& s) override;
-        void operator()(const Assert& s) override;
+        void operator()(const basic_block_t& bb, bool check_termination, int print = 0) override;
+        void operator()(const Undefined& s, location_t loc = boost::none, int print = 0) override;
+        void operator()(const Bin& s, location_t loc = boost::none, int print = 0) override;
+        void operator()(const Un& s, location_t loc = boost::none, int print = 0) override;
+        void operator()(const LoadMapFd& s, location_t loc = boost::none, int print = 0) override;
+        void operator()(const Call& s, location_t loc = boost::none, int print = 0) override;
+        void operator()(const Exit& s, location_t loc = boost::none, int print = 0) override;
+        void operator()(const Jmp& s, location_t loc = boost::none, int print = 0) override;
+        void operator()(const Mem& s, location_t loc = boost::none, int print = 0) override;
+        void operator()(const Packet& s, location_t loc = boost::none, int print = 0) override;
+        void operator()(const LockAdd& s, location_t loc = boost::none, int print = 0) override;
+        void operator()(const Assume& s, location_t loc = boost::none, int print = 0) override;
+        void operator()(const Assert& s, location_t loc = boost::none, int print = 0) override;
         void write(std::ostream& os) const override;
         std::string domain_name() const override;
         int get_instruction_count_upper_bound() override;
@@ -115,19 +117,19 @@ class abstract_domain_t {
     abstract_domain_t operator&(const abstract_domain_t& abs) const;
     abstract_domain_t widen(const abstract_domain_t& abs) const;
     abstract_domain_t narrow(const abstract_domain_t& abs) const;
-    void operator()(const basic_block_t& bb, bool check_termination);
-    void operator()(const Undefined& s);
-    void operator()(const Bin& s);
-    void operator()(const Un& s);
-    void operator()(const LoadMapFd& s);
-    void operator()(const Call& s);
-    void operator()(const Exit& s);
-    void operator()(const Jmp& s);
-    void operator()(const Mem& s);
-    void operator()(const Packet& s);
-    void operator()(const LockAdd& s);
-    void operator()(const Assume& s);
-    void operator()(const Assert& s);
+    void operator()(const basic_block_t& bb, bool check_termination, int print = 0);
+    void operator()(const Undefined& s, location_t loc = boost::none, int print = 0);
+    void operator()(const Bin& s, location_t loc = boost::none, int print = 0);
+    void operator()(const Un& s, location_t loc = boost::none, int print = 0);
+    void operator()(const LoadMapFd& s, location_t loc = boost::none, int print = 0);
+    void operator()(const Call& s, location_t loc = boost::none, int print = 0);
+    void operator()(const Exit& s, location_t loc = boost::none, int print = 0);
+    void operator()(const Jmp& s, location_t loc = boost::none, int print = 0);
+    void operator()(const Mem& s, location_t loc = boost::none, int print = 0);
+    void operator()(const Packet& s, location_t loc = boost::none, int print = 0);
+    void operator()(const LockAdd& s, location_t loc = boost::none, int print = 0);
+    void operator()(const Assume& s, location_t loc = boost::none, int print = 0);
+    void operator()(const Assert& s, location_t loc = boost::none, int print = 0);
     void write(std::ostream& os) const;
     std::string domain_name() const;
     int get_instruction_count_upper_bound();