diff --git a/.github/workflows/codeql-analysis.yml b/.github/workflows/codeql-analysis.yml index c0b5b174b..66aa30311 100644 --- a/.github/workflows/codeql-analysis.yml +++ b/.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' diff --git a/.gitignore b/.gitignore index e9ee955dc..322df4e5f 100644 --- a/.gitignore +++ b/.gitignore @@ -19,3 +19,4 @@ CMakeSettings.json cmake-build-debug/ cmake-build-release/ cmake-build-sanitize/ +.tags diff --git a/CMakeLists.txt b/CMakeLists.txt index 37cafd5f6..69e05be5e 100644 --- a/CMakeLists.txt +++ b/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) diff --git a/src/config.hpp b/src/config.hpp index 6e125fde2..5c6c5279d 100644 --- a/src/config.hpp +++ b/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; diff --git a/src/crab/abstract_domain.cpp b/src/crab/abstract_domain.cpp index 21e328a2b..f06741e39 100644 --- a/src/crab/abstract_domain.cpp +++ b/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 abstract_domain_t::abstract_domain_model::abstract_domain_model(Domain abs_val) @@ -104,68 +111,68 @@ abstract_domain_t::abstract_domain_model::narrow(const abstract_domain_t } template -void abstract_domain_t::abstract_domain_model::operator()(const basic_block_t& bb, bool check_termination) { - m_abs_val.operator()(bb, check_termination); +void abstract_domain_t::abstract_domain_model::operator()(const basic_block_t& bb, bool check_termination, int print) { + m_abs_val.operator()(bb, check_termination, print); } template -void abstract_domain_t::abstract_domain_model::operator()(const Undefined& s) { - m_abs_val.operator()(s); +void abstract_domain_t::abstract_domain_model::operator()(const Undefined& s, location_t loc, int print) { + m_abs_val.operator()(s, loc, print); } template -void abstract_domain_t::abstract_domain_model::operator()(const Bin& s) { - m_abs_val.operator()(s); +void abstract_domain_t::abstract_domain_model::operator()(const Bin& s, location_t loc, int print) { + m_abs_val.operator()(s, loc, print); } template -void abstract_domain_t::abstract_domain_model::operator()(const Un& s) { - m_abs_val.operator()(s); +void abstract_domain_t::abstract_domain_model::operator()(const Un& s, location_t loc, int print) { + m_abs_val.operator()(s, loc, print); } template -void abstract_domain_t::abstract_domain_model::operator()(const LoadMapFd& s) { - m_abs_val.operator()(s); +void abstract_domain_t::abstract_domain_model::operator()(const LoadMapFd& s, location_t loc, int print) { + m_abs_val.operator()(s, loc, print); } template -void abstract_domain_t::abstract_domain_model::operator()(const Call& s) { - m_abs_val.operator()(s); +void abstract_domain_t::abstract_domain_model::operator()(const Call& s, location_t loc, int print) { + m_abs_val.operator()(s, loc, print); } template -void abstract_domain_t::abstract_domain_model::operator()(const Exit& s) { - m_abs_val.operator()(s); +void abstract_domain_t::abstract_domain_model::operator()(const Exit& s, location_t loc, int print) { + m_abs_val.operator()(s, loc, print); } template -void abstract_domain_t::abstract_domain_model::operator()(const Jmp& s) { - m_abs_val.operator()(s); +void abstract_domain_t::abstract_domain_model::operator()(const Jmp& s, location_t loc, int print) { + m_abs_val.operator()(s, loc, print); } template -void abstract_domain_t::abstract_domain_model::operator()(const Mem& s) { - m_abs_val.operator()(s); +void abstract_domain_t::abstract_domain_model::operator()(const Mem& s, location_t loc, int print) { + m_abs_val.operator()(s, loc, print); } template -void abstract_domain_t::abstract_domain_model::operator()(const Packet& s) { - m_abs_val.operator()(s); +void abstract_domain_t::abstract_domain_model::operator()(const Packet& s, location_t loc, int print) { + m_abs_val.operator()(s, loc, print); } template -void abstract_domain_t::abstract_domain_model::operator()(const LockAdd& s) { - m_abs_val.operator()(s); +void abstract_domain_t::abstract_domain_model::operator()(const LockAdd& s, location_t loc, int print) { + m_abs_val.operator()(s, loc, print); } template -void abstract_domain_t::abstract_domain_model::operator()(const Assume& s) { - m_abs_val.operator()(s); +void abstract_domain_t::abstract_domain_model::operator()(const Assume& s, location_t loc, int print) { + m_abs_val.operator()(s, loc, print); } template -void abstract_domain_t::abstract_domain_model::operator()(const Assert& s) { - m_abs_val.operator()(s); +void abstract_domain_t::abstract_domain_model::operator()(const Assert& s, location_t loc, int print) { + m_abs_val.operator()(s, loc, print); } template @@ -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); diff --git a/src/crab/abstract_domain.hpp b/src/crab/abstract_domain.hpp index a1244ee3b..01af25c5f 100644 --- a/src/crab/abstract_domain.hpp +++ b/src/crab/abstract_domain.hpp @@ -1,11 +1,13 @@ #pragma once +#include #include "cfg.hpp" #include "linear_constraint.hpp" #include "string_constraints.hpp" #include "array_domain.hpp" using check_require_func_t = std::function; +using location_t = boost::optional>; class abstract_domain_t { private: class abstract_domain_concept { @@ -29,19 +31,19 @@ class abstract_domain_t { virtual std::unique_ptr operator&(const abstract_domain_concept& abs) const = 0; virtual std::unique_ptr widen(const abstract_domain_concept& abs) const = 0; virtual std::unique_ptr 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 operator&(const abstract_domain_concept& abs) const override; std::unique_ptr widen(const abstract_domain_concept& abs) const override; std::unique_ptr 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(); diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp index a28bc6897..cf5893d06 100644 --- a/src/crab/ebpf_domain.cpp +++ b/src/crab/ebpf_domain.cpp @@ -491,7 +491,7 @@ void ebpf_domain_t::overflow(variable_t lhs) { havoc(lhs); } -void ebpf_domain_t::operator()(const basic_block_t& bb, bool check_termination) { +void ebpf_domain_t::operator()(const basic_block_t& bb, bool check_termination, int print) { for (const Instruction& statement : bb) { std::visit(*this, statement); } @@ -542,7 +542,7 @@ void ebpf_domain_t::check_access_shared(NumAbsDomain& inv, const linear_expressi require(inv, ub <= region_size, std::string("Upper bound must be at most ") + region_size.name() + s); } -void ebpf_domain_t::operator()(const Assume& s) { +void ebpf_domain_t::operator()(const Assume& s, location_t loc, int print) { Condition cond = s.cond; auto dst = reg_pack(cond.left); if (std::holds_alternative(cond.right)) { @@ -573,9 +573,9 @@ void ebpf_domain_t::operator()(const Assume& s) { } } -void ebpf_domain_t::operator()(const Undefined& a) {} +void ebpf_domain_t::operator()(const Undefined& a, location_t loc, int print) {} -void ebpf_domain_t::operator()(const Un& stmt) { +void ebpf_domain_t::operator()(const Un& stmt, location_t loc, int print) { auto dst = reg_pack(stmt.dst); switch (stmt.op) { case Un::Op::BE16: @@ -594,31 +594,31 @@ void ebpf_domain_t::operator()(const Un& stmt) { } } -void ebpf_domain_t::operator()(const Exit& a) {} +void ebpf_domain_t::operator()(const Exit& a, location_t loc, int print) {} -void ebpf_domain_t::operator()(const Jmp& a) {} +void ebpf_domain_t::operator()(const Jmp& a, location_t loc, int print) {} -void ebpf_domain_t::operator()(const Comparable& s) { +void ebpf_domain_t::operator()(const Comparable& s, location_t loc, int print) { if (!type_inv.same_type(m_inv, s.r1, s.r2)) require(m_inv, linear_constraint_t::FALSE(), to_string(s)); } -void ebpf_domain_t::operator()(const Addable& s) { +void ebpf_domain_t::operator()(const Addable& s, location_t loc, int print) { if (!type_inv.implies_type(m_inv, type_is_pointer(reg_pack(s.ptr)), type_is_number(s.num))) require(m_inv, linear_constraint_t::FALSE(), "only numbers can be added to pointers (" + to_string(s) + ")"); } -void ebpf_domain_t::operator()(const ValidStore& s) { +void ebpf_domain_t::operator()(const ValidStore& s, location_t loc, int print) { if (!type_inv.implies_type(m_inv, type_is_not_stack(reg_pack(s.mem)), type_is_number(s.val))) require(m_inv, linear_constraint_t::FALSE(), "Only numbers can be stored to externally-visible regions"); } -void ebpf_domain_t::operator()(const TypeConstraint& s) { +void ebpf_domain_t::operator()(const TypeConstraint& s, location_t loc, int print) { if (!type_inv.is_in_group(m_inv, s.reg, s.types)) require(m_inv, linear_constraint_t::FALSE(), to_string(s)); } -void ebpf_domain_t::operator()(const ValidSize& s) { +void ebpf_domain_t::operator()(const ValidSize& s, location_t loc, int print) { using namespace crab::dsl_syntax; auto r = reg_pack(s.reg); require(m_inv, s.can_be_zero ? r.value >= 0 : r.value > 0, to_string(s)); @@ -727,7 +727,7 @@ crab::interval_t ebpf_domain_t::get_map_max_entries(const Reg& map_fd_reg) const return result; } -void ebpf_domain_t::operator()(const ValidMapKeyValue& s) { +void ebpf_domain_t::operator()(const ValidMapKeyValue& s, location_t loc, int print) { using namespace crab::dsl_syntax; auto fd_type = get_map_type(s.map_fd_reg); @@ -791,7 +791,7 @@ void ebpf_domain_t::operator()(const ValidMapKeyValue& s) { }); } -void ebpf_domain_t::operator()(const ValidAccess& s) { +void ebpf_domain_t::operator()(const ValidAccess& s, location_t loc, int print) { using namespace crab::dsl_syntax; bool is_comparison_check = s.width == (Value)Imm{0}; @@ -841,18 +841,18 @@ void ebpf_domain_t::operator()(const ValidAccess& s) { }); } -void ebpf_domain_t::operator()(const ZeroOffset& s) { +void ebpf_domain_t::operator()(const ZeroOffset& s, location_t loc, int print) { using namespace crab::dsl_syntax; auto reg = reg_pack(s.reg); require(m_inv, reg.offset == 0, to_string(s)); } -void ebpf_domain_t::operator()(const Assert& stmt) { +void ebpf_domain_t::operator()(const Assert& stmt, location_t loc, int print) { if (check_require || thread_local_options.assume_assertions) std::visit(*this, stmt.cst); } -void ebpf_domain_t::operator()(const Packet& a) { +void ebpf_domain_t::operator()(const Packet& a, location_t loc, int print) { auto reg = reg_pack(R0_RETURN_VALUE); type_inv.assign_type(m_inv, Reg{(uint8_t)R0_RETURN_VALUE}, T_NUM); havoc(reg.offset); @@ -1002,7 +1002,7 @@ void ebpf_domain_t::do_store_stack(NumAbsDomain& inv, int width, const A& addr, } } -void ebpf_domain_t::operator()(const Mem& b) { +void ebpf_domain_t::operator()(const Mem& b, location_t loc, int print) { if (m_inv.is_bottom()) return; if (std::holds_alternative(b.value)) { @@ -1039,11 +1039,11 @@ void ebpf_domain_t::do_mem_store(const Mem& b, Type val_type, Value val_value, s }); } -void ebpf_domain_t::operator()(const LockAdd& a) { +void ebpf_domain_t::operator()(const LockAdd& a, location_t loc, int print) { // nothing to do here } -void ebpf_domain_t::operator()(const Call& call) { +void ebpf_domain_t::operator()(const Call& call, location_t loc, int print) { using namespace crab::dsl_syntax; if (m_inv.is_bottom()) return; @@ -1141,7 +1141,7 @@ void ebpf_domain_t::do_load_mapfd(const Reg& dst_reg, int mapfd, bool maybe_null assign_valid_ptr(dst_reg, maybe_null); } -void ebpf_domain_t::operator()(const LoadMapFd& ins) { do_load_mapfd(ins.dst, ins.mapfd, false); } +void ebpf_domain_t::operator()(const LoadMapFd& ins, location_t loc, int print) { do_load_mapfd(ins.dst, ins.mapfd, false); } void ebpf_domain_t::assign_valid_ptr(const Reg& dst_reg, bool maybe_null) { using namespace crab::dsl_syntax; @@ -1155,7 +1155,7 @@ void ebpf_domain_t::assign_valid_ptr(const Reg& dst_reg, bool maybe_null) { m_inv += reg.value <= PTR_MAX; } -void ebpf_domain_t::operator()(const Bin& bin) { +void ebpf_domain_t::operator()(const Bin& bin, location_t loc, int print) { using namespace crab::dsl_syntax; auto dst = reg_pack(bin.dst); diff --git a/src/crab/ebpf_domain.hpp b/src/crab/ebpf_domain.hpp index ce8c02aae..47fc52490 100644 --- a/src/crab/ebpf_domain.hpp +++ b/src/crab/ebpf_domain.hpp @@ -15,6 +15,7 @@ #include "string_constraints.hpp" class ebpf_domain_t final { + using location_t = boost::optional>; public: ebpf_domain_t(); // Create an instance ebpf domain that resembles the initial state @@ -36,27 +37,27 @@ class ebpf_domain_t final { ebpf_domain_t narrow(const ebpf_domain_t& other) const; // Abstract transformers - void operator()(const basic_block_t& bb, bool check_termination); - void operator()(const Addable&); - void operator()(const Assert&); - void operator()(const Assume&); - void operator()(const Bin&); - void operator()(const Call&); - void operator()(const Comparable&); - void operator()(const Exit&); - void operator()(const Jmp&); - void operator()(const LoadMapFd&); - void operator()(const LockAdd&); - void operator()(const Mem&); - void operator()(const Packet&); - void operator()(const TypeConstraint&); - void operator()(const Un&); - void operator()(const Undefined&); - void operator()(const ValidAccess&); - void operator()(const ValidMapKeyValue&); - void operator()(const ValidSize&); - void operator()(const ValidStore&); - void operator()(const ZeroOffset&); + void operator()(const basic_block_t& bb, bool check_termination, int print = 0); + void operator()(const Addable&, location_t loc = boost::none, int print = 0); + void operator()(const Assert&, location_t loc = boost::none, int print = 0); + void operator()(const Assume&, location_t loc = boost::none, int print = 0); + void operator()(const Bin&, location_t loc = boost::none, int print = 0); + void operator()(const Call&, location_t loc = boost::none, int print = 0); + void operator()(const Comparable&, location_t loc = boost::none, int print = 0); + void operator()(const Exit&, location_t loc = boost::none, int print = 0); + void operator()(const Jmp&, location_t loc = boost::none, int print = 0); + void operator()(const LoadMapFd&, location_t loc = boost::none, int print = 0); + void operator()(const LockAdd&, location_t loc = boost::none, int print = 0); + void operator()(const Mem&, location_t loc = boost::none, int print = 0); + void operator()(const Packet&, location_t loc = boost::none, int print = 0); + void operator()(const TypeConstraint&, location_t loc = boost::none, int print = 0); + void operator()(const Un&, location_t loc = boost::none, int print = 0); + void operator()(const Undefined&, location_t loc = boost::none, int print = 0); + void operator()(const ValidAccess&, location_t loc = boost::none, int print = 0); + void operator()(const ValidMapKeyValue&, location_t loc = boost::none, int print = 0); + void operator()(const ValidSize&, location_t loc = boost::none, int print = 0); + void operator()(const ValidStore&, location_t loc = boost::none, int print = 0); + void operator()(const ZeroOffset&, location_t loc = boost::none, int print = 0); void write(std::ostream& o) const; std::string domain_name() const; diff --git a/src/crab/interval.hpp b/src/crab/interval.hpp index f8cee786e..30bb7f3a6 100644 --- a/src/crab/interval.hpp +++ b/src/crab/interval.hpp @@ -219,8 +219,6 @@ class interval_t final { [[nodiscard]] std::optional finite_size() const { return (_ub - _lb).number(); } private: - interval_t() : _lb(0), _ub(-1) {} - static number_t abs(const number_t& x) { return x < 0 ? -x : x; } static number_t max(const number_t& x, const number_t& y) { return x.operator<=(y) ? y : x; } @@ -228,6 +226,8 @@ class interval_t final { static number_t min(const number_t& x, const number_t& y) { return x.operator<(y) ? x : y; } public: + interval_t() : _lb(0), _ub(-1) {} + interval_t(const bound_t& lb, const bound_t& ub) : _lb(lb > ub ? bound_t{0} : lb), _ub(lb > ub ? bound_t{-1} : ub) { } diff --git a/src/crab/interval_prop_domain.cpp b/src/crab/interval_prop_domain.cpp new file mode 100644 index 000000000..f30be2e04 --- /dev/null +++ b/src/crab/interval_prop_domain.cpp @@ -0,0 +1,784 @@ +// Copyright (c) Prevail Verifier contributors. +// SPDX-License-Identifier: MIT + +#include "crab/interval_prop_domain.hpp" + +namespace std { + template <> + struct hash { + size_t operator()(const crab::reg_with_loc_t& reg) const { return reg.hash(); } + }; +} + +bool registers_cp_state_t::is_bottom() const { + return m_is_bottom; +} + +bool registers_cp_state_t::is_top() const { + if (m_is_bottom) return false; + if (m_interval_env == nullptr) return true; + for (auto it : m_cur_def) { + if (it != nullptr) return false; + } + return true; +} + +void registers_cp_state_t::set_to_top() { + m_cur_def = live_registers_t{nullptr}; + m_is_bottom = false; +} + +void registers_cp_state_t::set_to_bottom() { + m_is_bottom = true; +} + +void registers_cp_state_t::insert(register_t reg, const reg_with_loc_t& reg_with_loc, + interval_t interval) { + (*m_interval_env)[reg_with_loc] = interval; + m_cur_def[reg] = std::make_shared(reg_with_loc); +} + +std::optional registers_cp_state_t::find(reg_with_loc_t reg) const { + auto it = m_interval_env->find(reg); + if (it == m_interval_env->end()) return {}; + return it->second; +} + +std::optional registers_cp_state_t::find(register_t key) const { + if (m_cur_def[key] == nullptr) return {}; + const reg_with_loc_t& reg = *(m_cur_def[key]); + return find(reg); +} + +registers_cp_state_t registers_cp_state_t::operator|(const registers_cp_state_t& other) const { + if (is_bottom() || other.is_top()) { + return other; + } else if (other.is_bottom() || is_top()) { + return *this; + } + live_registers_t intervals_joined; + location_t loc = location_t(std::make_pair(label_t(-2, -2), 0)); + for (size_t i = 0; i < m_cur_def.size(); i++) { + if (m_cur_def[i] == nullptr || other.m_cur_def[i] == nullptr) continue; + auto it1 = find(*(m_cur_def[i])); + auto it2 = other.find(*(other.m_cur_def[i])); + if (it1 && it2) { + auto interval1 = it1.value(), interval2 = it2.value(); + auto reg = reg_with_loc_t((register_t)i, loc); + intervals_joined[i] = std::make_shared(reg); + (*m_interval_env)[reg] = interval1 | interval2; + } + } + return registers_cp_state_t(std::move(intervals_joined), m_interval_env); +} + +void registers_cp_state_t::adjust_bb_for_registers(location_t loc) { + location_t old_loc = location_t(std::make_pair(label_t(-2, -2), 0)); + for (size_t i = 0; i < m_cur_def.size(); i++) { + auto new_reg = reg_with_loc_t((register_t)i, loc); + auto old_reg = reg_with_loc_t((register_t)i, old_loc); + + auto it = find((register_t)i); + if (!it) continue; + + if (*m_cur_def[i] == old_reg) + m_interval_env->erase(old_reg); + + m_cur_def[i] = std::make_shared(new_reg); + (*m_interval_env)[new_reg] = it.value(); + + } +} + +void registers_cp_state_t::operator-=(register_t var) { + if (is_bottom()) { + return; + } + m_cur_def[var] = nullptr; +} + +void registers_cp_state_t::print_all_register_types() const { + std::cout << "\tinterval types: {\n"; + for (auto const& kv : *m_interval_env) { + std::cout << "\t\t" << kv.first << " : " << kv.second << "\n"; + } + std::cout << "\t}\n"; +} + +bool stack_cp_state_t::is_bottom() const { + return m_is_bottom; +} + +bool stack_cp_state_t::is_top() const { + if (m_is_bottom) return false; + return m_interval_values.empty(); +} + +void stack_cp_state_t::set_to_top() { + m_interval_values.clear(); + m_is_bottom = false; +} + +void stack_cp_state_t::set_to_bottom() { + m_is_bottom = true; +} + +stack_cp_state_t stack_cp_state_t::top() { + return stack_cp_state_t(false); +} + +std::optional stack_cp_state_t::find(uint64_t key) const { + auto it = m_interval_values.find(key); + if (it == m_interval_values.end()) return {}; + return it->second; +} + +void stack_cp_state_t::store(uint64_t key, interval_t val, int width) { + m_interval_values[key] = std::make_pair(val, width); +} + +void stack_cp_state_t::operator-=(uint64_t key) { + auto it = find(key); + if (it) + m_interval_values.erase(key); +} + +bool stack_cp_state_t::all_numeric(uint64_t start_loc, int width) const { + auto overlapping_cells = find_overlapping_cells(start_loc, width); + if (overlapping_cells.empty()) return false; + for (std::size_t i = 0; i < overlapping_cells.size()-1; i++) { + int width_i = find(overlapping_cells[i]).value().second; + if (overlapping_cells[i]+width_i != overlapping_cells[i+1]) return false; + } + return true; +} + +void stack_cp_state_t::remove_overlap(const std::vector& keys, uint64_t start, int width) { + for (auto& key : keys) { + auto type = find(key); + auto width_key = type.value().second; + if (key < start) { + int new_width = start-key; + store(key, interval_t::top(), new_width); + } + if (key+width_key > start+width) { + int new_width = key+width_key-(start+width); + store(start+width, interval_t::top(), new_width); + } + if (key >= start) *this -= key; + } +} + +std::vector stack_cp_state_t::find_overlapping_cells(uint64_t start, int width) const { + std::vector overlapping_cells; + auto it = m_interval_values.begin(); + while (it != m_interval_values.end() && it->first < start) { + it++; + } + if (it != m_interval_values.begin()) { + it--; + auto key = it->first; + auto width_key = it->second.second; + if (key < start && key+width_key > start) overlapping_cells.push_back(key); + } + + for (; it != m_interval_values.end(); it++) { + auto key = it->first; + if (key >= start && key < start+width) overlapping_cells.push_back(key); + if (key >= start+width) break; + } + return overlapping_cells; +} + +void join_stack(const stack_cp_state_t& stack1, uint64_t key1, int& loc1, + const stack_cp_state_t& stack2, uint64_t key2, int& loc2, + interval_values_stack_t& interval_values_joined) { + auto type1 = stack1.find(key1); auto type2 = stack2.find(key2); + auto& cells1 = type1.value(); auto& cells2 = type2.value(); + int width1 = cells1.second; int width2 = cells2.second; + auto& interval1 = cells1.first; auto& interval2 = cells2.first; + if (key1 == key2) { + if (width1 == width2) { + interval_values_joined[key1] = std::make_pair(interval1 | interval2, width1); + loc1++; loc2++; + } + else if (width1 < width2) { + interval_values_joined[key1] = std::make_pair(interval_t::top(), width1); + loc1++; + } + else { + interval_values_joined[key1] = std::make_pair(interval_t::top(), width2); + loc2++; + } + } + else if (key1 > key2) { + if (key2+width2 > key1+width1) { + interval_values_joined[key1] = std::make_pair(interval_t::top(), width1); + loc1++; + } + else if (key2+width2 > key1) { + interval_values_joined[key1] = std::make_pair(interval_t::top(), key2+width2-key1); + loc2++; + } + else loc2++; + } + else { + join_stack(stack2, key2, loc2, stack1, key1, loc1, interval_values_joined); + } +} + +stack_cp_state_t stack_cp_state_t::operator|(const stack_cp_state_t& other) const { + if (is_bottom() || other.is_top()) { + return other; + } else if (other.is_bottom() || is_top()) { + return *this; + } + interval_values_stack_t interval_values_joined; + auto stack1_keys = get_keys(); + auto stack2_keys = other.get_keys(); + int i = 0, j = 0; + while (i < static_cast(stack1_keys.size()) && j < static_cast(stack2_keys.size())) { + int key1 = stack1_keys[i], key2 = stack2_keys[j]; + join_stack(*this, key1, i, other, key2, j, interval_values_joined); + } + return stack_cp_state_t(std::move(interval_values_joined)); +} + +size_t stack_cp_state_t::size() const { + return m_interval_values.size(); +} + +std::vector stack_cp_state_t::get_keys() const { + std::vector keys; + keys.reserve(size()); + + for (auto const&kv : m_interval_values) { + keys.push_back(kv.first); + } + return keys; +} + +bool interval_prop_domain_t::is_bottom() const { + if (m_is_bottom) return true; + return (m_registers_interval_values.is_bottom() || m_stack_slots_interval_values.is_bottom()); +} + +bool interval_prop_domain_t::is_top() const { + if (m_is_bottom) return false; + return (m_registers_interval_values.is_top() && m_stack_slots_interval_values.is_top()); +} + +interval_prop_domain_t interval_prop_domain_t::bottom() { + interval_prop_domain_t cp; + cp.set_to_bottom(); + return cp; +} + +void interval_prop_domain_t::set_to_bottom() { + m_is_bottom = true; +} + +void interval_prop_domain_t::set_to_top() { + m_registers_interval_values.set_to_top(); + m_stack_slots_interval_values.set_to_top(); +} + +std::optional interval_prop_domain_t::find_interval_value(register_t reg) const { + return m_registers_interval_values.find(reg); +} + +std::optional interval_prop_domain_t::find_interval_at_loc(const reg_with_loc_t reg) const { + return m_registers_interval_values.find(reg); +} + +bool interval_prop_domain_t::operator<=(const interval_prop_domain_t& abs) const { + /* WARNING: The operation is not implemented yet.*/ + return true; +} + +void interval_prop_domain_t::operator|=(const interval_prop_domain_t& abs) { + interval_prop_domain_t tmp{abs}; + operator|=(std::move(tmp)); +} + +void interval_prop_domain_t::operator|=(interval_prop_domain_t&& abs) { + if (is_bottom()) { + *this = abs; + return; + } + *this = *this | std::move(abs); +} + +interval_prop_domain_t interval_prop_domain_t::operator|(const interval_prop_domain_t& other) const { + if (is_bottom() || other.is_top()) { + return other; + } + else if (other.is_bottom() || is_top()) { + return *this; + } + return interval_prop_domain_t(m_registers_interval_values | other.m_registers_interval_values, + m_stack_slots_interval_values | other.m_stack_slots_interval_values); +} + +interval_prop_domain_t interval_prop_domain_t::operator|(interval_prop_domain_t&& other) const { + if (is_bottom() || other.is_top()) { + return std::move(other); + } + else if (other.is_bottom() || is_top()) { + return *this; + } + return interval_prop_domain_t(m_registers_interval_values | std::move(other.m_registers_interval_values), + m_stack_slots_interval_values | std::move(other.m_stack_slots_interval_values)); +} + +interval_prop_domain_t interval_prop_domain_t::operator&(const interval_prop_domain_t& abs) const { + /* WARNING: The operation is not implemented yet.*/ + return abs; +} + +interval_prop_domain_t interval_prop_domain_t::widen(const interval_prop_domain_t& abs) const { + /* WARNING: The operation is not implemented yet.*/ + return abs; +} + +interval_prop_domain_t interval_prop_domain_t::narrow(const interval_prop_domain_t& other) const { + /* WARNING: The operation is not implemented yet.*/ + return other; +} + +void interval_prop_domain_t::write(std::ostream& os) const {} + +std::string interval_prop_domain_t::domain_name() const { + return "interval_prop_domain"; +} + +int interval_prop_domain_t::get_instruction_count_upper_bound() { + /* WARNING: The operation is not implemented yet.*/ + return 0; +} + +string_invariant interval_prop_domain_t::to_set() { + return string_invariant{}; +} + +interval_prop_domain_t interval_prop_domain_t::setup_entry() { + std::shared_ptr all_intervals = std::make_shared(); + registers_cp_state_t registers(all_intervals); + + interval_prop_domain_t cp(std::move(registers), stack_cp_state_t::top()); + return cp; +} + +void interval_prop_domain_t::operator()(const Un& u, location_t loc, int print) { + auto reg_with_loc = reg_with_loc_t(u.dst.v, loc); + m_registers_interval_values.insert(u.dst.v, reg_with_loc, interval_t::top()); +} + +void interval_prop_domain_t::operator()(const LoadMapFd &u, location_t loc, int print) { + m_registers_interval_values -= u.dst.v; +} + +void interval_prop_domain_t::operator()(const ValidSize& s, location_t loc, int print) { + auto reg_v = m_registers_interval_values.find(s.reg.v); + if (reg_v) { + auto reg_value = reg_v.value(); + if ((s.can_be_zero && reg_value.lb() >= bound_t(0)) + || (!s.can_be_zero && reg_value.lb() > bound_t(0))) { + return; + } + } + std::cout << "Valid Size assertion fail\n"; +} + +void interval_prop_domain_t::do_call(const Call& u, const interval_values_stack_t& store_in_stack, + location_t loc) { + + auto r0 = register_t{R0_RETURN_VALUE}; + for (const auto& kv : store_in_stack) { + auto key = kv.first; + auto width = kv.second.second; + auto overlapping_cells + = m_stack_slots_interval_values.find_overlapping_cells(key, width); + m_stack_slots_interval_values.remove_overlap(overlapping_cells, key, width); + m_stack_slots_interval_values.store(kv.first, kv.second.first, kv.second.second); + } + if (u.is_map_lookup) { + m_registers_interval_values -= r0; + } + else { + auto r0_with_loc = reg_with_loc_t(r0, loc); + m_registers_interval_values.insert(r0, r0_with_loc, interval_t::top()); + } +} + +void interval_prop_domain_t::operator()(const Packet &u, location_t loc, int print) { + auto r0 = register_t{R0_RETURN_VALUE}; + auto r0_with_loc = reg_with_loc_t(r0, loc); + m_registers_interval_values.insert(r0, r0_with_loc, interval_t::top()); +} + +void interval_prop_domain_t::operator()(const Assume &s, location_t loc, int print) { + // TODO: generalize for intervals + using Op = Condition::Op; + Condition cond = s.cond; + int64_t imm = 0; + bool is_imm = false; + auto reg_with_loc = reg_with_loc_t(cond.left.v, loc); + auto left_reg_optional = m_registers_interval_values.find(cond.left.v); + if (!left_reg_optional) { + return; + } + auto left_value = left_reg_optional.value(); + bound_t right_value = bound_t(-1); + if (std::holds_alternative(cond.right)) { + auto reg = std::get(cond.right).v; + auto right_reg_optional = m_registers_interval_values.find(reg); + if (!right_reg_optional) { + std::cout << "type error: assumption for an unknown register\n"; + return; + } + auto right_reg = right_reg_optional.value(); + auto right_reg_singleton = right_reg.singleton(); + if (!right_reg_singleton) { + std::cout << "assumption for a non-singleton register\n"; + return; + } + right_value = right_reg_singleton.value(); + } + else { + imm = std::get(cond.right).v; + is_imm = true; + right_value = bound_t(static_cast(imm)); + } + bool is_right_within_left_interval = left_value.lb() <= right_value + && right_value <= left_value.ub(); + switch (cond.op) { + case Op::EQ: { + if (is_right_within_left_interval) + m_registers_interval_values.insert(cond.left.v, reg_with_loc, interval_t(right_value)); + return; + } + case Op::NE: { + if (right_value <= left_value.lb() || right_value >= left_value.ub()) { + if (right_value == left_value.lb()) + m_registers_interval_values.insert(cond.left.v, reg_with_loc, + interval_t(bound_t(left_value.lb() + 1), left_value.ub())); + else if (right_value == left_value.ub()) + m_registers_interval_values.insert(cond.left.v, reg_with_loc, + interval_t(left_value.lb(), bound_t(left_value.ub() - 1))); + return; + } + break; + } + case Op::SGE: + case Op::GE: + { + if (is_right_within_left_interval || right_value < left_value.lb()) { + if (is_right_within_left_interval) { + if (cond.op == Op::GE && is_imm) { + auto value = bound_t(static_cast(imm)); + m_registers_interval_values.insert(cond.left.v, reg_with_loc, + interval_t(value, left_value.ub())); + } + else { + m_registers_interval_values.insert(cond.left.v, reg_with_loc, + interval_t(right_value, left_value.ub())); + } + } + return; + } + break; + } + case Op::SLE: + case Op::LE: + { + if (is_right_within_left_interval || right_value > left_value.ub()) { + if (is_right_within_left_interval) { + if (cond.op == Op::LE && is_imm && left_value.lb() < bound_t(0)) { + m_registers_interval_values.insert(cond.left.v, reg_with_loc, + interval_t(bound_t(0), right_value)); + } + else { + m_registers_interval_values.insert(cond.left.v, reg_with_loc, + interval_t(left_value.lb(), right_value)); + } + } + return; + } + break; + } + case Op::SGT: + case Op::GT: { + auto right_value_plus_1 = right_value + bound_t(1); + bool is_right_plus_1_within_left_interval = left_value.lb() <= right_value_plus_1 + && right_value_plus_1 <= left_value.ub(); + if (is_right_plus_1_within_left_interval || right_value_plus_1 < left_value.lb()) { + if (is_right_plus_1_within_left_interval) { + if (cond.op == Op::GT && is_imm) { + auto value = bound_t(static_cast(imm)); + m_registers_interval_values.insert(cond.left.v, reg_with_loc, + interval_t(value + bound_t(1), left_value.ub())); + } + else { + m_registers_interval_values.insert(cond.left.v, reg_with_loc, + interval_t(right_value_plus_1, left_value.ub())); + } + } + return; + } + break; + } + case Op::SLT: + case Op::LT: { + auto right_value_minus_1 = right_value - bound_t(1); + bool is_right_minus_1_within_left_interval = left_value.lb() <= right_value_minus_1 + && right_value_minus_1 <= left_value.ub(); + if (is_right_minus_1_within_left_interval || right_value_minus_1 > left_value.ub()) { + if (is_right_minus_1_within_left_interval) { + if (cond.op == Op::LT && is_imm) { + auto value = bound_t(static_cast(imm)); + m_registers_interval_values.insert(cond.left.v, reg_with_loc, + interval_t(left_value.lb(), value - bound_t(1))); + } + else { + m_registers_interval_values.insert(cond.left.v, reg_with_loc, + interval_t(left_value.lb(), right_value_minus_1)); + } + } + return; + } + break; + } + default: return; + m_registers_interval_values.insert(cond.left.v, reg_with_loc, interval_t::bottom()); + } +} + +void interval_prop_domain_t::do_bin(const Bin& bin, + const std::optional& src_interval_opt, + const std::optional& dst_interval_opt, + const std::optional& src_ptr_or_mapfd_opt, + const std::optional& dst_ptr_or_mapfd_opt, + const interval_t& subtract_interval, location_t loc) { + using Op = Bin::Op; + // if op is not MOV, + // we skip handling in this domain is when dst is pointer and src is numerical value + if (bin.op != Op::MOV && dst_ptr_or_mapfd_opt && src_interval_opt) return; + // if op is MOV, + // we skip handling in this domain is when both dst and src are pointers + // when dst is not known and src is pointer + if (bin.op == Op::MOV && + ((dst_ptr_or_mapfd_opt && src_ptr_or_mapfd_opt) + || (!dst_interval_opt && src_ptr_or_mapfd_opt))) + return; + + uint64_t imm = std::holds_alternative(bin.v) ? std::get(bin.v).v : 0; + interval_t src_interval, dst_interval; + if (src_interval_opt) src_interval = std::move(src_interval_opt.value()); + if (dst_interval_opt) dst_interval = std::move(dst_interval_opt.value()); + + auto reg_with_loc = reg_with_loc_t(bin.dst.v, loc); + switch (bin.op) + { + // ra = b + case Op::MOV: { + if (src_interval_opt) + dst_interval = src_interval; + else if (dst_interval_opt) { + m_registers_interval_values -= bin.dst.v; + return; + } + break; + } + // ra += b + case Op::ADD: { + if (dst_ptr_or_mapfd_opt && src_ptr_or_mapfd_opt) return; + if (dst_interval_opt && src_interval_opt) + dst_interval += src_interval; + else if (dst_interval_opt && src_ptr_or_mapfd_opt) { + m_registers_interval_values -= bin.dst.v; + return; + } + break; + } + // ra -= b + case Op::SUB: { + if (dst_ptr_or_mapfd_opt && src_ptr_or_mapfd_opt) + dst_interval = subtract_interval; + else if (dst_interval_opt && src_interval_opt) + dst_interval -= src_interval; + else if (dst_interval_opt && src_ptr_or_mapfd_opt) { + m_registers_interval_values -= bin.dst.v; + return; + } + break; + } + // ra *= b + case Op::MUL: { + dst_interval *= src_interval; + break; + } + // ra /= b + case Op::DIV: { + dst_interval /= src_interval; + break; + } + // ra %= b + case Op::MOD: { + dst_interval = dst_interval.SRem(src_interval); + break; + } + // ra |= b + case Op::OR: { + dst_interval = dst_interval.Or(src_interval); + break; + } + // ra &= b + case Op::AND: { + dst_interval = dst_interval.And(src_interval); + if ((int32_t)imm > 0) + dst_interval = interval_t(number_t(0), number_t(static_cast(imm))); + break; + } + // ra <<= b + case Op::LSH: { + dst_interval = dst_interval.Shl(src_interval); + break; + } + // ra >>= b + case Op::RSH: { + dst_interval = dst_interval.LShr(src_interval); + break; + } + // ra >>>= b + case Op::ARSH: { + dst_interval = dst_interval.AShr(src_interval); + break; + } + // ra ^= b + case Op::XOR: { + dst_interval = dst_interval.Xor(src_interval); + break; + } + default: { + dst_interval = interval_t::top(); + break; + } + } + m_registers_interval_values.insert(bin.dst.v, reg_with_loc, dst_interval); +} + + +void interval_prop_domain_t::do_load(const Mem& b, const Reg& target_reg, + std::optional basereg_type, std::optional targetreg_type, + location_t loc) { + if (!basereg_type) { + m_registers_interval_values -= target_reg.v; + return; + } + + auto basereg_ptr_or_mapfd_type = basereg_type.value(); + int offset = b.access.offset; + int width = b.access.width; + + auto reg_with_loc = reg_with_loc_t(target_reg.v, loc); + if (std::holds_alternative(basereg_ptr_or_mapfd_type)) { + auto p_with_off = std::get(basereg_ptr_or_mapfd_type); + if (p_with_off.get_region() == crab::region_t::T_STACK) { + auto ptr_offset = p_with_off.get_offset(); + auto load_at_interval = ptr_offset + number_t(static_cast(offset)); + auto load_at_singleton = load_at_interval.singleton(); + if (load_at_singleton) { + auto load_at = load_at_singleton.value(); + auto loaded = m_stack_slots_interval_values.find((uint64_t)load_at); + if (loaded) { + auto loaded_cells = loaded.value(); + m_registers_interval_values.insert(target_reg.v, reg_with_loc, + loaded_cells.first); + return; + } + } + auto load_at_lb_opt = load_at_interval.lb().number(); + auto load_at_ub_opt = load_at_interval.ub().number(); + if (!load_at_lb_opt || !load_at_ub_opt) { + m_registers_interval_values -= target_reg.v; + std::cout << "type error: missing offset information\n"; + return; + } + auto load_at_lb = load_at_lb_opt.value(); + auto load_at_ub = load_at_ub_opt.value(); + auto start = (uint64_t)load_at_lb; + auto width_to_check = (int)(load_at_ub+number_t(width)-load_at_lb); + + if (m_stack_slots_interval_values.all_numeric(start, width_to_check)) { + m_registers_interval_values.insert(target_reg.v, reg_with_loc, + interval_t::top()); + } + else { + m_registers_interval_values -= target_reg.v; + } + return; + } + } + // we check targetreg_type because in case we already loaded a pointer from ctx, + // we then do not store a number + if (!targetreg_type) { // we are loading from ctx, packet or shared + m_registers_interval_values.insert(target_reg.v, reg_with_loc, interval_t::top()); + } + else { + m_registers_interval_values -= target_reg.v; + } +} + +void interval_prop_domain_t::do_mem_store(const Mem& b, const Reg& target_reg, + std::optional basereg_type) { + int offset = b.access.offset; + int width = b.access.width; + + if (!basereg_type) { + return; + } + auto basereg_ptr_or_mapfd_type = basereg_type.value(); + auto targetreg_type = m_registers_interval_values.find(target_reg.v); + if (std::holds_alternative(basereg_ptr_or_mapfd_type)) { + auto basereg_ptr_with_off_type = std::get(basereg_ptr_or_mapfd_type); + auto offset_singleton = basereg_ptr_with_off_type.get_offset().singleton(); + if (!offset_singleton) { + std::cout << "doing a store with unknown offset\n"; + return; + } + auto store_at = (uint64_t)offset_singleton.value() + (uint64_t)offset; + if (basereg_ptr_with_off_type.get_region() == crab::region_t::T_STACK) { + auto overlapping_cells + = m_stack_slots_interval_values.find_overlapping_cells(store_at, width); + m_stack_slots_interval_values.remove_overlap(overlapping_cells, store_at, width); + + // if targetreg_type is empty, we are storing a pointer + if (!targetreg_type) return; + + auto type_to_store = targetreg_type.value(); + m_stack_slots_interval_values.store(store_at, type_to_store, width); + } + } + else {} +} + +std::optional interval_prop_domain_t::find_in_stack(uint64_t key) const { + return m_stack_slots_interval_values.find(key); +} + +void interval_prop_domain_t::adjust_bb_for_types(location_t loc) { + m_registers_interval_values.adjust_bb_for_registers(loc); +} + +void interval_prop_domain_t::print_all_register_types() const { + m_registers_interval_values.print_all_register_types(); +} + +std::vector interval_prop_domain_t::get_stack_keys() const { + return m_stack_slots_interval_values.get_keys(); +} + +bool interval_prop_domain_t::all_numeric_in_stack(uint64_t start_loc, int width) const { + return m_stack_slots_interval_values.all_numeric(start_loc, width); +} diff --git a/src/crab/interval_prop_domain.hpp b/src/crab/interval_prop_domain.hpp new file mode 100644 index 000000000..ddc2ec7af --- /dev/null +++ b/src/crab/interval_prop_domain.hpp @@ -0,0 +1,167 @@ +// Copyright (c) Prevail Verifier contributors. +// SPDX-License-Identifier: MIT + +#pragma once + +#include +#include + +#include "crab/abstract_domain.hpp" +#include "crab/region_domain.hpp" +#include "crab/cfg.hpp" +#include "linear_constraint.hpp" +#include "string_constraints.hpp" + +using crab::ptr_t; +using crab::ptr_or_mapfd_t; +using crab::mapfd_t; +using crab::ptr_with_off_t; +using crab::ptr_no_off_t; +using crab::reg_with_loc_t; +using crab::interval_t; +using crab::bound_t; +using crab::region_t; + +using live_registers_t = std::array, 11>; +using global_interval_env_t = std::unordered_map; + +class registers_cp_state_t { + + live_registers_t m_cur_def; + std::shared_ptr m_interval_env; + bool m_is_bottom = false; + + public: + bool is_bottom() const; + bool is_top() const; + void set_to_bottom(); + void set_to_top(); + std::optional find(reg_with_loc_t reg) const; + std::optional find(register_t key) const; + void insert(register_t, const reg_with_loc_t&, interval_t); + void operator-=(register_t); + registers_cp_state_t operator|(const registers_cp_state_t& other) const; + registers_cp_state_t(bool is_bottom = false) : m_interval_env(nullptr), + m_is_bottom(is_bottom) {} + explicit registers_cp_state_t(live_registers_t&& vars, + std::shared_ptr interval_env, bool is_bottom = false) + : m_cur_def(std::move(vars)), m_interval_env(interval_env), m_is_bottom(is_bottom) {} + explicit registers_cp_state_t(std::shared_ptr interval_env, + bool is_bottom = false) + : m_interval_env(interval_env), m_is_bottom(is_bottom) {} + void adjust_bb_for_registers(location_t); + void print_all_register_types() const; +}; + +using interval_cells_t = std::pair; // intervals with width +using interval_values_stack_t = std::map; + +class stack_cp_state_t { + + interval_values_stack_t m_interval_values; + bool m_is_bottom = false; + + public: + bool is_bottom() const; + bool is_top() const; + void set_to_bottom(); + void set_to_top(); + static stack_cp_state_t top(); + std::optional find(uint64_t) const; + void store(uint64_t, interval_t, int); + void operator-=(uint64_t); + bool all_numeric(uint64_t, int) const; + stack_cp_state_t operator|(const stack_cp_state_t& other) const; + stack_cp_state_t(bool is_bottom = false) : m_is_bottom(is_bottom) {} + explicit stack_cp_state_t(interval_values_stack_t&& interval_values, bool is_bottom = false) + : m_interval_values(std::move(interval_values)), m_is_bottom(is_bottom) {} + std::vector get_keys() const; + size_t size() const; + std::vector find_overlapping_cells(uint64_t, int) const; + void remove_overlap(const std::vector&, uint64_t, int); +}; + +class interval_prop_domain_t final { + registers_cp_state_t m_registers_interval_values; + stack_cp_state_t m_stack_slots_interval_values; + bool m_is_bottom = false; + + public: + + interval_prop_domain_t() = default; + interval_prop_domain_t(interval_prop_domain_t&& o) = default; + interval_prop_domain_t(const interval_prop_domain_t& o) = default; + explicit interval_prop_domain_t(registers_cp_state_t&& consts_regs, + stack_cp_state_t&& interval_stack_slots, bool is_bottom = false) : + m_registers_interval_values(std::move(consts_regs)), m_stack_slots_interval_values(std::move(interval_stack_slots)), + m_is_bottom(is_bottom) {} + interval_prop_domain_t& operator=(interval_prop_domain_t&& o) = default; + interval_prop_domain_t& operator=(const interval_prop_domain_t& o) = default; + // eBPF initialization: R1 points to ctx, R10 to stack, etc. + static interval_prop_domain_t setup_entry(); + // bottom/top + static interval_prop_domain_t bottom(); + void set_to_top(); + void set_to_bottom(); + bool is_bottom() const; + bool is_top() const; + // inclusion + bool operator<=(const interval_prop_domain_t& other) const; + // join + void operator|=(const interval_prop_domain_t& abs); + void operator|=(interval_prop_domain_t&& abs); + interval_prop_domain_t operator|(const interval_prop_domain_t& other) const; + interval_prop_domain_t operator|(interval_prop_domain_t&& abs) const; + // meet + interval_prop_domain_t operator&(const interval_prop_domain_t& other) const; + // widening + interval_prop_domain_t widen(const interval_prop_domain_t& other) const; + // narrowing + interval_prop_domain_t narrow(const interval_prop_domain_t& other) const; + //forget + void operator-=(variable_t var); + void operator-=(register_t reg) { m_registers_interval_values -= reg; } + + //// abstract transformers + void operator()(const Undefined &, location_t loc = boost::none, int print = 0) {} + void operator()(const Bin &, location_t loc = boost::none, int print = 0) {} + void operator()(const Un &, location_t loc = boost::none, int print = 0); + void operator()(const LoadMapFd &, location_t loc = boost::none, int print = 0); + void operator()(const Call &, location_t loc = boost::none, int print = 0) {} + void operator()(const Exit &, location_t loc = boost::none, int print = 0) {} + void operator()(const Jmp &, location_t loc = boost::none, int print = 0) {} + void operator()(const Mem &, location_t loc = boost::none, int print = 0) {} + void operator()(const Packet &, location_t loc = boost::none, int print = 0); + void operator()(const LockAdd &, location_t loc = boost::none, int print = 0) {} + void operator()(const Assume &, location_t loc = boost::none, int print = 0); + void operator()(const Assert &, location_t loc = boost::none, int print = 0) {} + void operator()(const ValidAccess&, location_t loc = boost::none, int print = 0) {} + void operator()(const Comparable& s, location_t loc = boost::none, int print = 0) {} + void operator()(const Addable& s, location_t loc = boost::none, int print = 0) {} + void operator()(const ValidStore& s, location_t loc = boost::none, int print = 0) {} + void operator()(const TypeConstraint& s, location_t loc = boost::none, int print = 0) {} + void operator()(const ValidSize& s, location_t loc = boost::none, int print = 0); + void operator()(const ValidMapKeyValue& s, location_t loc = boost::none, int print = 0) {} + void operator()(const ZeroOffset& s, location_t loc = boost::none, int print = 0) {} + void operator()(const basic_block_t& bb, bool check_termination, int print = 0) {} + void write(std::ostream& os) const; + std::string domain_name() const; + int get_instruction_count_upper_bound(); + string_invariant to_set(); + void set_require_check(check_require_func_t f) {} + + void do_load(const Mem&, const Reg&, std::optional, + std::optional, location_t); + void do_mem_store(const Mem&, const Reg&, std::optional); + void do_call(const Call&, const interval_values_stack_t&, location_t); + void do_bin(const Bin&, const std::optional&, const std::optional&, + const std::optional&, const std::optional&, + const interval_t&, location_t); + std::optional find_interval_value(register_t) const; + std::optional find_interval_at_loc(const reg_with_loc_t reg) const; + std::optional find_in_stack(uint64_t) const; + void adjust_bb_for_types(location_t); + void print_all_register_types() const; + std::vector get_stack_keys() const; + bool all_numeric_in_stack(uint64_t, int) const; +}; // end interval_prop_domain_t diff --git a/src/crab/offset_domain.cpp b/src/crab/offset_domain.cpp new file mode 100644 index 000000000..d3fba51b7 --- /dev/null +++ b/src/crab/offset_domain.cpp @@ -0,0 +1,947 @@ +// Copyright (c) Prevail Verifier contributors. +// SPDX-License-Identifier: MIT + +#include "crab/offset_domain.hpp" + +namespace std { + template <> + struct hash { + size_t operator()(const crab::reg_with_loc_t& reg) const { return reg.hash(); } + }; +} + +bool dist_t::operator==(const dist_t& d) const { + return (m_dist == d.m_dist && m_slack == d.m_slack); +} + +weight_t dist_t::offset_from_reference() const { + if (is_meta_pointer()) { + return (-m_dist+PACKET_META); + } + if (is_backward_pointer()) { + return (m_dist-PACKET_END); + } + return m_dist; +} + +void dist_t::write(std::ostream& o) const { + if (m_slack != -1) + o << "s" << m_slack << "+"; + if (is_forward_pointer()) o << "begin+"; + else if (is_meta_pointer()) o << "meta+"; + else if (is_backward_pointer()) o << "end+"; + auto offset = offset_from_reference(); + auto singleton_val = offset.singleton(); + if (singleton_val) o << singleton_val.value(); + else o << offset; +} + +bool dist_t::is_top() const { + if (m_is_bottom) return false; + return (m_slack == -1 && m_dist.is_top()); +} + +bool dist_t::is_bottom() const { + return m_is_bottom; +} + +void dist_t::set_to_top() { + m_slack = -1; + m_dist = interval_t::top(); + m_is_bottom = false; +} + +void dist_t::set_to_bottom() { + m_is_bottom = true; +} + +bool dist_t::is_meta_pointer() const { + return (m_dist.lb() > PACKET_END && m_dist.ub() <= PACKET_META); +} +bool dist_t::is_forward_pointer() const { + return (m_dist.lb() >= PACKET_BEGIN); +} +bool dist_t::is_backward_pointer() const { + return (m_dist.ub() <= PACKET_END); +} + +std::ostream& operator<<(std::ostream& o, const dist_t& d) { + d.write(o); + return o; +} + +bool inequality_t::is_top() const { + if (m_is_bottom) return false; + return (m_slack == -1 && m_value.is_top()); +} + +bool inequality_t::is_bottom() const { + return m_is_bottom; +} + +void inequality_t::set_to_top() { + m_value = interval_t::top(); + m_slack = -1; + m_is_bottom = false; +} + +void inequality_t::set_to_bottom() { + m_is_bottom = true; +} + + +std::ostream& operator<<(std::ostream& o, const inequality_t& ineq) { + ineq.write(o); + return o; +} + +void inequality_t::write(std::ostream& o) const { + o << m_slack << (m_rel == rop_t::R_GT ? ">" : + m_rel == rop_t::R_GE ? ">=" : + m_rel == rop_t::R_LT ? "<" : "<=") + << m_value; +} + +bool equality_t::is_top() const { + if (m_is_bottom) return false; + return (m_lhs.is_top() && m_rhs.is_top()); +} + +bool equality_t::is_bottom() const { + return m_is_bottom; +} + +void equality_t::set_to_top() { + m_lhs.set_to_top(); + m_rhs.set_to_top(); + m_is_bottom = false; +} + +void equality_t::set_to_bottom() { + m_is_bottom = true; +} + +std::ostream& operator<<(std::ostream& o, const equality_t& eq) { + eq.write(o); + return o; +} + +void equality_t::write(std::ostream& o) const { + o << m_lhs << " = " << m_rhs; +} + +void registers_state_t::insert(register_t reg, const reg_with_loc_t& reg_with_loc, + const dist_t& dist) { + (*m_offset_env)[reg_with_loc] = dist; + m_cur_def[reg] = std::make_shared(reg_with_loc); +} + +std::optional registers_state_t::find(reg_with_loc_t reg) const { + auto it = m_offset_env->find(reg); + if (it == m_offset_env->end()) return {}; + return it->second; +} + +std::optional registers_state_t::find(register_t key) const { + if (m_cur_def[key] == nullptr) return {}; + const reg_with_loc_t& reg = *(m_cur_def[key]); + return find(reg); +} + +void registers_state_t::set_to_top() { + m_cur_def = live_registers_t{nullptr}; + m_is_bottom = false; +} + +void registers_state_t::set_to_bottom() { + m_cur_def = live_registers_t{nullptr}; + m_is_bottom = true; +} + +bool registers_state_t::is_top() const { + if (m_is_bottom) return false; + if (m_offset_env == nullptr) return true; + for (auto &it : m_cur_def) { + if (it != nullptr) return false; + } + return true; +} + +bool registers_state_t::is_bottom() const { + return m_is_bottom; +} + +void registers_state_t::operator-=(register_t to_forget) { + if (is_bottom()) { + return; + } + m_cur_def[to_forget] = nullptr; +} + +registers_state_t registers_state_t::operator|(const registers_state_t& other) const { + if (is_bottom() || other.is_top()) { + return other; + } else if (other.is_bottom() || is_top()) { + return *this; + } + live_registers_t out_vars; + location_t loc = location_t(std::make_pair(label_t(-2, -2), 0)); + + for (size_t i = 0; i < m_cur_def.size(); i++) { + if (m_cur_def[i] == nullptr || other.m_cur_def[i] == nullptr) continue; + auto it1 = find(*(m_cur_def[i])); + auto it2 = other.find(*(other.m_cur_def[i])); + if (it1 && it2) { + dist_t dist1 = it1.value(), dist2 = it2.value(); + auto reg = reg_with_loc_t((register_t)i, loc); + if (dist1.m_slack != dist2.m_slack) continue; + auto dist_joined = dist_t(std::move(dist1.m_dist | dist2.m_dist), dist1.m_slack); + out_vars[i] = std::make_shared(reg); + (*m_offset_env)[reg] = dist_joined; + } + } + return registers_state_t(std::move(out_vars), m_offset_env, false); +} + +void registers_state_t::adjust_bb_for_registers(location_t loc) { + location_t old_loc = location_t(std::make_pair(label_t(-2, -2), 0)); + for (size_t i = 0; i < m_cur_def.size(); i++) { + auto new_reg = reg_with_loc_t((register_t)i, loc); + auto old_reg = reg_with_loc_t((register_t)i, old_loc); + + auto it = find((register_t)i); + if (!it) continue; + + if (*m_cur_def[i] == old_reg) + m_offset_env->erase(old_reg); + + m_cur_def[i] = std::make_shared(new_reg); + (*m_offset_env)[new_reg] = it.value(); + } +} + +void registers_state_t::print_all_register_types() const { + std::cout << "\toffset types: {\n"; + for (auto const& kv : *m_offset_env) { + std::cout << "\t\t" << kv.first << " : " << kv.second << "\n"; + } + std::cout << "\t}\n"; +} + +void stack_state_t::set_to_top() { + m_slot_dists.clear(); + m_is_bottom = false; +} + +void stack_state_t::set_to_bottom() { + m_slot_dists.clear(); + m_is_bottom = true; +} + +bool stack_state_t::is_top() const { + if (m_is_bottom) return false; + return m_slot_dists.empty(); +} + +bool stack_state_t::is_bottom() const { + return m_is_bottom; +} + +stack_state_t stack_state_t::top() { + return stack_state_t(false); +} + +std::optional stack_state_t::find(int key) const { + auto it = m_slot_dists.find(key); + if (it == m_slot_dists.end()) return {}; + return it->second; +} + +void stack_state_t::store(int key, dist_t d) { + m_slot_dists[key] = d; +} + +void stack_state_t::operator-=(int to_erase) { + if (is_bottom()) { + return; + } + m_slot_dists.erase(to_erase); +} + +stack_state_t stack_state_t::operator|(const stack_state_t& other) const { + if (is_bottom() || other.is_top()) { + return other; + } else if (other.is_bottom() || is_top()) { + return *this; + } + stack_slot_dists_t out_stack_dists; + for (auto const&kv: m_slot_dists) { + auto it = other.m_slot_dists.find(kv.first); + if (it != m_slot_dists.end() && kv.second == it->second) + out_stack_dists.insert(kv); + } + return stack_state_t(std::move(out_stack_dists), false); +} + +bool extra_constraints_t::is_top() const { + if (m_is_bottom) return false; + return (m_meta_and_begin.is_top() && m_begin_and_end.is_top()); +} + +bool extra_constraints_t::is_bottom() const { + return m_is_bottom; +} + +void extra_constraints_t::set_to_top() { + m_meta_and_begin.set_to_top(); + m_begin_and_end.set_to_top(); + m_is_bottom = false; +} + +void extra_constraints_t::set_to_bottom() { + m_is_bottom = true; +} + +void extra_constraints_t::add_meta_and_begin_constraint(equality_t&& eq, + inequality_t&& ineq) { + m_meta_and_begin = packet_constraint_t(std::move(eq), std::move(ineq), true); +} + +void extra_constraints_t::add_begin_and_end_constraint(equality_t&& eq, + inequality_t&& ineq) { + m_begin_and_end = packet_constraint_t(std::move(eq), std::move(ineq), false); +} +/* +void extra_constraints_t::normalize() { + weight_t dist_lhs = m_eq.m_lhs.m_dist - m_eq.m_rhs.m_dist - 4099; + weight_t dist_rhs = -4099; + slack_var_t s = m_eq.m_lhs.m_slack; + dist_lhs += m_ineq.m_value; + weight_t ineq_val = 0; + rop_t ineq_rel = m_ineq.m_rel; + + m_eq = equality_t(dist_t(dist_lhs, s), dist_t(dist_rhs)); + m_ineq = inequality_t(s, ineq_rel, ineq_val); +} +*/ + +packet_constraint_t packet_constraint_t::operator|(const packet_constraint_t& other) const { + //normalize(); + //other.normalize(); + + weight_t dist1 = m_eq.m_lhs.m_dist; + weight_t dist2 = other.m_eq.m_lhs.m_dist; + slack_var_t s = m_eq.m_lhs.m_slack; + + dist_t lhs = dist_t(dist1 | dist2, s); + dist_t rhs; + if (m_is_meta_constraint) rhs = dist_t(weight_t(number_t(PACKET_BEGIN))); + else rhs = dist_t(weight_t(number_t(PACKET_END))); + + equality_t out_eq(lhs, rhs); + inequality_t out_ineq(s, m_ineq.m_rel, weight_t(number_t(0))); + return packet_constraint_t(std::move(out_eq), std::move(out_ineq), m_is_meta_constraint); + // have to handle case for different slack vars +} + +std::ostream& operator<<(std::ostream& o, const packet_constraint_t& p) { + p.write(o); + return o; +} + +void packet_constraint_t::write(std::ostream& o) const { + o << m_eq << "\n"; + o << m_ineq << "\n"; +} + +void packet_constraint_t::set_to_top() { + m_eq.set_to_top(); + m_ineq.set_to_top(); + m_is_bottom = false; +} + +void packet_constraint_t::set_to_bottom() { + m_is_bottom = true; +} + +bool packet_constraint_t::is_top() const { + if (m_is_bottom) return false; + return (m_eq.is_top() && m_ineq.is_top()); +} + +bool packet_constraint_t::is_bottom() const { + return m_is_bottom; +} + +std::optional packet_constraint_t::get_limit() const { + // TODO: normalize constraint, if required + auto dist = m_eq.m_lhs.m_dist; + if (dist.is_top()) return {}; + return dist.ub(); +} + +extra_constraints_t extra_constraints_t::operator|(const extra_constraints_t& other) const { + auto meta_and_begin = m_meta_and_begin | other.m_meta_and_begin; + auto begin_and_end = m_begin_and_end | other.m_begin_and_end; + return extra_constraints_t(std::move(meta_and_begin), std::move(begin_and_end), false); +} + +std::optional extra_constraints_t::get_end_limit() const { + return m_begin_and_end.get_limit(); +} + +std::optional extra_constraints_t::get_meta_limit() const { + return m_meta_and_begin.get_limit(); +} + +ctx_t::ctx_t(const ebpf_context_descriptor_t* desc) { + if (desc->data >= 0) { + m_dists[desc->data] = dist_t(weight_t(number_t(PACKET_BEGIN))); + } + if (desc->end >= 0) { + m_dists[desc->end] = dist_t(weight_t(number_t(PACKET_END))); + } + if (desc->meta >= 0) { + m_dists[desc->meta] = dist_t(weight_t(number_t(PACKET_META))); + } + m_size = desc->size; +} + +int ctx_t::get_size() const { + return m_size; +} + +std::optional ctx_t::find(uint64_t key) const { + auto it = m_dists.find(key); + if (it == m_dists.end()) return {}; + return it->second; +} + +offset_domain_t offset_domain_t::setup_entry() { + std::shared_ptr ctx = std::make_shared(global_program_info.type.context_descriptor); + std::shared_ptr all_types = std::make_shared(); + registers_state_t regs(all_types); + + offset_domain_t off_d(std::move(regs), stack_state_t::top(), ctx); + return off_d; +} + +offset_domain_t offset_domain_t::bottom() { + offset_domain_t off; + off.set_to_bottom(); + return off; +} + +void offset_domain_t::set_to_top() { + m_reg_state.set_to_top(); + m_stack_state.set_to_top(); + m_extra_constraints.set_to_top(); +} + +void offset_domain_t::set_to_bottom() { + m_is_bottom = true; +} + +bool offset_domain_t::is_bottom() const { + return m_is_bottom; +} + +bool offset_domain_t::is_top() const { + if (m_is_bottom) return false; + return (m_reg_state.is_top() && m_stack_state.is_top() && m_extra_constraints.is_top()); +} + +// inclusion +bool offset_domain_t::operator<=(const offset_domain_t& other) const { return true; } + +// join +void offset_domain_t::operator|=(const offset_domain_t& abs) { + offset_domain_t tmp{abs}; + operator|=(std::move(tmp)); +} + +void offset_domain_t::operator|=(offset_domain_t&& abs) { + if (is_bottom()) { + *this = abs; + return; + } + *this = *this | std::move(abs); +} + +offset_domain_t offset_domain_t::operator|(const offset_domain_t& other) const { + if (is_bottom() || other.is_top()) { + return other; + } + else if (other.is_bottom() || is_top()) { + return *this; + } + return offset_domain_t(m_reg_state | other.m_reg_state, m_stack_state | other.m_stack_state, m_extra_constraints | other.m_extra_constraints, m_ctx_dists, std::max(m_slack, other.m_slack)); +} + +offset_domain_t offset_domain_t::operator|(offset_domain_t&& other) const { + if (is_bottom() || other.is_top()) { + return std::move(other); + } + else if (other.is_bottom() || is_top()) { + return *this; + } + return offset_domain_t(m_reg_state | std::move(other.m_reg_state), + m_stack_state | std::move(other.m_stack_state), + m_extra_constraints | std::move(other.m_extra_constraints), + m_ctx_dists, std::max(m_slack, other.m_slack)); +} + +// meet +offset_domain_t offset_domain_t::operator&(const offset_domain_t& other) const { + /* WARNING: The operation is not implemented yet.*/ + return other; +} + +// widening +offset_domain_t offset_domain_t::widen(const offset_domain_t& other) const { + /* WARNING: The operation is not implemented yet.*/ + return other; +} + +// narrowing +offset_domain_t offset_domain_t::narrow(const offset_domain_t& other) const { + /* WARNING: The operation is not implemented yet.*/ + return other; +} + +//forget +void offset_domain_t::operator-=(variable_t var) {} + +void offset_domain_t::write(std::ostream& os) const {} + +std::string offset_domain_t::domain_name() const { + return "offset_domain"; +} + +int offset_domain_t::get_instruction_count_upper_bound() { + /* WARNING: The operation is not implemented yet.*/ + return 0; +} + +string_invariant offset_domain_t::to_set() { return string_invariant{}; } + +void offset_domain_t::operator()(const LoadMapFd &u, location_t loc, int print) { + m_reg_state -= u.dst.v; +} + +void offset_domain_t::operator()(const Packet &u, location_t loc, int print) { + register_t r0_reg{R0_RETURN_VALUE}; + m_reg_state -= r0_reg; +} + +void offset_domain_t::operator()(const Call &u, location_t loc, int print) { + register_t r0_reg{R0_RETURN_VALUE}; + m_reg_state -= r0_reg; +} + +void offset_domain_t::operator()(const Assume &b, location_t loc, int print) { + Condition cond = b.cond; + if (cond.op == Condition::Op::LE) { + if (std::holds_alternative(cond.right)) { + auto right_reg = std::get(cond.right).v; + auto dist_left = m_reg_state.find(cond.left.v); + auto dist_right = m_reg_state.find(right_reg); + if (!dist_left || !dist_right) { + // this should not happen, comparison between a packet pointer and either + // other region's pointers or numbers; possibly raise type error + //exit(1); + std::cout << "type_error: one of the pointers being compared isn't packet pointer\n"; + return; + } + dist_t left_reg_dist = dist_left.value(); + dist_t right_reg_dist = dist_right.value(); + slack_var_t s = m_slack++; + dist_t f = dist_t(left_reg_dist.m_dist, s); + dist_t b = dist_t(right_reg_dist.m_dist); + auto eq = equality_t(f, b); + auto ineq = inequality_t(s, rop_t::R_GE, weight_t(number_t(0))); + if (f.is_meta_pointer() && b.is_forward_pointer()) { + m_extra_constraints.add_meta_and_begin_constraint(std::move(eq), std::move(ineq)); + } + else if (f.is_forward_pointer() && b.is_backward_pointer()) { + m_extra_constraints.add_begin_and_end_constraint(std::move(eq), std::move(ineq)); + } + } + } + else {} //we do not need to deal with other cases +} + +bool is_packet_pointer(std::optional& type) { + if (!type) { // not a pointer + return false; + } + auto ptr_or_mapfd_type = type.value(); + return (std::holds_alternative(ptr_or_mapfd_type) + && std::get(ptr_or_mapfd_type).get_region() == crab::region_t::T_PACKET); +} + +bool is_stack_pointer(std::optional& type) { + if (!type) { // not a pointer + return false; + } + auto ptr_or_mapfd_type = type.value(); + return (std::holds_alternative(ptr_or_mapfd_type) + && std::get(ptr_or_mapfd_type).get_region() == crab::region_t::T_STACK); +} + +void offset_domain_t::update_offset_info(const dist_t&& dist, const interval_t&& change, + const reg_with_loc_t& reg_with_loc, uint8_t reg, Bin::Op op) { + auto offset = dist.m_dist; + if (op == Bin::Op::ADD) { + if (dist.is_forward_pointer()) offset += change; + else if (dist.is_backward_pointer()) offset -= change; + else offset -= change; + } + else if (op == Bin::Op::SUB) { + // TODO: needs precise handling of subtraction + offset = interval_t::top(); + } + m_reg_state.insert(reg, reg_with_loc, dist_t(offset)); +} + +interval_t offset_domain_t::do_bin(const Bin &bin, + const std::optional& src_interval_opt, + const std::optional& dst_interval_opt, + std::optional& src_ptr_or_mapfd_opt, + std::optional& dst_ptr_or_mapfd_opt, location_t loc) { + using Op = Bin::Op; + // if both src and dst are numbers, nothing to do in offset domain + // if we are doing a move, where src is a number and dst is not set, nothing to do + if ((dst_interval_opt && src_interval_opt) + || (src_interval_opt && !dst_ptr_or_mapfd_opt && bin.op == Op::MOV)) + return interval_t::bottom(); + // offset domain only handles packet pointers + if (!is_packet_pointer(src_ptr_or_mapfd_opt) && !is_packet_pointer(dst_ptr_or_mapfd_opt)) + return interval_t::bottom(); + + interval_t src_interval, dst_interval; + if (src_interval_opt) src_interval = std::move(src_interval_opt.value()); + if (dst_interval_opt) dst_interval = std::move(dst_interval_opt.value()); + + Reg src; + if (std::holds_alternative(bin.v)) src = std::get(bin.v); + + auto reg_with_loc = reg_with_loc_t(bin.dst.v, loc); + switch (bin.op) + { + // ra = rb; + case Op::MOV: { + if (!is_packet_pointer(src_ptr_or_mapfd_opt)) { + m_reg_state -= bin.dst.v; + return interval_t::bottom(); + } + auto src_offset_opt = m_reg_state.find(src.v); + if (!src_offset_opt) { + std::cout << "type_error: src is a packet_pointer and no offset info found\n"; + return interval_t::bottom(); + } + m_reg_state.insert(bin.dst.v, reg_with_loc, src_offset_opt.value()); + break; + } + // ra += rb + case Op::ADD: { + dist_t dist_to_update; + interval_t interval_to_add; + if (is_packet_pointer(dst_ptr_or_mapfd_opt) + && is_packet_pointer(src_ptr_or_mapfd_opt)) { + m_reg_state -= bin.dst.v; + return interval_t::bottom(); + } + else if (is_packet_pointer(dst_ptr_or_mapfd_opt) && src_interval_opt) { + auto dst_offset_opt = m_reg_state.find(bin.dst.v); + if (!dst_offset_opt) { + std::cout << "type_error: dst is a packet_pointer and no offset info found\n"; + m_reg_state -= bin.dst.v; + return interval_t::bottom(); + } + dist_to_update = std::move(dst_offset_opt.value()); + interval_to_add = std::move(src_interval_opt.value()); + } + else { + auto src_offset_opt = m_reg_state.find(src.v); + if (!src_offset_opt) { + std::cout << "type_error: src is a packet_pointer and no offset info found\n"; + m_reg_state -= bin.dst.v; + return interval_t::bottom(); + } + dist_to_update = std::move(src_offset_opt.value()); + interval_to_add = std::move(dst_interval_opt.value()); + } + update_offset_info(std::move(dist_to_update), std::move(interval_to_add), + reg_with_loc, bin.dst.v, bin.op); + break; + } + // ra -= rb + case Op::SUB: { + dist_t dist_to_update; + interval_t interval_to_sub; + if (is_packet_pointer(dst_ptr_or_mapfd_opt) + && is_packet_pointer(src_ptr_or_mapfd_opt)) { + m_reg_state -= bin.dst.v; + return interval_t::top(); + } + else if (is_packet_pointer(dst_ptr_or_mapfd_opt) && src_interval_opt) { + auto dst_offset_opt = m_reg_state.find(bin.dst.v); + if (!dst_offset_opt) { + std::cout << "type_error: dst is a packet_pointer and no offset info found\n"; + m_reg_state -= bin.dst.v; + return interval_t::bottom(); + } + dist_to_update = std::move(dst_offset_opt.value()); + interval_to_sub = std::move(src_interval_opt.value()); + } + else { + auto src_offset_opt = m_reg_state.find(src.v); + if (!src_offset_opt) { + std::cout << "type_error: src is a packet_pointer and no offset info found\n"; + m_reg_state -= bin.dst.v; + return interval_t::bottom(); + } + dist_to_update = std::move(src_offset_opt.value()); + interval_to_sub = std::move(dst_interval_opt.value()); + } + update_offset_info(std::move(dist_to_update), std::move(interval_to_sub), + reg_with_loc, bin.dst.v, bin.op); + break; + } + default: { + m_reg_state -= bin.dst.v; + break; + } + } + return interval_t::bottom(); +} + +bool offset_domain_t::lower_bound_satisfied(const dist_t& dist, int offset) const { + auto meta_limit = m_extra_constraints.get_meta_limit(); + auto end_limit = m_extra_constraints.get_end_limit(); + + dist_t dist1 = dist; + if (dist.is_meta_pointer()) { + dist1 = dist_t(dist.offset_from_reference() + + (meta_limit ? weight_t(meta_limit.value()-PACKET_META) : weight_t(bound_t(0)))); + } + if (dist.is_backward_pointer()) { + dist1 = dist_t(dist.offset_from_reference() + + (end_limit ? weight_t(end_limit.value()) : weight_t(bound_t(0)))); + } + + bound_t lb = meta_limit ? meta_limit.value()-PACKET_META : bound_t(0); + return (dist1.m_dist.lb()+offset >= lb); +} + +bool offset_domain_t::upper_bound_satisfied(const dist_t& dist, int offset, int width, + bool is_comparison_check) const { + auto meta_limit = m_extra_constraints.get_meta_limit(); + auto end_limit = m_extra_constraints.get_end_limit(); + + dist_t dist1 = dist; + if (dist.is_meta_pointer()) { + dist1 = dist_t(dist.offset_from_reference() + (meta_limit ? + weight_t(meta_limit.value()-PACKET_META) : weight_t(bound_t((0))))); + } + if (dist.is_backward_pointer()) { + dist1 = dist_t(dist.offset_from_reference() + + (end_limit ? weight_t(end_limit.value()) : + weight_t(bound_t(is_comparison_check ? MAX_PACKET_SIZE : 0)))); + } + + bound_t ub = is_comparison_check ? bound_t(MAX_PACKET_SIZE) + : (end_limit ? end_limit.value() : bound_t(0)); + return (dist1.m_dist.ub()+offset+width <= ub); +} + +bool offset_domain_t::check_packet_access(const Reg& r, int width, int offset, + bool is_comparison_check) const { + auto it = m_reg_state.find(r.v); + if (!it) return false; + dist_t dist = it.value(); + + return (lower_bound_satisfied(dist, offset) + && upper_bound_satisfied(dist, offset, width, is_comparison_check)); +} + +void offset_domain_t::check_valid_access(const ValidAccess& s, + std::optional& reg_type, std::optional& interval_type, + std::optional& width_interval) const { + + bool is_comparison_check = s.width == (Value)Imm{0}; + number_t width_from_interval; + if (width_interval) { + auto& val = width_interval.value(); + std::optional valid_num = val.ub().number(); + if (!valid_num) { + return; + } + width_from_interval = valid_num.value(); + } + else if (std::holds_alternative(s.width)) { + return; + } + int width = std::holds_alternative(s.width) ? std::get(s.width).v + : int(width_from_interval); + + if (reg_type) { + auto reg_ptr_or_mapfd_type = reg_type.value(); + if (std::holds_alternative(reg_ptr_or_mapfd_type)) { + auto reg_with_off_ptr_type = std::get(reg_ptr_or_mapfd_type); + auto offset = reg_with_off_ptr_type.get_offset(); + auto offset_to_check = offset+interval_t(number_t(s.offset)); + auto offset_lb = offset_to_check.lb(); + auto offset_plus_width_ub = offset_to_check.ub()+bound_t(width); + if (reg_with_off_ptr_type.get_region() == crab::region_t::T_STACK) { + if (bound_t(STACK_BEGIN) <= offset_lb + && offset_plus_width_ub <= bound_t(EBPF_STACK_SIZE)) + return; + } + else if (reg_with_off_ptr_type.get_region() == crab::region_t::T_CTX) { + if (bound_t(CTX_BEGIN) <= offset_lb + && offset_plus_width_ub <= bound_t(m_ctx_dists->get_size())) + return; + } + else { // shared + if (bound_t(SHARED_BEGIN) <= offset_lb && + offset_plus_width_ub <= reg_with_off_ptr_type.get_region_size().lb()) return; + // TODO: check null access + //return; + } + } + else if (std::holds_alternative(reg_ptr_or_mapfd_type)) { + auto reg_no_off_ptr_type = std::get(reg_ptr_or_mapfd_type); + if (reg_no_off_ptr_type.get_region() == crab::region_t::T_PACKET) { + if (check_packet_access(s.reg, width, s.offset, is_comparison_check)) return; + } + } + else { + if (is_comparison_check) return; + std::cout << "FDs cannot be dereferenced directly\n"; + // mapfd + } + } + if (interval_type) { + auto &interval = interval_type.value(); + if (is_comparison_check) return; + auto singleton = interval.singleton(); + if (s.or_null) { + if (singleton && singleton.value() == number_t(0)) return; + std::cout << "type error: non-null number\n"; + } + else std::cout << "type error: only pointers can be dereferenced\n"; + } + std::cout << "valid access assert fail\n"; + //exit(1); +} + +void offset_domain_t::do_mem_store(const Mem& b, const Reg& target_reg, + std::optional& basereg_type, + std::optional& targetreg_type) { + int offset = b.access.offset; + + if (is_stack_pointer(basereg_type)) { + auto basereg_with_off = std::get(basereg_type.value()); + auto offset_singleton = basereg_with_off.get_offset().singleton(); + if (!offset_singleton) { + std::cout << "doing a stack store at an unknown offset\n"; + m_reg_state -= target_reg.v; + return; + } + auto ptr_offset = offset_singleton.value(); + auto store_at = (uint64_t)(ptr_offset + offset); + if (is_packet_pointer(targetreg_type)) { + auto it = m_reg_state.find(target_reg.v); + if (!it) { + std::cout << "type_error: register is a packet_pointer and no offset info found\n"; + return; + } + m_stack_state.store(store_at, it.value()); + } + else { + m_stack_state -= store_at; + } + } + else {} // in the rest cases, we do not store +} + +void offset_domain_t::do_load(const Mem& b, const Reg& target_reg, + std::optional& basereg_type, location_t loc) { + if (!basereg_type) { + m_reg_state -= target_reg.v; + return; + } + auto basereg_ptr_type = basereg_type.value(); + int offset = b.access.offset; + + if (std::holds_alternative(basereg_ptr_type)) { + auto p_with_off = std::get(basereg_ptr_type); + auto p_offset = p_with_off.get_offset(); + auto offset_singleton = p_offset.singleton(); + + if (p_with_off.get_region() == crab::region_t::T_CTX) { + if (!offset_singleton) { + m_reg_state -= target_reg.v; + return; + } + auto load_at = (uint64_t)offset_singleton.value() + (uint64_t)offset; + auto it = m_ctx_dists->find(load_at); + if (!it) { + m_reg_state -= target_reg.v; + return; + } + dist_t d = it.value(); + auto reg = reg_with_loc_t(target_reg.v, loc); + m_reg_state.insert(target_reg.v, reg, dist_t(d)); + } + else if (p_with_off.get_region() == crab::region_t::T_STACK) { + if (!offset_singleton) { + m_reg_state -= target_reg.v; + return; + } + auto ptr_offset = offset_singleton.value(); + auto load_at = (uint64_t)(ptr_offset + offset); + auto it = m_stack_state.find(load_at); + + if (!it) { + m_reg_state -= target_reg.v; + return; + } + dist_t d = it.value(); + auto reg = reg_with_loc_t(target_reg.v, loc); + m_reg_state.insert(target_reg.v, reg, dist_t(d)); + } + else { // shared + m_reg_state -= target_reg.v; + } + } + else { // we are loading from packet, or we have mapfd + m_reg_state -= target_reg.v; + } +} + +std::optional offset_domain_t::find_offset_at_loc(const reg_with_loc_t reg) const { + return m_reg_state.find(reg); +} + +std::optional offset_domain_t::find_in_ctx(int key) const { + return m_ctx_dists->find(key); +} + +std::optional offset_domain_t::find_in_stack(int key) const { + return m_stack_state.find(key); +} + +std::optional offset_domain_t::find_offset_info(register_t reg) const { + return m_reg_state.find(reg); +} + +void offset_domain_t::adjust_bb_for_types(location_t loc) { + m_reg_state.adjust_bb_for_registers(loc); +} + +void offset_domain_t::print_all_register_types() const { + m_reg_state.print_all_register_types(); +} diff --git a/src/crab/offset_domain.hpp b/src/crab/offset_domain.hpp new file mode 100644 index 000000000..e228c12fe --- /dev/null +++ b/src/crab/offset_domain.hpp @@ -0,0 +1,300 @@ +// Copyright (c) Prevail Verifier contributors. +// SPDX-License-Identifier: MIT + +#pragma once + +#include + +#include +#include "crab/abstract_domain.hpp" +#include "crab/region_domain.hpp" +#include "crab/cfg.hpp" +#include "linear_constraint.hpp" +#include "string_constraints.hpp" + +constexpr int STACK_BEGIN = 0; +constexpr int CTX_BEGIN = 0; +constexpr int PACKET_BEGIN = 0; +constexpr int SHARED_BEGIN = 0; +constexpr int PACKET_END = -4100; +constexpr int PACKET_META = -1; +constexpr int MAX_PACKET_SIZE = 0xffff; + +using crab::ptr_or_mapfd_t; +using crab::ptr_t; +using crab::mapfd_t; +using crab::ptr_with_off_t; +using crab::ptr_no_off_t; +using crab::reg_with_loc_t; +using crab::interval_t; +using crab::bound_t; + +using weight_t = interval_t; +using slack_var_t = int; + +enum class rop_t { + R_GT, + R_GE, + R_LT, + R_LE +}; + +struct dist_t { + slack_var_t m_slack; + weight_t m_dist; + bool m_is_bottom = false; + + dist_t(weight_t d, slack_var_t s = -1, bool bottom = false) + : m_slack(s), m_dist(d), m_is_bottom(bottom) {} + dist_t() : m_slack(-1), m_dist(weight_t::top()), m_is_bottom(false) {} + bool operator==(const dist_t& d) const; + void write(std::ostream&) const; + bool is_top() const; + bool is_bottom() const; + void set_to_top(); + void set_to_bottom(); + friend std::ostream& operator<<(std::ostream& o, const dist_t& d); + bool is_meta_pointer() const; + bool is_forward_pointer() const; + bool is_backward_pointer() const; + weight_t offset_from_reference() const; +}; + +struct inequality_t { + slack_var_t m_slack; + rop_t m_rel; + weight_t m_value; + bool m_is_bottom = false; + + inequality_t(slack_var_t slack, rop_t rel, weight_t val) : m_slack(slack), m_rel(rel) + , m_value(val) {} + inequality_t() : m_slack(-1), m_value(weight_t::top()) {} + bool is_top() const; + bool is_bottom() const; + void set_to_top(); + void set_to_bottom(); + void write(std::ostream&) const; + friend std::ostream& operator<<(std::ostream&, const inequality_t&); +}; // represents `slack rel value;`, e.g., `s >= 0` + +struct equality_t { + dist_t m_lhs; + dist_t m_rhs; + bool m_is_bottom = false; + + equality_t(dist_t lhs, dist_t rhs) : m_lhs(lhs), m_rhs(rhs) {} + equality_t() = default; + bool is_top() const; + bool is_bottom() const; + void set_to_top(); + void set_to_bottom(); + void write(std::ostream&) const; + friend std::ostream& operator<<(std::ostream&, const equality_t&); +}; // represents constraint `p[0] = p[1];`, e.g., `begin+8+s = end` + +struct packet_constraint_t { + equality_t m_eq; + inequality_t m_ineq; + bool m_is_meta_constraint; + bool m_is_bottom = false; + + bool is_bottom() const; + bool is_top() const; + void set_to_bottom(); + void set_to_top(); + std::optional get_limit() const; + packet_constraint_t() = default; + packet_constraint_t(equality_t&& eq, inequality_t&& ineq, bool is_meta_constraint, + bool is_bottom = false) : m_eq(eq), m_ineq(ineq), + m_is_meta_constraint(is_meta_constraint), m_is_bottom(is_bottom) {} + packet_constraint_t operator|(const packet_constraint_t&) const; + void write(std::ostream&) const; + friend std::ostream& operator<<(std::ostream&, const packet_constraint_t&); +}; + +using live_registers_t = std::array, 11>; +using global_offset_env_t = std::unordered_map; + +class registers_state_t { + + live_registers_t m_cur_def; + std::shared_ptr m_offset_env; + bool m_is_bottom = false; + + public: + registers_state_t(bool is_bottom = false) : m_offset_env(nullptr), m_is_bottom(is_bottom) {} + registers_state_t(std::shared_ptr offset_env, bool is_bottom = false) : m_offset_env(offset_env), m_is_bottom(is_bottom) {} + explicit registers_state_t(live_registers_t&& vars, std::shared_ptr + offset_env, bool is_bottom = false) + : m_cur_def(std::move(vars)), m_offset_env(std::move(offset_env)), m_is_bottom(is_bottom) {} + + registers_state_t operator|(const registers_state_t&) const; + void operator-=(register_t); + void set_to_top(); + void set_to_bottom(); + bool is_bottom() const; + bool is_top() const; + void insert(register_t, const reg_with_loc_t&, const dist_t&); + std::optional find(reg_with_loc_t reg) const; + std::optional find(register_t key) const; + friend std::ostream& operator<<(std::ostream& o, const registers_state_t& p); + void adjust_bb_for_registers(location_t); + void print_all_register_types() const; +}; + +class stack_state_t { + using stack_slot_dists_t = std::unordered_map; // represents `sp[n] = dist;`, where n \belongs [0,511], e.g., `sp[508] = begin+16` + + stack_slot_dists_t m_slot_dists; + bool m_is_bottom = false; + + public: + stack_state_t(bool is_bottom = false) : m_is_bottom(is_bottom) {} + std::optional find(int) const; + void store(int, dist_t); + void operator-=(int); + void set_to_top(); + void set_to_bottom(); + bool is_bottom() const; + bool is_top() const; + static stack_state_t top(); + stack_state_t operator|(const stack_state_t&) const; + explicit stack_state_t(stack_slot_dists_t&& stack_dists, bool is_bottom = false) + : m_slot_dists(std::move(stack_dists)), m_is_bottom(is_bottom) {} +}; + +class extra_constraints_t { + + packet_constraint_t m_meta_and_begin; + packet_constraint_t m_begin_and_end; + bool m_is_bottom = false; + + public: + extra_constraints_t(bool is_bottom = false) : m_is_bottom(is_bottom) {} + bool is_bottom() const; + bool is_top() const; + void set_to_top(); + void set_to_bottom(); + void normalize(); + std::optional get_end_limit() const; + std::optional get_meta_limit() const; + void add_meta_and_begin_constraint(equality_t&&, inequality_t&&); + void add_begin_and_end_constraint(equality_t&&, inequality_t&&); + extra_constraints_t operator|(const extra_constraints_t&) const; + explicit extra_constraints_t(packet_constraint_t&& meta_and_begin, + packet_constraint_t&& begin_and_end, bool is_bottom = false) + : m_meta_and_begin(meta_and_begin), m_begin_and_end(begin_and_end), + m_is_bottom(is_bottom) {} +}; + +class ctx_t { + using ctx_dists_t = std::unordered_map; // represents `cp[n] = dist;` + ctx_dists_t m_dists; + int m_size; + + public: + ctx_t(const ebpf_context_descriptor_t* desc); + std::optional find(uint64_t) const; + int get_size() const; +}; + + +class offset_domain_t final { + + bool m_is_bottom = false; + registers_state_t m_reg_state; + stack_state_t m_stack_state; + extra_constraints_t m_extra_constraints; + std::shared_ptr m_ctx_dists; + slack_var_t m_slack = 0; + + public: + offset_domain_t() = default; + offset_domain_t(offset_domain_t&& o) = default; + offset_domain_t(const offset_domain_t& o) = default; + offset_domain_t& operator=(offset_domain_t&& o) = default; + offset_domain_t& operator=(const offset_domain_t& o) = default; + explicit offset_domain_t(registers_state_t&& reg, stack_state_t&& stack, + extra_constraints_t extra, std::shared_ptr ctx, slack_var_t s = 0) + : m_reg_state(std::move(reg)), m_stack_state(std::move(stack)), + m_extra_constraints(std::move(extra)), m_ctx_dists(ctx), m_slack(s) {} + + explicit offset_domain_t(registers_state_t&& reg, stack_state_t&& stack, + std::shared_ptr ctx, slack_var_t s = 0) : m_reg_state(std::move(reg)), + m_stack_state(std::move(stack)), m_ctx_dists(ctx), m_slack(s) {} + + static offset_domain_t setup_entry(); + // bottom/top + static offset_domain_t bottom(); + void set_to_top(); + void set_to_bottom(); + bool is_bottom() const; + bool is_top() const; + // inclusion + bool operator<=(const offset_domain_t& other) const; + // join + void operator|=(const offset_domain_t& abs); + void operator|=(offset_domain_t&& abs); + offset_domain_t operator|(const offset_domain_t& other) const; + offset_domain_t operator|(offset_domain_t&& abs) const; + // meet + offset_domain_t operator&(const offset_domain_t& other) const; + // widening + offset_domain_t widen(const offset_domain_t& other) const; + // narrowing + offset_domain_t narrow(const offset_domain_t& other) const; + //forget + void operator-=(variable_t var); + void operator-=(register_t reg) { m_reg_state -= reg; } + + //// abstract transformers + void operator()(const Undefined &, location_t loc = boost::none, int print = 0) {} + void operator()(const Bin &, location_t loc = boost::none, int print = 0) {} + void operator()(const Un &, location_t loc = boost::none, int print = 0) {} + void operator()(const LoadMapFd &, location_t loc = boost::none, int print = 0); + void operator()(const Call &, location_t loc = boost::none, int print = 0); + void operator()(const Exit &, location_t loc = boost::none, int print = 0) {} + void operator()(const Jmp &, location_t loc = boost::none, int print = 0) {} + void operator()(const Mem &, location_t loc = boost::none, int print = 0) {} + void operator()(const Packet &, location_t loc = boost::none, int print = 0); + void operator()(const LockAdd &, location_t loc = boost::none, int print = 0) {} + void operator()(const Assume &, location_t loc = boost::none, int print = 0); + void operator()(const Assert &, location_t loc = boost::none, int print = 0) {} + void operator()(const ValidAccess&, location_t loc = boost::none, int print = 0) {} + void operator()(const Comparable& s, location_t loc = boost::none, int print = 0) {} + void operator()(const Addable& s, location_t loc = boost::none, int print = 0) {} + void operator()(const ValidStore& s, location_t loc = boost::none, int print = 0) {} + void operator()(const TypeConstraint& s, location_t loc = boost::none, int print = 0) {} + void operator()(const ValidSize& s, location_t loc = boost::none, int print = 0) {} + void operator()(const ValidMapKeyValue& s, location_t loc = boost::none, int print = 0) {} + void operator()(const ZeroOffset& s, location_t loc = boost::none, int print = 0) {} + void operator()(const basic_block_t& bb, bool check_termination, int print = 0) {} + void write(std::ostream& os) const; + std::string domain_name() const; + int get_instruction_count_upper_bound(); + string_invariant to_set(); + void set_require_check(check_require_func_t f) {} + + void do_load(const Mem&, const Reg&, std::optional&, location_t loc); + void do_mem_store(const Mem&, const Reg&, std::optional&, + std::optional&); + interval_t do_bin(const Bin&, const std::optional&, + const std::optional&, + std::optional&, + std::optional&, location_t); + bool upper_bound_satisfied(const dist_t&, int, int, bool) const; + bool lower_bound_satisfied(const dist_t&, int) const; + bool check_packet_access(const Reg&, int, int, bool) const; + void check_valid_access(const ValidAccess&, std::optional&, + std::optional&, std::optional&) const; + + std::optional find_in_ctx(int) const; + std::optional find_in_stack(int) const; + std::optional find_offset_at_loc(const reg_with_loc_t) const; + std::optional find_offset_info(register_t reg) const; + void update_offset_info(const dist_t&&, const interval_t&&, + const reg_with_loc_t&, uint8_t, Bin::Op); + dist_t update_offset(const dist_t&, const weight_t&, const interval_t&, Bin::Op); + void adjust_bb_for_types(location_t); + void print_all_register_types() const; +}; // end offset_domain_t diff --git a/src/crab/region_domain.cpp b/src/crab/region_domain.cpp new file mode 100644 index 000000000..6ded73c4e --- /dev/null +++ b/src/crab/region_domain.cpp @@ -0,0 +1,1054 @@ +// Copyright (c) Prevail Verifier contributors. +// SPDX-License-Identifier: MIT + +#include "crab/region_domain.hpp" + +using crab::___print___; +using crab::ptr_t; +using crab::mapfd_t; +using crab::ptr_or_mapfd_t; +using crab::ptr_with_off_t; +using crab::ptr_no_off_t; +using crab::ctx_t; +using crab::global_region_env_t; +using crab::reg_with_loc_t; +using crab::live_registers_t; +using crab::register_types_t; +using crab::map_key_size_t; +using crab::map_value_size_t; +using crab::ptr_or_mapfd_cells_t; + +namespace std { + template <> + struct hash { + size_t operator()(const crab::reg_with_loc_t& reg) const { return reg.hash(); } + }; + + // does not seem to work for me + /* + template <> + struct equal_to { + constexpr bool operator()(const crab::ptr_t& p1, const crab::ptr_t& p2) const { + if (p1.index() != p2.index()) return false; + if (std::holds_alternative(p1)) { + auto ptr_no_off1 = std::get(p1); + auto ptr_no_off2 = std::get(p2); + return (ptr_no_off1.get_region() == ptr_no_off2.get_region()); + } + else { + auto ptr_with_off1 = std::get(p1); + auto ptr_with_off2 = std::get(p2); + return (ptr_with_off1.get_region() == ptr_with_off2.get_region() && ptr_with_off1.get_offset() == ptr_with_off2.get_offset()); + } + } + }; + */ + + static ptr_t get_ptr(const ptr_or_mapfd_t& t) { + return std::visit( overloaded + { + []( const ptr_with_off_t& x ){ return ptr_t{x};}, + []( const ptr_no_off_t& x ){ return ptr_t{x};}, + []( auto& ) { return ptr_t{};} + }, t + ); + } +} + + +namespace crab { + +inline std::string get_reg_ptr(const region_t& r) { + switch (r) { + case region_t::T_CTX: + return "ctx_p"; + case region_t::T_STACK: + return "stack_p"; + case region_t::T_PACKET: + return "packet_p"; + default: + return "shared_p"; + } +} + +static bool same_region(const ptr_t& ptr1, const ptr_t& ptr2) { + return ((std::holds_alternative(ptr1) + && std::holds_alternative(ptr2)) + || (std::holds_alternative(ptr1) + && std::holds_alternative(ptr2))); +} + +static void print_ptr_type(const ptr_t& ptr) { + if (std::holds_alternative(ptr)) { + ptr_with_off_t ptr_with_off = std::get(ptr); + std::cout << ptr_with_off; + } + else { + ptr_no_off_t ptr_no_off = std::get(ptr); + std::cout << ptr_no_off; + } +} + +static void print_ptr_or_mapfd_type(const ptr_or_mapfd_t& ptr_or_mapfd) { + if (std::holds_alternative(ptr_or_mapfd)) { + std::cout << std::get(ptr_or_mapfd); + } + else { + auto ptr = get_ptr(ptr_or_mapfd); + print_ptr_type(ptr); + } +} + +inline std::ostream& operator<<(std::ostream& o, const region_t& t) { + o << static_cast::type>(t); + return o; +} + +bool operator==(const ptr_with_off_t& p1, const ptr_with_off_t& p2) { + return (p1.get_region() == p2.get_region() && p1.get_offset() == p2.get_offset() + && p1.get_region_size() == p2.get_region_size()); +} + +bool operator!=(const ptr_with_off_t& p1, const ptr_with_off_t& p2) { + return !(p1 == p2); +} + +void ptr_with_off_t::write(std::ostream& o) const { + o << get_reg_ptr(m_r) << "<" << m_offset; + if (m_region_size.lb() >= bound_t(0)) o << "," << m_region_size; + o << ">"; +} + +std::ostream& operator<<(std::ostream& o, const ptr_with_off_t& p) { + p.write(o); + return o; +} + +interval_t ptr_with_off_t::get_region_size() const { return m_region_size; } + +void ptr_with_off_t::set_offset(interval_t off) { m_offset = off; } + +void ptr_with_off_t::set_region_size(interval_t region_sz) { m_region_size = region_sz; } + +void ptr_with_off_t::set_region(region_t r) { m_r = r; } + +ptr_with_off_t ptr_with_off_t::operator|(const ptr_with_off_t& other) const { + return ptr_with_off_t(m_r, m_offset | other.m_offset, m_region_size | other.m_region_size); +} + +bool operator==(const ptr_no_off_t& p1, const ptr_no_off_t& p2) { + return (p1.get_region() == p2.get_region()); +} + +bool operator!=(const ptr_no_off_t& p1, const ptr_no_off_t& p2) { + return !(p1 == p2); +} + +void ptr_no_off_t::write(std::ostream& o) const { + o << get_reg_ptr(get_region()); +} + +std::ostream& operator<<(std::ostream& o, const ptr_no_off_t& p) { + p.write(o); + return o; +} + +void ptr_no_off_t::set_region(region_t r) { m_r = r; } + +bool operator==(const mapfd_t& m1, const mapfd_t& m2) { + return (m1.get_value_type() == m2.get_value_type()); +} + +std::ostream& operator<<(std::ostream& o, const mapfd_t& m) { + m.write(o); + return o; +} + +bool mapfd_t::has_type_map_programs() const { + return (m_value_type == EbpfMapValueType::PROGRAM); +} + +void mapfd_t::write(std::ostream& o) const { + if (has_type_map_programs()) { + o << "map_fd_programs"; + } + else { + o << "map_fd"; + } +} + +void reg_with_loc_t::write(std::ostream& o) const { + o << "r" << static_cast(m_reg) << "@" << m_loc->second << " in " << m_loc->first << " "; +} + +std::ostream& operator<<(std::ostream& o, const reg_with_loc_t& reg) { + reg.write(o); + return o; +} + +bool reg_with_loc_t::operator==(const reg_with_loc_t& other) const { + return (m_reg == other.m_reg && m_loc == other.m_loc); +} + +std::size_t reg_with_loc_t::hash() const { + // Similar to boost::hash_combine + using std::hash; + + std::size_t seed = hash()(m_reg); + seed ^= hash()(m_loc->first.from) + 0x9e3779b9 + (seed << 6) + (seed >> 2); + seed ^= hash()(m_loc->first.to) + 0x9e3779b9 + (seed << 6) + (seed >> 2); + seed ^= hash()(m_loc->second) + 0x9e3779b9 + (seed << 6) + (seed >> 2); + + return seed; +} + +ctx_t::ctx_t(const ebpf_context_descriptor_t* desc) +{ + if (desc->data >= 0) { + m_packet_ptrs[desc->data] = crab::ptr_no_off_t(crab::region_t::T_PACKET); + } + if (desc->end >= 0) { + m_packet_ptrs[desc->end] = crab::ptr_no_off_t(crab::region_t::T_PACKET); + } + if (desc->meta >= 0) { + m_packet_ptrs[desc->meta] = crab::ptr_no_off_t(crab::region_t::T_PACKET); + } +} + +size_t ctx_t::size() const { + return m_packet_ptrs.size(); +} + +std::vector ctx_t::get_keys() const { + std::vector keys; + keys.reserve(size()); + + for (auto const&kv : m_packet_ptrs) { + keys.push_back(kv.first); + } + return keys; +} + +std::optional ctx_t::find(uint64_t key) const { + auto it = m_packet_ptrs.find(key); + if (it == m_packet_ptrs.end()) return {}; + return it->second; +} + +register_types_t register_types_t::operator|(const register_types_t& other) const { + if (is_bottom() || other.is_top()) { + return other; + } else if (other.is_bottom() || is_top()) { + return *this; + } + live_registers_t out_vars; + + // a hack to store region information at the start of a joined basic block + // in join, we do not know the label of the bb, hence we store the information + // at a bb that is not used anywhere else in the program, and later when we know + // the bb label, we can fix + location_t loc = location_t(std::make_pair(label_t(-2, -2), 0)); + + for (size_t i = 0; i < m_cur_def.size(); i++) { + if (m_cur_def[i] == nullptr || other.m_cur_def[i] == nullptr) continue; + auto it1 = find(*(m_cur_def[i])); + auto it2 = other.find(*(other.m_cur_def[i])); + if (it1 && it2) { + ptr_or_mapfd_t ptr_or_mapfd1 = it1.value(), ptr_or_mapfd2 = it2.value(); + auto reg = reg_with_loc_t((register_t)i, loc); + if (ptr_or_mapfd1 == ptr_or_mapfd2) { + out_vars[i] = m_cur_def[i]; + } + else if (!std::holds_alternative(ptr_or_mapfd1) + && !std::holds_alternative(ptr_or_mapfd2)) { + auto ptr1 = get_ptr(ptr_or_mapfd1); + auto ptr2 = get_ptr(ptr_or_mapfd2); + if (std::holds_alternative(ptr1) + && std::holds_alternative(ptr2)) { + ptr_with_off_t ptr_with_off1 = std::get(ptr1); + ptr_with_off_t ptr_with_off2 = std::get(ptr2); + if (ptr_with_off1.get_region() == ptr_with_off2.get_region()) { + out_vars[i] = std::make_shared(reg); + (*m_region_env)[reg] = std::move(ptr_with_off1 | ptr_with_off2); + } + } + } + } + } + return register_types_t(std::move(out_vars), m_region_env, false); +} + +void register_types_t::operator-=(register_t var) { + if (is_bottom()) { + return; + } + m_cur_def[var] = nullptr; +} + +void register_types_t::set_to_bottom() { + m_is_bottom = true; +} + +void register_types_t::set_to_top() { + m_cur_def = live_registers_t{nullptr}; + m_is_bottom = false; +} + +bool register_types_t::is_bottom() const { return m_is_bottom; } + +bool register_types_t::is_top() const { + if (m_is_bottom) { return false; } + if (m_region_env == nullptr) return true; + for (auto it : m_cur_def) { + if (it != nullptr) return false; + } + return true; +} + +void register_types_t::insert(register_t reg, const reg_with_loc_t& reg_with_loc, + const ptr_or_mapfd_t& type) { + (*m_region_env)[reg_with_loc] = type; + m_cur_def[reg] = std::make_shared(reg_with_loc); +} + +void register_types_t::print_all_register_types() const { + std::cout << "\tregion types: {\n"; + for (auto const& kv : *m_region_env) { + std::cout << "\t\t" << kv.first << " : "; + print_ptr_or_mapfd_type(kv.second); + std::cout << "\n"; + } + std::cout << "\t}\n"; +} + +std::optional register_types_t::find(reg_with_loc_t reg) const { + auto it = m_region_env->find(reg); + if (it == m_region_env->end()) return {}; + return it->second; +} + +std::optional register_types_t::find(register_t key) const { + if (m_cur_def[key] == nullptr) return {}; + const reg_with_loc_t& reg = *(m_cur_def[key]); + return find(reg); +} + +void register_types_t::adjust_bb_for_registers(location_t loc) { + location_t old_loc = location_t(std::make_pair(label_t(-2, -2), 0)); + for (size_t i = 0; i < m_cur_def.size(); i++) { + auto new_reg = reg_with_loc_t((register_t)i, loc); + auto old_reg = reg_with_loc_t((register_t)i, old_loc); + + auto it = find((register_t)i); + if (!it) continue; + + if (*m_cur_def[i] == old_reg) { + m_region_env->erase(old_reg); + } + + m_cur_def[i] = std::make_shared(new_reg); + (*m_region_env)[new_reg] = it.value(); + + } +} + +stack_t stack_t::operator|(const stack_t& other) const { + if (is_bottom() || other.is_top()) { + return other; + } else if (other.is_bottom() || is_top()) { + return *this; + } + ptr_or_mapfd_types_t out_ptrs; + for (auto const&kv: m_ptrs) { + auto maybe_ptr_or_mapfd_cells = other.find(kv.first); + if (maybe_ptr_or_mapfd_cells) { + auto ptr_or_mapfd_cells1 = kv.second; + auto ptr_or_mapfd_cells2 = maybe_ptr_or_mapfd_cells.value(); + auto ptr_or_mapfd1 = ptr_or_mapfd_cells1.first; + auto ptr_or_mapfd2 = ptr_or_mapfd_cells2.first; + int width1 = ptr_or_mapfd_cells1.second; + int width2 = ptr_or_mapfd_cells2.second; + int width_joined = std::max(width1, width2); + if (ptr_or_mapfd1 == ptr_or_mapfd2) { + out_ptrs[kv.first] = std::make_pair(ptr_or_mapfd1, width_joined); + } + else if (std::holds_alternative(ptr_or_mapfd1) && + std::holds_alternative(ptr_or_mapfd2)) { + auto ptr_with_off1 = std::get(ptr_or_mapfd1); + auto ptr_with_off2 = std::get(ptr_or_mapfd2); + if (ptr_with_off1.get_region() == ptr_with_off2.get_region()) { + out_ptrs[kv.first] + = std::make_pair(ptr_with_off1 | ptr_with_off2, width_joined); + } + } + } + } + return stack_t(std::move(out_ptrs), false); +} + +void stack_t::operator-=(uint64_t key) { + auto it = find(key); + if (it) + m_ptrs.erase(key); +} + +void stack_t::operator-=(const std::vector& keys) { + for (auto &key : keys) { + *this -= key; + } +} + +void stack_t::set_to_bottom() { + m_ptrs.clear(); + m_is_bottom = true; +} + +void stack_t::set_to_top() { + m_ptrs.clear(); + m_is_bottom = false; +} + +stack_t stack_t::bottom() { return stack_t(true); } + +stack_t stack_t::top() { return stack_t(false); } + +bool stack_t::is_bottom() const { return m_is_bottom; } + +bool stack_t::is_top() const { + if (m_is_bottom) + return false; + return m_ptrs.empty(); +} + +void stack_t::store(uint64_t key, ptr_or_mapfd_t value, int width) { + m_ptrs[key] = std::make_pair(value, width); +} + +size_t stack_t::size() const { + return m_ptrs.size(); +} + +std::vector stack_t::get_keys() const { + std::vector keys; + keys.reserve(size()); + + for (auto const&kv : m_ptrs) { + keys.push_back(kv.first); + } + return keys; +} + + +std::optional stack_t::find(uint64_t key) const { + auto it = m_ptrs.find(key); + if (it == m_ptrs.end()) return {}; + return it->second; +} + +std::vector stack_t::find_overlapping_cells(uint64_t start, int width) const { + std::vector overlapping_cells; + auto it = m_ptrs.begin(); + while (it != m_ptrs.end() && it->first < start) { + it++; + } + if (it != m_ptrs.begin()) { + it--; + auto key = it->first; + auto width_key = it->second.second; + if (key < start && key+width_key > start) overlapping_cells.push_back(key); + } + + for (; it != m_ptrs.end(); it++) { + auto key = it->first; + if (key >= start && key < start+width) overlapping_cells.push_back(key); + if (key >= start+width) break; + } + return overlapping_cells; +} + +} + +std::optional region_domain_t::find_ptr_or_mapfd_type(register_t reg) const { + return m_registers.find(reg); +} + +bool region_domain_t::is_bottom() const { + if (m_is_bottom) return true; + return (m_stack.is_bottom() || m_registers.is_bottom()); +} + +bool region_domain_t::is_top() const { + if (m_is_bottom) return false; + return (m_stack.is_top() && m_registers.is_top()); +} + +region_domain_t region_domain_t::bottom() { + region_domain_t typ; + typ.set_to_bottom(); + return typ; +} + +void region_domain_t::set_to_bottom() { + m_is_bottom = true; +} + +void region_domain_t::set_to_top() { + m_stack.set_to_top(); + m_registers.set_to_top(); +} + +std::optional region_domain_t::find_ptr_or_mapfd_at_loc(const reg_with_loc_t& reg) const { + return m_registers.find(reg); +} + +size_t region_domain_t::ctx_size() const { + return m_ctx->size(); +} + +std::vector region_domain_t::get_ctx_keys() const { + return m_ctx->get_keys(); +} + +std::vector region_domain_t::get_stack_keys() const { + return m_stack.get_keys(); +} + +std::optional region_domain_t::find_in_ctx(uint64_t key) const { + return m_ctx->find(key); +} + +std::optional region_domain_t::find_in_stack(uint64_t key) const { + return m_stack.find(key); +} + +bool region_domain_t::operator<=(const region_domain_t& abs) const { + /* WARNING: The operation is not implemented yet.*/ + return true; +} + +void region_domain_t::operator|=(const region_domain_t& abs) { + region_domain_t tmp{abs}; + operator|=(std::move(tmp)); +} + +void region_domain_t::operator|=(region_domain_t&& abs) { + if (is_bottom()) { + *this = abs; + return; + } + *this = *this | std::move(abs); +} + +region_domain_t region_domain_t::operator|(const region_domain_t& other) const { + if (is_bottom() || other.is_top()) { + return other; + } + else if (other.is_bottom() || is_top()) { + return *this; + } + return region_domain_t(m_registers | other.m_registers, m_stack | other.m_stack, other.m_ctx); +} + +region_domain_t region_domain_t::operator|(region_domain_t&& other) const { + if (is_bottom() || other.is_top()) { + return std::move(other); + } + else if (other.is_bottom() || is_top()) { + return *this; + } + return region_domain_t(m_registers | std::move(other.m_registers), m_stack | std::move(other.m_stack), other.m_ctx); +} + +region_domain_t region_domain_t::operator&(const region_domain_t& abs) const { + /* WARNING: The operation is not implemented yet.*/ + return abs; +} + +region_domain_t region_domain_t::widen(const region_domain_t& abs) const { + /* WARNING: The operation is not implemented yet.*/ + return abs; +} + +region_domain_t region_domain_t::narrow(const region_domain_t& other) const { + /* WARNING: The operation is not implemented yet.*/ + return other; +} + +std::string region_domain_t::domain_name() const { + return "region_domain"; +} + +int region_domain_t::get_instruction_count_upper_bound() { + /* WARNING: The operation is not implemented yet.*/ + return 0; +} + +string_invariant region_domain_t::to_set() { + return string_invariant{}; +} + +void region_domain_t::operator()(const LoadMapFd &u, location_t loc, int print) { + auto reg = u.dst.v; + auto reg_with_loc = reg_with_loc_t(reg, loc); + const EbpfMapDescriptor& desc = global_program_info.platform->get_map_descriptor(u.mapfd); + const EbpfMapValueType& map_value_type = global_program_info.platform-> + get_map_type(desc.type).value_type; + map_key_size_t map_key_size = desc.key_size; + map_value_size_t map_value_size = desc.value_size; + auto type = mapfd_t(u.mapfd, map_value_type, map_key_size, map_value_size); + m_registers.insert(reg, reg_with_loc, type); +} + +void region_domain_t::operator()(const Call &u, location_t loc, int print) { + std::optional maybe_fd_reg{}; + for (ArgSingle param : u.singles) { + if (param.kind == ArgSingle::Kind::MAP_FD) maybe_fd_reg = param.reg; + break; + } + register_t r0_reg{R0_RETURN_VALUE}; + auto r0 = reg_with_loc_t(r0_reg, loc); + if (u.is_map_lookup) { + if (!maybe_fd_reg) { + m_registers -= r0_reg; + return; + } + auto ptr_or_mapfd = m_registers.find(maybe_fd_reg->v); + if (!ptr_or_mapfd || !std::holds_alternative(ptr_or_mapfd.value())) { + m_registers -= r0_reg; + return; + } + auto mapfd = std::get(ptr_or_mapfd.value()); + auto map_desc = global_program_info.platform->get_map_descriptor(mapfd.get_mapfd()); + if (mapfd.get_value_type() == EbpfMapValueType::MAP) { + const EbpfMapDescriptor& inner_map_desc = global_program_info.platform-> + get_map_descriptor(map_desc.inner_map_fd); + const EbpfMapValueType& inner_map_value_type = global_program_info.platform-> + get_map_type(inner_map_desc.type).value_type; + map_key_size_t inner_map_key_size = inner_map_desc.key_size; + map_value_size_t inner_map_value_size = inner_map_desc.value_size; + auto type = mapfd_t(map_desc.inner_map_fd, inner_map_value_type, + inner_map_key_size, inner_map_value_size); + m_registers.insert(r0_reg, r0, type); + } + else { + auto type = ptr_with_off_t(crab::region_t::T_SHARED, interval_t(number_t(0)), + interval_t(number_t(mapfd.get_value_size()))); + m_registers.insert(r0_reg, r0, type); + } + } + else { + m_registers -= r0_reg; + } +} + +void region_domain_t::operator()(const Packet & u, location_t loc, int print) { + m_registers -= register_t{R0_RETURN_VALUE}; +} + +void region_domain_t::operator()(const Addable& u, location_t loc, int print) { + + auto maybe_ptr_type1 = m_registers.find(u.ptr.v); + auto maybe_ptr_type2 = m_registers.find(u.num.v); + // a -> b <-> !a || b + if (!maybe_ptr_type1 || !maybe_ptr_type2) { + return; + } + std::cout << "Addable assertion fail\n"; +} + +void region_domain_t::operator()(const ValidStore& u, location_t loc, int print) { + + bool is_stack_p = is_stack_pointer(u.mem.v); + auto maybe_ptr_type2 = m_registers.find(u.val.v); + + if (is_stack_p || !maybe_ptr_type2) { + return; + } + std::cout << "Valid store assertion fail\n"; +} + +region_domain_t region_domain_t::setup_entry() { + + std::shared_ptr ctx = std::make_shared(global_program_info.type.context_descriptor); + std::shared_ptr all_types = std::make_shared(); + + register_types_t typ(all_types); + + auto r1 = reg_with_loc_t(R1_ARG, std::make_pair(label_t::entry, static_cast(0))); + auto r10 = reg_with_loc_t(R10_STACK_POINTER, std::make_pair(label_t::entry, static_cast(0))); + + typ.insert(R1_ARG, r1, ptr_with_off_t(crab::region_t::T_CTX, interval_t(number_t(0)))); + typ.insert(R10_STACK_POINTER, r10, ptr_with_off_t(crab::region_t::T_STACK, interval_t(number_t(512)))); + + region_domain_t inv(std::move(typ), crab::stack_t::top(), ctx); + return inv; +} + +void region_domain_t::report_type_error(std::string s, location_t loc) { + std::cout << "type_error at line " << loc->second << " in bb " << loc->first << "\n"; + std::cout << s; + error_location = loc; + set_to_bottom(); +} + +void region_domain_t::operator()(const TypeConstraint& s, location_t loc, int print) { + auto it = find_ptr_or_mapfd_type(s.reg.v); + if (it) { + // it is a pointer or mapfd + ptr_or_mapfd_t ptr_or_mapfd_type = it.value(); + if (std::holds_alternative(ptr_or_mapfd_type)) { + if (s.types == TypeGroup::non_map_fd) return; + if (s.types == TypeGroup::pointer || s.types == TypeGroup::ptr_or_num) return; + ptr_with_off_t ptr_with_off = std::get(ptr_or_mapfd_type); + if (ptr_with_off.get_region() == crab::region_t::T_CTX) { + if (s.types == TypeGroup::ctx) return; + } + else if (ptr_with_off.get_region() == crab::region_t::T_SHARED) { + if (s.types == TypeGroup::shared || s.types == TypeGroup::mem + || s.types == TypeGroup::mem_or_num) return; + } + else { + if (s.types == TypeGroup::stack || s.types == TypeGroup::mem + || s.types == TypeGroup::stack_or_packet + || s.types == TypeGroup::mem_or_num) { + return; + } + } + } + else if (std::holds_alternative(ptr_or_mapfd_type)) { + if (s.types == TypeGroup::non_map_fd) return; + if (s.types == TypeGroup::pointer || s.types == TypeGroup::ptr_or_num) return; + if (s.types == TypeGroup::packet || s.types == TypeGroup::mem + || s.types == TypeGroup::mem_or_num) return; + } + else { + auto map_fd = std::get(ptr_or_mapfd_type); + if (map_fd.has_type_map_programs()) { + if (s.types == TypeGroup::map_fd_programs) return; + } else { + if (s.types == TypeGroup::map_fd) return; + } + } + } + else { + // if we don't know the type, we assume it is a number + if (s.types == TypeGroup::number || s.types == TypeGroup::ptr_or_num + || s.types == TypeGroup::non_map_fd || s.types == TypeGroup::ptr_or_num + || s.types == TypeGroup::mem_or_num) + return; + } + std::cout << "type constraint assert fail: " << s << "\n"; + //exit(1); +} + +void region_domain_t::update_ptr_or_mapfd(ptr_or_mapfd_t&& ptr_or_mapfd, const interval_t&& change, + Bin::Op op, const reg_with_loc_t& reg_with_loc, uint8_t reg) { + if (std::holds_alternative(ptr_or_mapfd)) { + auto ptr_or_mapfd_with_off = std::get(ptr_or_mapfd); + auto offset = ptr_or_mapfd_with_off.get_offset(); + auto updated_offset = op == Bin::Op::ADD ? offset + change : offset - change; + ptr_or_mapfd_with_off.set_offset(updated_offset); + m_registers.insert(reg, reg_with_loc, ptr_or_mapfd_with_off); + } + else if (std::holds_alternative(ptr_or_mapfd)) { + m_registers.insert(reg, reg_with_loc, ptr_or_mapfd); + } + else { + std::cout << "type error: mapfd register cannot be incremented/decremented\n"; + m_registers -= reg; + } +} + +interval_t region_domain_t::do_bin(const Bin& bin, + const std::optional& src_interval_opt, + const std::optional& dst_interval_opt, + const std::optional& src_ptr_or_mapfd_opt, + const std::optional& dst_ptr_or_mapfd_opt, location_t loc) { + + using Op = Bin::Op; + // if both src and dst are numbers, nothing to do in region domain + // if we are doing a move, where src is a number and dst is not set, nothing to do + if ((dst_interval_opt && src_interval_opt) + || (src_interval_opt && !dst_ptr_or_mapfd_opt && bin.op == Op::MOV)) + return interval_t::bottom(); + + ptr_or_mapfd_t src_ptr_or_mapfd, dst_ptr_or_mapfd; + interval_t src_interval, dst_interval; + if (src_ptr_or_mapfd_opt) src_ptr_or_mapfd = std::move(src_ptr_or_mapfd_opt.value()); + if (dst_ptr_or_mapfd_opt) dst_ptr_or_mapfd = std::move(dst_ptr_or_mapfd_opt.value()); + if (src_interval_opt) src_interval = std::move(src_interval_opt.value()); + if (dst_interval_opt) dst_interval = std::move(dst_interval_opt.value()); + + auto reg = reg_with_loc_t(bin.dst.v, loc); + + switch (bin.op) + { + // ra = b, where b is a pointer/mapfd, a numerical register, or a constant; + case Op::MOV: { + // b is a pointer/mapfd + if (src_ptr_or_mapfd_opt) + m_registers.insert(bin.dst.v, reg, src_ptr_or_mapfd); + // b is a numerical register, or constant + else if (dst_ptr_or_mapfd_opt) { + m_registers -= bin.dst.v; + } + break; + } + // ra += b, where ra is a pointer/mapfd, or a numerical register, + // b is a pointer/mapfd, a numerical register, or a constant; + case Op::ADD: { + // adding pointer to another + if (src_ptr_or_mapfd_opt && dst_ptr_or_mapfd_opt) { + if (is_stack_pointer(bin.dst.v)) + m_stack.set_to_top(); + else { + // TODO: handle other cases properly + std::cout << "type error: addition of two pointers\n"; + } + m_registers -= bin.dst.v; + } + // ra is a pointer/mapfd + // b is a numerical register, or a constant + else if (dst_ptr_or_mapfd_opt && src_interval_opt) { + update_ptr_or_mapfd(std::move(dst_ptr_or_mapfd), std::move(src_interval), + bin.op, reg, bin.dst.v); + } + // b is a pointer/mapfd + // ra is a numerical register + else if (src_ptr_or_mapfd_opt && dst_interval_opt) { + update_ptr_or_mapfd(std::move(src_ptr_or_mapfd), std::move(dst_interval), + bin.op, reg, bin.dst.v); + } + // this should not occur + else assert(false); + break; + } + // ra -= b, where ra is a pointer/mapfd + // b is a pointer/mapfd, numerical register, or a constant; + case Op::SUB: { + // b is a pointer/mapfd + if (dst_ptr_or_mapfd_opt && src_ptr_or_mapfd_opt) { + if (std::holds_alternative(dst_ptr_or_mapfd) && + std::holds_alternative(src_ptr_or_mapfd)) { + std::cout << "type error: mapfd registers subtraction not defined\n"; + } + else if (std::holds_alternative(dst_ptr_or_mapfd) && + std::holds_alternative(src_ptr_or_mapfd)) { + auto dst_ptr_or_mapfd_with_off = std::get(dst_ptr_or_mapfd); + auto src_ptr_or_mapfd_with_off = std::get(src_ptr_or_mapfd); + if (dst_ptr_or_mapfd_with_off.get_region() + == src_ptr_or_mapfd_with_off.get_region()) { + m_registers -= bin.dst.v; + return (dst_ptr_or_mapfd_with_off.get_offset() - + src_ptr_or_mapfd_with_off.get_offset()); + } + else + std::cout << + "type error: subtraction between pointers of different region\n"; + } + else if (!same_region(get_ptr(dst_ptr_or_mapfd), get_ptr(src_ptr_or_mapfd))) { + std::cout << "type error: subtraction between pointers of different region\n"; + } + m_registers -= bin.dst.v; + } + // b is a numerical register, or a constant + else if (dst_ptr_or_mapfd_opt && src_interval_opt) { + update_ptr_or_mapfd(std::move(dst_ptr_or_mapfd), std::move(src_interval), + bin.op, reg, bin.dst.v); + } + break; + } + default: { + m_registers -= bin.dst.v; + break; + } + } + return interval_t::bottom(); +} + +void region_domain_t::do_load(const Mem& b, const Reg& target_reg, location_t loc) { + + int width = b.access.width; + int offset = b.access.offset; + Reg basereg = b.access.basereg; + + auto it = m_registers.find(basereg.v); + if (!it) { + std::string s = std::to_string(static_cast(basereg.v)); + std::string desc = std::string("\tloading from an unknown pointer, or from number - r") + s + "\n"; + //report_type_error(desc, loc); + std::cout << desc; + m_registers -= target_reg.v; + return; + } + auto type_basereg = it.value(); + + if (!std::holds_alternative(type_basereg) + || std::get(type_basereg).get_region() == crab::region_t::T_SHARED) { + // loading from either packet, shared region or mapfd does not happen in region domain + m_registers -= target_reg.v; + return; + } + + auto type_with_off = std::get(type_basereg); + auto p_offset = type_with_off.get_offset(); + auto offset_singleton = p_offset.singleton(); + + switch (type_with_off.get_region()) { + case crab::region_t::T_STACK: { + if (!offset_singleton) { + for (auto const& k : m_stack.get_keys()) { + auto start = p_offset.lb(); + auto end = p_offset.ub()+bound_t(offset+width); + if (bound_t((int)k) >= start && bound_t((int)k) < end) { + std::cout << + "stack load at unknown offset, and offset range contains pointers\n"; + break; + } + } + m_registers -= target_reg.v; + } + else { + auto ptr_offset = offset_singleton.value(); + auto load_at = (uint64_t)(ptr_offset + offset); + + auto it = m_stack.find(load_at); + + if (!it) { + // no field at loaded offset in stack + m_registers -= target_reg.v; + return; + } + auto type_loaded = it.value(); + + auto reg = reg_with_loc_t(target_reg.v, loc); + m_registers.insert(target_reg.v, reg, type_loaded.first); + } + break; + } + case crab::region_t::T_CTX: { + + if (!offset_singleton) { + for (auto const& k : m_ctx->get_keys()) { + auto start = p_offset.lb(); + auto end = p_offset.ub()+bound_t(offset+width); + if (bound_t((int)k) >= start && bound_t((int)k) < end) { + std::cout << + "ctx load at unknown offset, and offset range contains pointers\n"; + break; + } + } + m_registers -= target_reg.v; + } + else { + auto ptr_offset = offset_singleton.value(); + auto load_at = (uint64_t)(ptr_offset + offset); + auto it = m_ctx->find(load_at); + + if (!it) { + // no field at loaded offset in ctx + m_registers -= target_reg.v; + return; + } + ptr_no_off_t type_loaded = it.value(); + + auto reg = reg_with_loc_t(target_reg.v, loc); + m_registers.insert(target_reg.v, reg, type_loaded); + } + break; + } + + default: { + assert(false); + } + } +} + +void region_domain_t::do_mem_store(const Mem& b, const Reg& target_reg, location_t loc) { + + int offset = b.access.offset; + Reg basereg = b.access.basereg; + int width = b.access.width; + + // TODO: move generic checks to type domain + auto maybe_basereg_type = m_registers.find(basereg.v); + if (!maybe_basereg_type) { + std::string s = std::to_string(static_cast(basereg.v)); + std::string desc = std::string("\tstoring at an unknown pointer, or from number - r") + s + "\n"; + //report_type_error(desc, loc); + std::cout << desc; + return; + } + auto basereg_type = maybe_basereg_type.value(); + auto targetreg_type = m_registers.find(target_reg.v); + + if (std::holds_alternative(basereg_type)) { + // base register is either CTX_P, STACK_P or SHARED_P + auto basereg_type_with_off = std::get(basereg_type); + + if (basereg_type_with_off.get_region() == crab::region_t::T_STACK) { + auto offset_singleton = basereg_type_with_off.get_offset().singleton(); + if (!offset_singleton) { + std::cout << "type error: storing to a pointer with unknown offset\n"; + return; + } + auto store_at = (uint64_t)offset+(uint64_t)offset_singleton.value(); + // type of basereg is STACK_P + auto overlapping_cells = m_stack.find_overlapping_cells(store_at, width); + m_stack -= overlapping_cells; + + // if targetreg_type is empty, we are storing a number + if (!targetreg_type) return; + + auto type_to_store = targetreg_type.value(); + m_stack.store(store_at, type_to_store, width); + } + else if (basereg_type_with_off.get_region() == crab::region_t::T_CTX) { + // type of basereg is CTX_P + if (targetreg_type) { + std::string s = std::to_string(static_cast(target_reg.v)); + std::string desc = std::string("\twe cannot store a pointer, r") + s + ", into ctx\n"; + // report_type_error(desc, loc); + std::cout << desc; + return; + } + } + else { + // type of basereg is SHARED_P + if (targetreg_type) std::cout << "\twe cannot store a pointer into shared\n"; + } + } + else if (std::holds_alternative(basereg_type)) { + // base register type is a PACKET_P + if (targetreg_type) { + std::string s = std::to_string(static_cast(target_reg.v)); + std::string desc = std::string("\twe cannot store a pointer, r") + s + ", into packet\n"; + //report_type_error(desc, loc); + std::cout << desc; + return; + } + } + else { + std::cout << "\twe cannot store a pointer into a mapfd\n"; + return; + } +} + + +bool region_domain_t::is_stack_pointer(register_t reg) const { + auto type = m_registers.find(reg); + if (!type) { // not a pointer + return false; + } + auto ptr_or_mapfd_type = type.value(); + return (std::holds_alternative(ptr_or_mapfd_type) && + std::get(ptr_or_mapfd_type).get_region() == crab::region_t::T_STACK); +} + +void region_domain_t::adjust_bb_for_types(location_t loc) { + m_registers.adjust_bb_for_registers(loc); +} + +void region_domain_t::print_all_register_types() const { + m_registers.print_all_register_types(); +} diff --git a/src/crab/region_domain.hpp b/src/crab/region_domain.hpp new file mode 100644 index 000000000..b3cb945b7 --- /dev/null +++ b/src/crab/region_domain.hpp @@ -0,0 +1,286 @@ +// Copyright (c) Prevail Verifier contributors. +// SPDX-License-Identifier: MIT + +#pragma once + +#include +#include + +#include "crab/abstract_domain.hpp" +#include "crab/cfg.hpp" +#include "linear_constraint.hpp" +#include "string_constraints.hpp" +#include + +#include "platform.hpp" + +using crab::interval_t; +using crab::bound_t; + +namespace crab { + +enum class region_t { + T_CTX, + T_STACK, + T_PACKET, + T_SHARED +}; + + +class ptr_no_off_t { + region_t m_r; + + public: + ptr_no_off_t() = default; + ptr_no_off_t(const ptr_no_off_t &) = default; + ptr_no_off_t(ptr_no_off_t &&) = default; + ptr_no_off_t &operator=(const ptr_no_off_t &) = default; + ptr_no_off_t &operator=(ptr_no_off_t &&) = default; + ptr_no_off_t(region_t _r) : m_r(_r) {} + + constexpr region_t get_region() const { return m_r; } + void set_region(region_t); + void write(std::ostream&) const; + friend std::ostream& operator<<(std::ostream& o, const ptr_no_off_t& p); + //bool operator==(const ptr_no_off_t& p2); + //bool operator!=(const ptr_no_off_t& p2); +}; + +class ptr_with_off_t { + region_t m_r; + interval_t m_offset; + interval_t m_region_size; + + public: + ptr_with_off_t() = default; + ptr_with_off_t(const ptr_with_off_t &) = default; + ptr_with_off_t(ptr_with_off_t &&) = default; + ptr_with_off_t &operator=(const ptr_with_off_t &) = default; + ptr_with_off_t &operator=(ptr_with_off_t &&) = default; + ptr_with_off_t(region_t _r, interval_t _off, interval_t _region_sz=interval_t::top()) + : m_r(_r), m_offset(_off), m_region_size(_region_sz) {} + ptr_with_off_t operator|(const ptr_with_off_t&) const; + interval_t get_region_size() const; + void set_region_size(interval_t); + interval_t get_offset() const { return m_offset; } + void set_offset(interval_t); + constexpr region_t get_region() const { return m_r; } + void set_region(region_t); + void write(std::ostream&) const; + friend std::ostream& operator<<(std::ostream& o, const ptr_with_off_t& p); + //bool operator==(const ptr_with_off_t& p2); + //bool operator!=(const ptr_with_off_t& p2); +}; + +using map_key_size_t = unsigned int; +using map_value_size_t = unsigned int; + +class mapfd_t { + int m_mapfd; + EbpfMapValueType m_value_type; + map_key_size_t m_key_size; + map_value_size_t m_value_size; + + public: + mapfd_t(const mapfd_t&) = default; + mapfd_t(mapfd_t&&) = default; + mapfd_t &operator=(const mapfd_t&) = default; + mapfd_t &operator=(mapfd_t&&) = default; + mapfd_t(int mapfd, EbpfMapValueType val_type, map_key_size_t key_size, + map_value_size_t value_size) + : m_mapfd(mapfd), m_value_type(val_type), m_key_size(key_size), m_value_size(value_size) {} + friend std::ostream& operator<<(std::ostream&, const mapfd_t&); + void write(std::ostream&) const; + + bool has_type_map_programs() const; + constexpr EbpfMapValueType get_value_type() const { return m_value_type; } + constexpr map_key_size_t get_key_size() const { return m_key_size; } + constexpr map_value_size_t get_value_size() const { return m_value_size; } + constexpr int get_mapfd() const { return m_mapfd; } +}; + +using ptr_t = std::variant; +using register_t = uint8_t; +using location_t = boost::optional>; + +class reg_with_loc_t { + register_t m_reg; + location_t m_loc; + + public: + reg_with_loc_t(register_t _r, location_t _loc) : m_reg(_r), m_loc(_loc) {} + bool operator==(const reg_with_loc_t& other) const; + std::size_t hash() const; + friend std::ostream& operator<<(std::ostream& o, const reg_with_loc_t& reg); + void write(std::ostream& ) const; +}; + +class ctx_t { + using ptr_types_t = std::unordered_map; + + ptr_types_t m_packet_ptrs; + + public: + ctx_t(const ebpf_context_descriptor_t* desc); + size_t size() const; + std::vector get_keys() const; + std::optional find(uint64_t key) const; +}; + +using ptr_or_mapfd_t = std::variant; +using ptr_or_mapfd_cells_t = std::pair; +using ptr_or_mapfd_types_t = std::map; + +class stack_t { + ptr_or_mapfd_types_t m_ptrs; + bool m_is_bottom; + + public: + stack_t(bool is_bottom = false) : m_is_bottom(is_bottom) {} + stack_t(ptr_or_mapfd_types_t && ptrs, bool is_bottom) + : m_ptrs(std::move(ptrs)) , m_is_bottom(is_bottom) {} + + stack_t operator|(const stack_t& other) const; + void operator-=(uint64_t); + void operator-=(const std::vector&); + void set_to_bottom(); + void set_to_top(); + static stack_t bottom(); + static stack_t top(); + bool is_bottom() const; + bool is_top() const; + const ptr_or_mapfd_types_t &get_ptrs() { return m_ptrs; } + void store(uint64_t, ptr_or_mapfd_t, int); + std::optional find(uint64_t) const; + std::vector get_keys() const; + std::vector find_overlapping_cells(uint64_t, int) const; + size_t size() const; +}; + +using live_registers_t = std::array, 11>; +using global_region_env_t = std::unordered_map; + +class register_types_t { + + live_registers_t m_cur_def; + std::shared_ptr m_region_env; + bool m_is_bottom = false; + + public: + register_types_t(bool is_bottom = false) : m_region_env(nullptr), m_is_bottom(is_bottom) {} + explicit register_types_t(live_registers_t&& vars, + std::shared_ptr reg_type_env, bool is_bottom = false) + : m_cur_def(std::move(vars)), m_region_env(reg_type_env), m_is_bottom(is_bottom) {} + + explicit register_types_t(std::shared_ptr reg_type_env, + bool is_bottom = false) + : m_region_env(reg_type_env), m_is_bottom(is_bottom) {} + + register_types_t operator|(const register_types_t& other) const; + void operator-=(register_t var); + void set_to_bottom(); + void set_to_top(); + bool is_bottom() const; + bool is_top() const; + void insert(register_t reg, const reg_with_loc_t& reg_with_loc, const ptr_or_mapfd_t& type); + std::optional find(reg_with_loc_t reg) const; + std::optional find(register_t key) const; + const live_registers_t &get_vars() { return m_cur_def; } + void adjust_bb_for_registers(location_t loc); + void print_all_register_types() const; +}; + +} + +class region_domain_t final { + + bool m_is_bottom = false; + location_t error_location = boost::none; + crab::stack_t m_stack; + crab::register_types_t m_registers; + std::shared_ptr m_ctx; + + public: + + region_domain_t() = default; + region_domain_t(region_domain_t&& o) = default; + region_domain_t(const region_domain_t& o) = default; + region_domain_t& operator=(region_domain_t&& o) = default; + region_domain_t& operator=(const region_domain_t& o) = default; + region_domain_t(crab::register_types_t&& _types, crab::stack_t&& _st, std::shared_ptr _ctx) + : m_stack(std::move(_st)), m_registers(std::move(_types)), m_ctx(_ctx) {} + // eBPF initialization: R1 points to ctx, R10 to stack, etc. + static region_domain_t setup_entry(); + // bottom/top + static region_domain_t bottom(); + void set_to_top(); + void set_to_bottom(); + bool is_bottom() const; + bool is_top() const; + // inclusion + bool operator<=(const region_domain_t& other) const; + // join + void operator|=(const region_domain_t& abs); + void operator|=(region_domain_t&& abs); + region_domain_t operator|(const region_domain_t& other) const; + region_domain_t operator|(region_domain_t&& abs) const; + // meet + region_domain_t operator&(const region_domain_t& other) const; + // widening + region_domain_t widen(const region_domain_t& other) const; + // narrowing + region_domain_t narrow(const region_domain_t& other) const; + //forget + void operator-=(variable_t var); + void operator-=(register_t var) { m_registers -= var; } + + //// abstract transformers + void operator()(const Undefined &, location_t loc = boost::none, int print = 0) {} + void operator()(const Bin &, location_t loc = boost::none, int print = 0) {} + void operator()(const Un &, location_t loc = boost::none, int print = 0) {} + void operator()(const LoadMapFd &, location_t loc = boost::none, int print = 0); + void operator()(const Call &, location_t loc = boost::none, int print = 0); + void operator()(const Exit &, location_t loc = boost::none, int print = 0) {} + void operator()(const Jmp &, location_t loc = boost::none, int print = 0) {} + void operator()(const Mem &, location_t loc = boost::none, int print = 0) {} + void operator()(const Packet &, location_t loc = boost::none, int print = 0); + void operator()(const LockAdd &, location_t loc = boost::none, int print = 0) {} + void operator()(const Assume &, location_t loc = boost::none, int print = 0) {} + void operator()(const Assert &, location_t loc = boost::none, int print = 0) {} + void operator()(const ValidAccess&, location_t loc = boost::none, int print = 0) {} + void operator()(const Comparable&, location_t loc = boost::none, int print = 0) {} + void operator()(const Addable&, location_t loc = boost::none, int print = 0); + void operator()(const ValidStore&, location_t loc = boost::none, int print = 0); + void operator()(const TypeConstraint&, location_t loc = boost::none, int print = 0); + void operator()(const ValidSize&, location_t loc = boost::none, int print = 0) {} + void operator()(const ValidMapKeyValue&, location_t loc = boost::none, int print = 0) {} + void operator()(const ZeroOffset&, location_t loc = boost::none, int print = 0) {} + void operator()(const basic_block_t& bb, bool check_termination, int print = 0) {} + void write(std::ostream& os) const {} + friend std::ostream& operator<<(std::ostream&, const region_domain_t&); + std::string domain_name() const; + int get_instruction_count_upper_bound(); + string_invariant to_set(); + void set_require_check(check_require_func_t f) {} + + void do_load(const Mem&, const Reg&, location_t); + void do_mem_store(const Mem&, const Reg&, location_t); + interval_t do_bin(const Bin&, const std::optional&, + const std::optional&, + const std::optional&, + const std::optional&, location_t); + void update_ptr_or_mapfd(crab::ptr_or_mapfd_t&&, const interval_t&&, Bin::Op, + const crab::reg_with_loc_t&, uint8_t); + + void report_type_error(std::string, location_t); + std::optional find_ptr_or_mapfd_type(register_t) const; + size_t ctx_size() const; + std::optional find_in_ctx(uint64_t key) const; + std::vector get_ctx_keys() const; + std::optional find_in_stack(uint64_t key) const; + std::optional find_ptr_or_mapfd_at_loc(const crab::reg_with_loc_t&) const; + std::vector get_stack_keys() const; + bool is_stack_pointer(register_t) const; + void adjust_bb_for_types(location_t loc); + void print_all_register_types() const; +}; // end region_domain_t diff --git a/src/crab/type_domain.cpp b/src/crab/type_domain.cpp new file mode 100644 index 000000000..0257ba0ce --- /dev/null +++ b/src/crab/type_domain.cpp @@ -0,0 +1,727 @@ +// Copyright (c) Prevail Verifier contributors. +// SPDX-License-Identifier: MIT + +#include + +#include "crab/type_domain.hpp" + +namespace std { + static ptr_t get_ptr(const ptr_or_mapfd_t& t) { + return std::visit( overloaded + { + []( const ptr_with_off_t& x ){ return ptr_t{x};}, + []( const ptr_no_off_t& x ){ return ptr_t{x};}, + []( auto& ) { return ptr_t{};} + }, t + ); + } +} + +static std::string size(int w) { return std::string("u") + std::to_string(w * 8); } + +static void print_ptr_no_off_type(const ptr_no_off_t& ptr, std::optional& dist) { + std::cout << ptr; + if (dist) { + std::cout << "<" << dist.value() << ">"; + } +} + +static void print_ptr_type(const ptr_t& ptr, std::optional& dist) { + if (std::holds_alternative(ptr)) { + ptr_with_off_t ptr_with_off = std::get(ptr); + std::cout << ptr_with_off; + } + else { + ptr_no_off_t ptr_no_off = std::get(ptr); + print_ptr_no_off_type(ptr_no_off, dist); + } +} + +static void print_ptr_or_mapfd_type(const ptr_or_mapfd_t& ptr_or_mapfd, std::optional& d) { + if (std::holds_alternative(ptr_or_mapfd)) { + std::cout << std::get(ptr_or_mapfd); + } + else { + auto ptr = get_ptr(ptr_or_mapfd); + print_ptr_type(ptr, d); + } +} + +static void print_number(interval_t num) { + std::cout << "number"; + if (!num.is_top()) { + std::cout << "<" << num << ">"; + } +} + +static void print_register(Reg r, std::optional& p, std::optional& d, + std::optional n) { + std::cout << r << " : "; + if (p) { + print_ptr_or_mapfd_type(p.value(), d); + } + if (n) { + print_number(n.value()); + } +} + +static void print_annotated(const Call& call, std::optional& p, + std::optional& d, std::optional& n) { + std::cout << " "; + print_register(Reg{(uint8_t)R0_RETURN_VALUE}, p, d, n); + std::cout << " = " << call.name << ":" << call.func << "(...)\n"; +} + +static void print_annotated(const Bin& b, std::optional& p, + std::optional& d, std::optional& n) { + std::cout << " "; + print_register(b.dst, p, d, n); + std::cout << " " << b.op << "= " << b.v << "\n"; +} + +static void print_annotated(const LoadMapFd& u, std::optional& p) { + std::cout << " "; + std::optional d; + std::optional n; + print_register(u.dst, p, d, n); + std::cout << " = map_fd " << u.mapfd << "\n"; +} + +static void print_annotated(const Mem& b, std::optional& p, + std::optional& d, std::optional& n) { + if (b.is_load) { + std::cout << " "; + print_register(std::get(b.value), p, d, n); + std::cout << " = "; + } + std::string sign = b.access.offset < 0 ? " - " : " + "; + int offset = std::abs(b.access.offset); + std::cout << "*(" << size(b.access.width) << " *)"; + std::cout << "(" << b.access.basereg << sign << offset << ")\n"; +} + +bool type_domain_t::is_bottom() const { + return m_is_bottom; +} + +bool type_domain_t::is_top() const { + if (m_is_bottom) return false; + return (m_region.is_top() && m_offset.is_top() && m_interval.is_top()); +} + +type_domain_t type_domain_t::bottom() { + type_domain_t typ; + typ.set_to_bottom(); + return typ; +} + +void type_domain_t::set_to_bottom() { + m_is_bottom = true; +} + +void type_domain_t::set_to_top() { + m_region.set_to_top(); + m_offset.set_to_top(); + m_interval.set_to_top(); +} + +bool type_domain_t::operator<=(const type_domain_t& abs) const { + /* WARNING: The operation is not implemented yet.*/ + return true; +} + +void type_domain_t::operator|=(const type_domain_t& abs) { + type_domain_t tmp{abs}; + operator|=(std::move(tmp)); +} + +void type_domain_t::operator|=(type_domain_t&& abs) { + if (is_bottom()) { + *this = abs; + return; + } + *this = *this | std::move(abs); +} + +type_domain_t type_domain_t::operator|(const type_domain_t& other) const { + if (is_bottom() || other.is_top()) { + return other; + } + else if (other.is_bottom() || is_top()) { + return *this; + } + return type_domain_t(m_region | other.m_region, m_offset | other.m_offset, + m_interval | other.m_interval); +} + +type_domain_t type_domain_t::operator|(type_domain_t&& other) const { + if (is_bottom() || other.is_top()) { + return std::move(other); + } + else if (other.is_bottom() || is_top()) { + return *this; + } + return type_domain_t(m_region | std::move(other.m_region), + m_offset | std::move(other.m_offset), m_interval | std::move(other.m_interval)); +} + +type_domain_t type_domain_t::operator&(const type_domain_t& abs) const { + /* WARNING: The operation is not implemented yet.*/ + return abs; +} + +type_domain_t type_domain_t::widen(const type_domain_t& abs) const { + /* WARNING: The operation is not implemented yet.*/ + return abs; +} + +type_domain_t type_domain_t::narrow(const type_domain_t& other) const { + /* WARNING: The operation is not implemented yet.*/ + return other; +} + +std::string type_domain_t::domain_name() const { + return "type_domain"; +} + +int type_domain_t::get_instruction_count_upper_bound() { + /* WARNING: The operation is not implemented yet.*/ + return 0; +} + +string_invariant type_domain_t::to_set() { + return string_invariant{}; +} + +void type_domain_t::operator()(const Undefined & u, location_t loc, int print) { + if (print > 0) { + std::cout << " " << u << "\n"; + return; + } + m_region(u, loc); + m_offset(u, loc); + m_interval(u, loc); +} + +void type_domain_t::operator()(const Un &u, location_t loc, int print) { + if (print > 0) { + std::cout << " " << u << "\n"; + return; + } + m_interval(u, loc); +} + +void type_domain_t::operator()(const LoadMapFd &u, location_t loc, int print) { + if (print > 0) { + auto reg = reg_with_loc_t(u.dst.v, loc); + auto region = m_region.find_ptr_or_mapfd_at_loc(reg); + print_annotated(u, region); + return; + } + m_region(u, loc); + m_offset(u, loc); + m_interval(u, loc); +} + +void type_domain_t::operator()(const Call &u, location_t loc, int print) { + auto r0 = register_t{R0_RETURN_VALUE}; + + if (print > 0) { + auto r0_reg = reg_with_loc_t(r0, loc); + auto region = m_region.find_ptr_or_mapfd_at_loc(r0_reg); + auto offset = m_offset.find_offset_at_loc(r0_reg); + auto interval = m_interval.find_interval_at_loc(r0_reg); + print_annotated(u, region, offset, interval); + return; + } + + using interval_values_stack_t = std::map; + interval_values_stack_t stack_values; + for (ArgPair param : u.pairs) { + if (param.kind == ArgPair::Kind::PTR_TO_UNINIT_MEM) { + auto maybe_ptr_or_mapfd = m_region.find_ptr_or_mapfd_type(param.mem.v); + auto maybe_width_interval = m_interval.find_interval_value(param.size.v); + if (!maybe_ptr_or_mapfd || !maybe_width_interval) continue; + auto ptr_or_mapfd = maybe_ptr_or_mapfd.value(); + auto width_interval = maybe_width_interval.value(); + if (std::holds_alternative(ptr_or_mapfd)) { + auto ptr_with_off = std::get(ptr_or_mapfd); + if (ptr_with_off.get_region() == region_t::T_STACK) { + auto offset_singleton = ptr_with_off.get_offset().singleton(); + if (!offset_singleton) { + std::cout << "storing at an unknown offset in stack\n"; + continue; + } + auto offset = (uint64_t)offset_singleton.value(); + if (auto single_width = width_interval.singleton(); single_width) { + int width = (int)single_width.value(); + stack_values[offset] = std::make_pair(interval_t::top(), width); + } + } + } + } + } + m_region(u, loc); + m_offset(u, loc); + m_interval.do_call(u, stack_values, loc); +} + +void type_domain_t::operator()(const Exit &u, location_t loc, int print) { + if (print > 0) { + std::cout << " " << u << "\n"; + return; + } + m_region(u, loc); + m_offset(u, loc); + m_interval(u, loc); +} + +void type_domain_t::operator()(const Jmp &u, location_t loc, int print) { + if (print > 0) { + std::cout << " " << u << "\n"; + return; + } + m_region(u, loc); + m_offset(u, loc); + m_interval(u, loc); +} + +void type_domain_t::operator()(const Packet & u, location_t loc, int print) { + if (print > 0) { + std::cout << " " << u << "\n"; + return; + } + m_region(u, loc); + m_offset(u, loc); + m_interval(u, loc); +} + +void type_domain_t::operator()(const LockAdd &u, location_t loc, int print) { + if (print > 0) { + std::cout << " " << u << "\n"; + return; + } + m_region(u, loc); + m_offset(u, loc); + m_interval(u, loc); +} + +void type_domain_t::operator()(const Assume &u, location_t loc, int print) { + if (print > 0) { + std::cout << " " << u << "\n"; + return; + } + Condition cond = u.cond; + auto ptr_or_mapfd = m_region.find_ptr_or_mapfd_type(cond.left.v); + if (ptr_or_mapfd) { + auto ptr_or_mapfd_type = ptr_or_mapfd.value(); + if (std::holds_alternative(ptr_or_mapfd_type)) + m_offset(u, loc); + } + m_interval(u, loc); +} + +void type_domain_t::operator()(const ValidAccess& s, location_t loc, int print) { + auto reg_type = m_region.find_ptr_or_mapfd_type(s.reg.v); + auto interval_type = m_interval.find_interval_value(s.reg.v); + std::optional width_interval = {}; + if (std::holds_alternative(s.width)) { + width_interval = m_interval.find_interval_value(std::get(s.width).v); + } + m_offset.check_valid_access(s, reg_type, interval_type, width_interval); +} + +void type_domain_t::operator()(const TypeConstraint& s, location_t loc, int print) { + m_region(s, loc); +} + +void type_domain_t::operator()(const Assert &u, location_t loc, int print) { + if (print > 0) { + std::cout << " " << u << "\n"; + return; + } + std::visit([this, loc, print](const auto& v) { std::apply(*this, std::make_tuple(v, loc, print)); }, u.cst); +} + +static bool is_mapfd_type(const ptr_or_mapfd_t& ptr_or_mapfd) { + return (std::holds_alternative(ptr_or_mapfd)); +} + +static region_t get_region(const ptr_t& ptr) { + if (std::holds_alternative(ptr)) { + return std::get(ptr).get_region(); + } + else { + return std::get(ptr).get_region(); + } +} + +void type_domain_t::operator()(const Comparable& u, location_t loc, int print) { + if (print > 0) { + std::cout << " " << u << "\n"; + return; + } + + auto maybe_ptr_or_mapfd1 = m_region.find_ptr_or_mapfd_type(u.r1.v); + auto maybe_ptr_or_mapfd2 = m_region.find_ptr_or_mapfd_type(u.r2.v); + auto maybe_interval1 = m_interval.find_interval_value(u.r1.v); + auto maybe_interval2 = m_interval.find_interval_value(u.r2.v); + if (maybe_ptr_or_mapfd1 && maybe_ptr_or_mapfd2) { + if (!maybe_interval1 && !maybe_interval2) { + // an extra check just to make sure registers are not labelled both ptrs and numbers + auto ptr_or_mapfd1 = maybe_ptr_or_mapfd1.value(); + auto ptr_or_mapfd2 = maybe_ptr_or_mapfd1.value(); + if (is_mapfd_type(ptr_or_mapfd1) && is_mapfd_type(ptr_or_mapfd2)) { + return; + } + else if (!is_mapfd_type(ptr_or_mapfd1) && !is_mapfd_type(ptr_or_mapfd2)) { + auto ptr1 = get_ptr(ptr_or_mapfd1); + auto ptr2 = get_ptr(ptr_or_mapfd2); + if (get_region(ptr1) == get_region(ptr2)) { + return; + } + } + } + } + else if (!maybe_ptr_or_mapfd1 && !maybe_ptr_or_mapfd2) { + // all other cases when we do not have a ptr or mapfd, the type is a number + return; + } + std::cout << "Non-comparable types\n"; +} + +void type_domain_t::operator()(const Addable& u, location_t loc, int print) { + if (print > 0) { + std::cout << " " << u << "\n"; + return; + } + m_region(u, loc); +} + +void type_domain_t::operator()(const ValidStore& u, location_t loc, int print) { + if (print > 0) { + std::cout << " " << u << "\n"; + return; + } + m_region(u, loc); +} + + +void type_domain_t::operator()(const ValidSize& u, location_t loc, int print) { + if (print > 0) { + std::cout << " " << u << "\n"; + return; + } + m_interval(u, loc); +} + +void type_domain_t::operator()(const ValidMapKeyValue& u, location_t loc, int print) { + if (print > 0) { + std::cout << " " << u << "\n"; + return; + } + int width; + auto maybe_ptr_or_mapfd_basereg = m_region.find_ptr_or_mapfd_type(u.access_reg.v); + auto maybe_mapfd = m_region.find_ptr_or_mapfd_type(u.map_fd_reg.v); + if (maybe_ptr_or_mapfd_basereg && maybe_mapfd) { + auto ptr_or_mapfd_basereg = maybe_ptr_or_mapfd_basereg.value(); + auto mapfd = maybe_mapfd.value(); + if (is_mapfd_type(mapfd)) { + auto mapfd_type = std::get(mapfd); + if (u.key) { + width = (int)mapfd_type.get_key_size(); + } + else { + width = (int)mapfd_type.get_value_size(); + } + if (std::holds_alternative(ptr_or_mapfd_basereg)) { + auto ptr_with_off = std::get(ptr_or_mapfd_basereg); + if (ptr_with_off.get_region() == region_t::T_STACK) { + auto offset_singleton = ptr_with_off.get_offset().singleton(); + if (!offset_singleton) { + std::cout << "reading the stack at an unknown offset\n"; + return; + } + auto offset_to_check = (uint64_t)offset_singleton.value(); + auto it = m_interval.all_numeric_in_stack(offset_to_check, width); + if (it) return; + auto it2 = m_region.find_in_stack(offset_to_check); + if (it2) { + std::cout << "type error: map update with a non-numerical value\n"; + } + } + } + else if (std::holds_alternative(ptr_or_mapfd_basereg)) { + auto ptr_no_off = std::get(ptr_or_mapfd_basereg); + if (ptr_no_off.get_region() == region_t::T_PACKET) { + if (m_offset.check_packet_access(u.access_reg, width, 0, true)) return; + } + } + } + } + std::cout << "valid map key value assertion failed\n"; +} + +void type_domain_t::operator()(const ZeroOffset& u, location_t loc, int print) { + if (print > 0) { + std::cout << " " << u << "\n"; + return; + } + auto maybe_ptr_or_mapfd = m_region.find_ptr_or_mapfd_type(u.reg.v); + if (maybe_ptr_or_mapfd) { + if (std::holds_alternative(maybe_ptr_or_mapfd.value())) { + auto ptr_type_with_off = std::get(maybe_ptr_or_mapfd.value()); + if (ptr_type_with_off.get_offset() == interval_t(number_t(0))) return; + } + auto maybe_dist = m_offset.find_offset_info(u.reg.v); + if (maybe_dist) { + auto dist_val = maybe_dist.value().m_dist; + auto single_val = dist_val.singleton(); + if (single_val) { + auto dist_value = single_val.value(); + if (dist_value == number_t(0)) return; + } + } + } + std::cout << "Zero Offset assertion fail\n"; +} + +type_domain_t type_domain_t::setup_entry() { + region_domain_t reg = region_domain_t::setup_entry(); + offset_domain_t off = offset_domain_t::setup_entry(); + interval_prop_domain_t cp = interval_prop_domain_t::setup_entry(); + type_domain_t typ(std::move(reg), std::move(off), std::move(cp)); + return typ; +} + +void type_domain_t::operator()(const Bin& bin, location_t loc, int print) { + if (print > 0) { + auto reg_with_loc = reg_with_loc_t(bin.dst.v, loc); + auto region = m_region.find_ptr_or_mapfd_at_loc(reg_with_loc); + auto offset = m_offset.find_offset_at_loc(reg_with_loc); + auto interval = m_interval.find_interval_at_loc(reg_with_loc); + print_annotated(bin, region, offset, interval); + return; + } + + auto dst_ptr_or_mapfd = m_region.find_ptr_or_mapfd_type(bin.dst.v); + auto dst_interval = m_interval.find_interval_value(bin.dst.v); + // both region domain and interval domain should not have a definition for the dst register + assert(!dst_ptr_or_mapfd || !dst_interval); + + std::optional src_ptr_or_mapfd; + std::optional src_interval; + if (std::holds_alternative(bin.v)) { + Reg r = std::get(bin.v); + src_ptr_or_mapfd = m_region.find_ptr_or_mapfd_type(r.v); + src_interval = m_interval.find_interval_value(r.v); + // both region domain and interval domain should not have a definition for the src register + assert(!src_ptr_or_mapfd || !src_interval); + } + else { + auto imm = std::get(bin.v); + src_interval = interval_t(number_t(static_cast(imm.v))); + } + + using Op = Bin::Op; + // for all operations except mov, add, sub, the src and dst should be numbers + if ((src_ptr_or_mapfd || dst_ptr_or_mapfd) + && (bin.op != Op::MOV && bin.op != Op::ADD && bin.op != Op::SUB)) { + std::cout << "type error: operation on pointers not allowed\n"; + m_region -= bin.dst.v; + m_offset -= bin.dst.v; + m_interval -= bin.dst.v; + return; + } + + interval_t subtracted_reg = + m_region.do_bin(bin, src_interval, dst_interval, src_ptr_or_mapfd, dst_ptr_or_mapfd, loc); + interval_t subtracted_off = + m_offset.do_bin(bin, src_interval, dst_interval, src_ptr_or_mapfd, dst_ptr_or_mapfd, loc); + auto subtracted = subtracted_reg.is_bottom() ? subtracted_off : subtracted_reg; + m_interval.do_bin(bin, src_interval, dst_interval, src_ptr_or_mapfd, dst_ptr_or_mapfd, + subtracted, loc); +} + +void type_domain_t::do_load(const Mem& b, const Reg& target_reg, location_t loc, int print) { + + if (print > 0) { + auto target_reg_loc = reg_with_loc_t(target_reg.v, loc); + auto region = m_region.find_ptr_or_mapfd_at_loc(target_reg_loc); + auto offset = m_offset.find_offset_at_loc(target_reg_loc); + auto interval = m_interval.find_interval_at_loc(target_reg_loc); + print_annotated(b, region, offset, interval); + return; + } + + Reg basereg = b.access.basereg; + auto basereg_type = m_region.find_ptr_or_mapfd_type(basereg.v); + + m_region.do_load(b, target_reg, loc); + + auto updated_targetreg_type = m_region.find_ptr_or_mapfd_type(target_reg.v); + + m_interval.do_load(b, target_reg, basereg_type, updated_targetreg_type, loc); + m_offset.do_load(b, target_reg, basereg_type, loc); +} + +void type_domain_t::do_mem_store(const Mem& b, const Reg& target_reg, location_t loc, int print) { + + if (print > 0) { + std::cout << " " << b << ";\n"; + return; + } + + Reg basereg = b.access.basereg; + auto basereg_type = m_region.find_ptr_or_mapfd_type(basereg.v); + auto targetreg_type = m_region.find_ptr_or_mapfd_type(target_reg.v); + + m_region.do_mem_store(b, target_reg, loc); + m_interval.do_mem_store(b, target_reg, basereg_type); + m_offset.do_mem_store(b, target_reg, basereg_type, targetreg_type); +} + +void type_domain_t::operator()(const Mem& b, location_t loc, int print) { + if (std::holds_alternative(b.value)) { + if (b.is_load) { + do_load(b, std::get(b.value), loc, print); + } else { + do_mem_store(b, std::get(b.value), loc, print); + } + } else { + std::string s = std::to_string(static_cast(std::get(b.value).v)); + std::string desc = std::string("\tEither loading to a number (not allowed) or storing a number (not allowed yet) - ") + s + "\n"; + //report_type_error(desc, loc); + std::cout << desc; + return; + } +} + +// the method does not work well as it requires info about the label of basic block we are in +// this info is not available when we are only printing any state +// but it is available when we are processing a basic block for all its instructions:w +// +void type_domain_t::print_registers() const { + std::cout << "\tregister types: {\n"; + for (size_t i = 0; i < NUM_REGISTERS; i++) { + register_t reg = (register_t)i; + auto maybe_ptr_or_mapfd_type = m_region.find_ptr_or_mapfd_type(reg); + auto maybe_offset = m_offset.find_offset_info(reg); + auto maybe_interval = m_interval.find_interval_value(reg); + if (maybe_ptr_or_mapfd_type || maybe_interval) { + std::cout << "\t\t"; + print_register(Reg{(uint8_t)reg}, maybe_ptr_or_mapfd_type, maybe_offset, + maybe_interval); + std::cout << "\n"; + } + } + std::cout << "\t}\n"; +} + +void type_domain_t::print_ctx() const { + std::vector ctx_keys = m_region.get_ctx_keys(); + std::cout << "\tctx: {\n"; + for (auto const& k : ctx_keys) { + auto ptr = m_region.find_in_ctx(k); + auto dist = m_offset.find_in_ctx(k); + if (ptr) { + std::cout << "\t\t" << k << ": "; + print_ptr_type(ptr.value(), dist); + std::cout << ",\n"; + } + } + std::cout << "\t}\n"; +} + +void type_domain_t::print_stack() const { + std::vector stack_keys_region = m_region.get_stack_keys(); + std::vector stack_keys_interval = m_interval.get_stack_keys(); + std::cout << "\tstack: {\n"; + for (auto const& k : stack_keys_region) { + auto maybe_ptr_or_mapfd_cells = m_region.find_in_stack(k); + auto dist = m_offset.find_in_stack(k); + if (maybe_ptr_or_mapfd_cells) { + auto ptr_or_mapfd_cells = maybe_ptr_or_mapfd_cells.value(); + int width = ptr_or_mapfd_cells.second; + auto ptr_or_mapfd = ptr_or_mapfd_cells.first; + std::cout << "\t\t[" << k << "-" << k+width-1 << "] : "; + print_ptr_or_mapfd_type(ptr_or_mapfd, dist); + std::cout << ",\n"; + } + } + for (auto const& k : stack_keys_interval) { + auto maybe_interval_cells = m_interval.find_in_stack(k); + if (maybe_interval_cells) { + auto interval_cells = maybe_interval_cells.value(); + std::cout << "\t\t" << "[" << k << "-" << k+interval_cells.second-1 << "] : "; + print_number(interval_cells.first); + std::cout << ",\n"; + } + } + std::cout << "\t}\n"; +} + +void type_domain_t::adjust_bb_for_types(location_t loc) { + m_region.adjust_bb_for_types(loc); + m_offset.adjust_bb_for_types(loc); + m_interval.adjust_bb_for_types(loc); +} + +void type_domain_t::operator()(const basic_block_t& bb, bool check_termination, int print) { + auto label = bb.label(); + if (print < 0) { + std::cout << "state of stack and ctx in program:\n"; + print_ctx(); + print_stack(); + std::cout << "\n"; + return; + } + if (print > 0) { + if (label == label_t::entry) { + m_is_bottom = false; + } + std::cout << label << ":\n"; + } + + uint32_t curr_pos = 0; + location_t loc = location_t(std::make_pair(label, curr_pos)); + if (print == 0) + adjust_bb_for_types(loc); + + for (const Instruction& statement : bb) { + loc = location_t(std::make_pair(label, ++curr_pos)); + if (print > 0) + std::cout << " " << curr_pos << "."; + //if (print <= 0) std::cout << statement << "\n"; + std::visit([this, loc, print](const auto& v) { std::apply(*this, std::make_tuple(v, loc, print)); }, statement); + //if (print > 0 && error_location->first == loc->first && error_location->second == loc->second) std::cout << "type_error\n"; + } + + if (print > 0) { + auto [it, et] = bb.next_blocks(); + if (it != et) { + std::cout << " " << "goto "; + for (; it != et;) { + std::cout << *it; + ++it; + if (it == et) { + std::cout << ";"; + } else { + std::cout << ","; + } + } + } + std::cout << "\n\n"; + } +} + +void type_domain_t::write(std::ostream& o) const { + if (is_bottom()) { + o << "_|_"; + } +} + +std::ostream& operator<<(std::ostream& o, const type_domain_t& typ) { + typ.write(o); + return o; +} diff --git a/src/crab/type_domain.hpp b/src/crab/type_domain.hpp new file mode 100644 index 000000000..1fbbaa15e --- /dev/null +++ b/src/crab/type_domain.hpp @@ -0,0 +1,100 @@ +// Copyright (c) Prevail Verifier contributors. +// SPDX-License-Identifier: MIT + +#pragma once + +#include + +#include "crab/abstract_domain.hpp" +#include "crab/region_domain.hpp" +#include "crab/interval_prop_domain.hpp" +#include "crab/offset_domain.hpp" +#include "crab/cfg.hpp" +#include "linear_constraint.hpp" +#include "string_constraints.hpp" + +constexpr int NUM_REGISTERS = 11; + +using crab::ptr_or_mapfd_t; +using crab::mapfd_t; +using crab::region_t; + +class type_domain_t final { + region_domain_t m_region; + offset_domain_t m_offset; + interval_prop_domain_t m_interval; + bool m_is_bottom = false; + + public: + + type_domain_t() = default; + type_domain_t(type_domain_t&& o) = default; + type_domain_t(const type_domain_t& o) = default; + explicit type_domain_t(region_domain_t&& reg, offset_domain_t&& off, interval_prop_domain_t&& + interval, bool is_bottom = false) : + m_region(reg), m_offset(off), m_interval(interval), m_is_bottom(is_bottom) {} + type_domain_t& operator=(type_domain_t&& o) = default; + type_domain_t& operator=(const type_domain_t& o) = default; + // eBPF initialization: R1 points to ctx, R10 to stack, etc. + static type_domain_t setup_entry(); + // bottom/top + static type_domain_t bottom(); + void set_to_top(); + void set_to_bottom(); + bool is_bottom() const; + bool is_top() const; + // inclusion + bool operator<=(const type_domain_t& other) const; + // join + void operator|=(const type_domain_t& abs); + void operator|=(type_domain_t&& abs); + type_domain_t operator|(const type_domain_t& other) const; + type_domain_t operator|(type_domain_t&& abs) const; + // meet + type_domain_t operator&(const type_domain_t& other) const; + // widening + type_domain_t widen(const type_domain_t& other) const; + // narrowing + type_domain_t narrow(const type_domain_t& other) const; + //forget + void operator-=(variable_t var); + + //// abstract transformers + void operator()(const Undefined &, location_t loc = boost::none, int print = 0); + void operator()(const Bin &, location_t loc = boost::none, int print = 0); + void operator()(const Un &, location_t loc = boost::none, int print = 0); + void operator()(const LoadMapFd &, location_t loc = boost::none, int print = 0); + void operator()(const Call &, location_t loc = boost::none, int print = 0); + void operator()(const Exit &, location_t loc = boost::none, int print = 0); + void operator()(const Jmp &, location_t loc = boost::none, int print = 0); + void operator()(const Mem &, location_t loc = boost::none, int print = 0); + void operator()(const Packet &, location_t loc = boost::none, int print = 0); + void operator()(const LockAdd &, location_t loc = boost::none, int print = 0); + void operator()(const Assume &, location_t loc = boost::none, int print = 0); + void operator()(const Assert &, location_t loc = boost::none, int print = 0); + void operator()(const ValidAccess&, location_t loc = boost::none, int print = 0); + void operator()(const Comparable&, location_t loc = boost::none, int print = 0); + void operator()(const Addable&, location_t loc = boost::none, int print = 0); + void operator()(const ValidStore&, location_t loc = boost::none, int print = 0); + void operator()(const TypeConstraint&, location_t loc = boost::none, int print = 0); + void operator()(const ValidSize&, location_t loc = boost::none, int print = 0); + void operator()(const ValidMapKeyValue&, location_t loc = boost::none, int print = 0); + void operator()(const ZeroOffset&, location_t loc = boost::none, int print = 0); + void operator()(const basic_block_t& bb, bool check_termination, int print = 0); + void write(std::ostream& os) const; + friend std::ostream& operator<<(std::ostream& o, const type_domain_t& dom); + std::string domain_name() const; + int get_instruction_count_upper_bound(); + string_invariant to_set(); + void set_require_check(check_require_func_t f) {} + + private: + + void do_load(const Mem&, const Reg&, location_t, int print = 0); + void do_mem_store(const Mem&, const Reg&, location_t, int print = 0); + void report_type_error(std::string, location_t); + void print_registers() const; + void print_ctx() const; + void print_stack() const; + void adjust_bb_for_types(location_t); +}; // end type_domain_t diff --git a/src/crab_verifier.cpp b/src/crab_verifier.cpp index 1d262865f..10e5f24ac 100644 --- a/src/crab_verifier.cpp +++ b/src/crab_verifier.cpp @@ -17,6 +17,10 @@ #include "crab/abstract_domain.hpp" #include "crab/ebpf_domain.hpp" +#include "crab/type_domain.hpp" +#include "crab/interval_prop_domain.hpp" +#include "crab/region_domain.hpp" +#include "crab/offset_domain.hpp" #include "crab/fwd_analyzer.hpp" #include "asm_syntax.hpp" @@ -125,7 +129,8 @@ static abstract_domain_t make_initial(const ebpf_verifier_options_t* options) { return abstract_domain_t(entry_inv); } case abstract_domain_kind::TYPE_DOMAIN: { - // TODO + type_domain_t entry_inv = type_domain_t::setup_entry(); + return abstract_domain_t(entry_inv); } default: // FIXME: supported abstract domains should be checked in check.cpp @@ -168,12 +173,27 @@ crab_results get_ebpf_report(std::ostream& s, cfg_t& cfg, program_info info, con crab::run_forward_analyzer(cfg, std::move(entry_dom), options->check_termination); // Analyze the control-flow graph. - checks_db db = generate_report(cfg, pre_invariants, post_invariants); - if (thread_local_options.print_invariants) { + //checks_db db = generate_report(cfg, pre_invariants, post_invariants); + checks_db db; + if (thread_local_options.abstract_domain == abstract_domain_kind::TYPE_DOMAIN) { + auto exit_state = post_invariants.at(label_t::exit); + // only to print ctx and stack, fix later + exit_state(cfg.get_node(label_t::exit), options->check_termination, -1); for (const label_t& label : cfg.sorted_labels()) { - s << "\nPre-invariant : " << pre_invariants.at(label) << "\n"; - s << cfg.get_node(label); - s << "\nPost-invariant: " << post_invariants.at(label) << "\n"; + auto pre_state = pre_invariants.at(label); + auto post_state = post_invariants.at(label); + pre_state(cfg.get_node(label), options->check_termination, + thread_local_options.print_invariants); + } + } + else { + db = generate_report(cfg, pre_invariants, post_invariants); + if (thread_local_options.print_invariants) { + for (const label_t& label : cfg.sorted_labels()) { + s << "\nPre-invariant : " << pre_invariants.at(label) << "\n"; + s << cfg.get_node(label); + s << "\nPost-invariant: " << post_invariants.at(label) << "\n"; + } } } return crab_results(std::move(cfg), std::move(pre_invariants), std::move(post_invariants), std::move(db)); diff --git a/src/ebpf_proof.cpp b/src/ebpf_proof.cpp index 5a6b087f2..58203f08e 100644 --- a/src/ebpf_proof.cpp +++ b/src/ebpf_proof.cpp @@ -1,9 +1,14 @@ +// Copyright (c) Prevail Verifier contributors. +// SPDX-License-Identifier: MIT + #include "ebpf_proof.hpp" bool ebpf_generate_proof(std::ostream& s, const InstructionSeq& prog, const program_info& info, const ebpf_verifier_options_t* options, const crab_results& results) { + if (!results.pass_verify()) { // If the program is not correct then we cannot generate a proof + std::cout << "Proof generation not implemented\n"; return false; } @@ -18,6 +23,5 @@ bool ebpf_generate_proof(std::ostream& s, const InstructionSeq& prog, const prog implement it so that we can be sure that our types are correct. */ - s << "TODO: proof\n"; return false; } diff --git a/src/ebpf_proof.hpp b/src/ebpf_proof.hpp index 65e479758..8137e019b 100644 --- a/src/ebpf_proof.hpp +++ b/src/ebpf_proof.hpp @@ -5,6 +5,7 @@ #include "config.hpp" #include "crab/cfg.hpp" #include "crab_verifier.hpp" +#include "crab/type_domain.hpp" // - prog is a prevail representation of the eBPF program // - results contains the Crab CFG together with the inferred invariants diff --git a/src/main/check.cpp b/src/main/check.cpp index 093e28eca..d15a322ee 100644 --- a/src/main/check.cpp +++ b/src/main/check.cpp @@ -45,7 +45,7 @@ int main(int argc, char** argv) { app.add_flag("-l", list, "List sections"); std::string domain = "zoneCrab"; - std::set doms{"stats", "linux", "zoneCrab", "cfg"}; + std::set doms{"stats", "linux", "zoneCrab", "cfg", "type"}; app.add_set("-d,--dom,--domain", domain, doms, "Abstract domain")->type_name("DOMAIN"); app.add_flag("--termination", ebpf_verifier_options.check_termination, "Verify termination"); @@ -145,8 +145,11 @@ int main(int argc, char** argv) { print_map_descriptors(global_program_info.map_descriptors, out); } - if (domain == "zoneCrab") { + if (domain == "zoneCrab" || domain == "type") { ebpf_verifier_stats_t verifier_stats; + if (domain == "type") { + ebpf_verifier_options.abstract_domain = abstract_domain_kind::TYPE_DOMAIN; + } auto [res, seconds] = timed_execution([&] { return ebpf_verify_program(std::cout, prog, raw_prog.info, &ebpf_verifier_options, &verifier_stats); }); @@ -155,9 +158,11 @@ int main(int argc, char** argv) { } std::cout << res.pass_verify() << "," << seconds << "," << resident_set_size_kb() << "\n"; + /* if (gen_proof) { ebpf_generate_proof(std::cout, prog, raw_prog.info, &ebpf_verifier_options, res); } + */ return !res.pass_verify(); } else if (domain == "linux") {