Revert "Stack memory tracking improvements" (vbpf#613)

This reverts commit 934951e. ---- Signed-off-by: Elazar Gershuni <[email protected]>
dthaler · Apr 11, 2024 · 28ce3ea · 28ce3ea
1 parent 934951e
commit 28ce3ea
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 207 deletions.
diff --git a/src/crab/array_domain.cpp b/src/crab/array_domain.cpp
@@ -110,9 +110,9 @@ class cell_t final {
         return {number_t{static_cast<int>(o)}, number_t{static_cast<int>(o)} + number_t{static_cast<int>(size - 1)}};
     }
 
-  public:
     [[nodiscard]] interval_t to_interval() const { return to_interval(_offset, _size); }
 
+  public:
     [[nodiscard]] bool is_null() const { return _offset == 0 && _size == 0; }
 
     [[nodiscard]] offset_t get_offset() const { return _offset; }
@@ -447,72 +447,6 @@ std::ostream& operator<<(std::ostream& o, offset_map_t& m) {
     return o;
 }
 
-// Create a new cell that is a subset of an existing cell.
-void array_domain_t::split_cell(NumAbsDomain& inv, data_kind_t kind, int cell_start_index, unsigned int len) {
-    assert(kind == data_kind_t::svalues || kind == data_kind_t::uvalues);
-
-    // Get the values from the indicated stack range.
-    std::optional<linear_expression_t> svalue = load(inv, data_kind_t::svalues, number_t(cell_start_index), len);
-    std::optional<linear_expression_t> uvalue = load(inv, data_kind_t::uvalues, number_t(cell_start_index), len);
-
-    // Create a new cell for that range.
-    offset_map_t& offset_map = lookup_array_map(kind);
-    cell_t new_cell = offset_map.mk_cell(cell_start_index, len);
-    inv.assign(new_cell.get_scalar(data_kind_t::svalues), svalue);
-    inv.assign(new_cell.get_scalar(data_kind_t::uvalues), uvalue);
-}
-
-// Prepare to havoc bytes in the middle of a cell by potentially splitting the cell if it is numeric,
-// into the part to the left of the havoced portion, and the part to the right of the havoced portion.
-void array_domain_t::split_number_var(NumAbsDomain& inv, data_kind_t kind, const linear_expression_t& i,
-                                      const linear_expression_t& elem_size) {
-    assert(kind == data_kind_t::svalues || kind == data_kind_t::uvalues);
-    offset_map_t& offset_map = lookup_array_map(kind);
-    interval_t ii = inv.eval_interval(i);
-    std::optional<number_t> n = ii.singleton();
-    if (!n) {
-        // We can only split a singleton offset.
-        return;
-    }
-    interval_t i_elem_size = inv.eval_interval(elem_size);
-    std::optional<number_t> n_bytes = i_elem_size.singleton();
-    if (!n_bytes) {
-        // We can only split a singleton size.
-        return;
-    }
-    auto size = static_cast<unsigned int>(*n_bytes);
-    offset_t o((uint64_t)*n);
-
-    std::vector<cell_t> cells = offset_map.get_overlap_cells(o, size);
-    for (cell_t const& c : cells) {
-        interval_t intv = c.to_interval();
-        int cell_start_index = (int)*intv.lb().number();
-        int cell_end_index = (int)*intv.ub().number();
-
-        if (!this->num_bytes.all_num(cell_start_index, cell_end_index + 1) || (cell_end_index + 1 < cell_start_index + sizeof(int64_t))) {
-            // We can only split numeric cells of size 8 or less.
-            continue;
-        }
-
-        std::optional<number_t> old_number = inv.eval_interval(c.get_scalar(kind)).singleton();
-        if (!old_number) {
-            // We can only split cells with a singleton value.
-            continue;
-        }
-        int64_t old_sint = old_number->cast_to_sint64();
-        uint64_t old_uint = old_number->cast_to_uint64();
-
-        if (cell_start_index < o) {
-            // Use the bytes to the left of the specified range.
-            split_cell(inv, kind, cell_start_index, (unsigned int)(o - cell_start_index));
-        }
-        if (o + size - 1 < cell_end_index) {
-            // Use the bytes to the right of the specified range.
-            split_cell(inv, kind, (int)(o + size), (unsigned int)(cell_end_index - (o + size - 1)));
-        }
-    }
-}
-
 // we can only treat this as non-member because we use global state
 static std::optional<std::pair<offset_t, unsigned>>
 kill_and_find_var(NumAbsDomain& inv, data_kind_t kind, const linear_expression_t& i, const linear_expression_t& elem_size) {
@@ -688,22 +622,11 @@ std::optional<linear_expression_t> array_domain_t::load(NumAbsDomain& inv, data_
     return {};
 }
 
-// We are about to write to a given range of bytes on the stack.
-// Any cells covering that range need to be removed, and any cells that only
-// partially cover that range can be split such that any non-covered portions become new cells.
-static std::optional<std::pair<offset_t, unsigned>> split_and_find_var(array_domain_t& array_domain, NumAbsDomain& inv, data_kind_t kind, const linear_expression_t& idx, const linear_expression_t& elem_size) {
-    if (kind == data_kind_t::svalues || kind == data_kind_t::uvalues) {
-        array_domain.split_number_var(inv, kind, idx, elem_size);
-    }
-    return kill_and_find_var(inv, kind, idx, elem_size);
-}
-
-
 std::optional<variable_t> array_domain_t::store(NumAbsDomain& inv, data_kind_t kind,
                                                 const linear_expression_t& idx,
                                                 const linear_expression_t& elem_size,
                                                 const linear_expression_t& val) {
-    auto maybe_cell = split_and_find_var(*this, inv, kind, idx, elem_size);
+    auto maybe_cell = kill_and_find_var(inv, kind, idx, elem_size);
     if (maybe_cell) {
         // perform strong update
         auto [offset, size] = *maybe_cell;
@@ -725,7 +648,7 @@ std::optional<variable_t> array_domain_t::store_type(NumAbsDomain& inv,
                                                      const linear_expression_t& elem_size,
                                                      const linear_expression_t& val) {
     auto kind = data_kind_t::types;
-    auto maybe_cell = split_and_find_var(*this, inv, kind, idx, elem_size);
+    auto maybe_cell = kill_and_find_var(inv, kind, idx, elem_size);
     if (maybe_cell) {
         // perform strong update
         auto [offset, size] = *maybe_cell;
@@ -748,7 +671,7 @@ std::optional<variable_t> array_domain_t::store_type(NumAbsDomain& inv,
 }
 
 void array_domain_t::havoc(NumAbsDomain& inv, data_kind_t kind, const linear_expression_t& idx, const linear_expression_t& elem_size) {
-    auto maybe_cell = split_and_find_var(*this, inv, kind, idx, elem_size);
+    auto maybe_cell = kill_and_find_var(inv, kind, idx, elem_size);
     if (maybe_cell && kind == data_kind_t::types) {
         auto [offset, size] = *maybe_cell;
         num_bytes.havoc(offset, size);

diff --git a/src/crab/array_domain.hpp b/src/crab/array_domain.hpp
@@ -87,10 +87,6 @@ class array_domain_t final {
     // Perform array stores over an array segment
     void store_numbers(NumAbsDomain& inv, variable_t _idx, variable_t _width);
 
-    void split_number_var(NumAbsDomain& inv, data_kind_t kind, const linear_expression_t& i,
-                          const linear_expression_t& elem_size);
-    void split_cell(NumAbsDomain& inv, data_kind_t kind, int cell_start_index, unsigned int len);
-
     void initialize_numbers(int lb, int width);
 };
 

diff --git a/test-data/stack.yaml b/test-data/stack.yaml
@@ -1,128 +1,6 @@
 # Copyright (c) Prevail Verifier contributors.
 # SPDX-License-Identifier: MIT
 ---
-test-case: stack load 16 bits across multiple variables
-
-pre: ["r10.type=stack", "r10.stack_offset=512",
-      "s[504...504].type=number", "s[504...504].svalue=1", "s[504...504].uvalue=1",
-      "s[505...505].type=number", "s[505...505].svalue=2", "s[505...505].uvalue=2"]
-
-code:
-  <start>: |
-    r0 = *(u16 *)(r10 - 8) ; load 2 bytes spanning s[504...505]: 0x01 and 0x02 -> 0x0201
-
-post:
-  - r10.type=stack
-  - r10.stack_offset=512
-  - s[504...505].type=number
-  - s[504].svalue=1
-  - s[504].uvalue=1
-  - s[505].svalue=2
-  - s[505].uvalue=2
-  - r0.type=number
-  - r0.svalue=513
-  - r0.uvalue=513
----
-test-case: stack load 32 bits across multiple variables
-
-pre: ["r10.type=stack", "r10.stack_offset=512",
-      "s[504...505].type=number", "s[504...505].svalue=22136", "s[504...505].uvalue=22136",
-      "s[506...507].type=number", "s[506...507].svalue=4660", "s[506...507].uvalue=4660"]
-
-code:
-  <start>: |
-    r0 = *(u32 *)(r10 - 8) ; load s[504...507]: 0x5678 and 0x1234 -> 0x12345678 on little-endian
-
-post:
-  - r10.type=stack
-  - r10.stack_offset=512
-  - s[504...507].type=number
-  - s[504...505].svalue=22136
-  - s[504...505].uvalue=22136
-  - s[506...507].svalue=4660
-  - s[506...507].uvalue=4660
-  - r0.type=number
-  - r0.svalue=305419896
-  - r0.uvalue=305419896
----
-test-case: stack load 64 bits across multiple variables
-
-pre: ["r10.type=stack", "r10.stack_offset=512",
-      "s[504...507].type=number", "s[504...507].svalue=2596069104", "s[504...507].uvalue=2596069104",
-      "s[508...511].type=number", "s[508...511].svalue=305419896", "s[508...511].uvalue=305419896"]
-
-code:
-  <start>: |
-    r0 = *(u64 *)(r10 - 8) ; load s[504...511]: 0x9abcdef0 and 0x12345678 -> 0x123456789abcdef0 on little-endian
-
-post:
-  - r10.type=stack
-  - r10.stack_offset=512
-  - s[504...511].type=number
-  - s[504...507].svalue=2596069104
-  - s[504...507].uvalue=2596069104
-  - s[508...511].svalue=305419896
-  - s[508...511].uvalue=305419896
-  - r0.type=number
-  - r0.svalue=1311768467463790320
-  - r0.uvalue=1311768467463790320
----
-test-case: stack re-assign immediate first
-
-pre: ["r10.type=stack", "r10.stack_offset=512",
-      "s[504...511].type=number", "s[504...511].svalue=1311768467463790320", "s[504...511].uvalue=1311768467463790320"]
-
-code:
-  <start>: |
-    *(u32 *)(r10 - 8) = 0 ; zero the first four bytes of 0x123456789abcdef0 -> 0x12345678 on little-endian machine
-
-post:
-  - r10.type=stack
-  - r10.stack_offset=512
-  - s[504...511].type=number
-  - s[504...507].svalue=0
-  - s[504...507].uvalue=0
-  - s[508...511].svalue=305419896
-  - s[508...511].uvalue=305419896
----
-test-case: stack re-assign immediate middle
-
-pre: ["r10.type=stack", "r10.stack_offset=512",
-      "s[504...511].type=number", "s[504...511].svalue=1311768467463790320", "s[504...511].uvalue=1311768467463790320"]
-
-code:
-  <start>: |
-    *(u32 *)(r10 - 6) = 0 ; zero the first four bytes of 0x123456789abcdef0
-
-post:
-  - r10.type=stack
-  - r10.stack_offset=512
-  - s[504...511].type=number
-  - s[504...505].svalue=57072
-  - s[504...505].uvalue=57072
-  - s[506...509].svalue=0
-  - s[506...509].uvalue=0
-  - s[510...511].svalue=4660
-  - s[510...511].uvalue=4660
----
-test-case: stack re-assign immediate last
-
-pre: ["r10.type=stack", "r10.stack_offset=512",
-      "s[504...511].type=number", "s[504...511].svalue=1311768467463790320", "s[504...511].uvalue=1311768467463790320"]
-
-code:
-  <start>: |
-    *(u32 *)(r10 - 4) = 0 ; zero the last four bytes of 0x123456789abcdef0
-
-post:
-  - r10.type=stack
-  - r10.stack_offset=512
-  - s[504...511].type=number
-  - s[504...507].svalue=2596069104
-  - s[504...507].uvalue=2596069104
-  - s[508...511].svalue=0
-  - s[508...511].uvalue=0
----
 test-case: set numeric size
 
 pre: ["r1.type=number",