Support different word sizes for distinct memory regions #466
Comments
|
@priyasiddharth talk to @igcontreras . Prepreq for this is to compute for each dsa-node the minimum alignment required. |
|
I've prototyped local memory IIUC To reproduce: @igcontreras I would appreciate if you can tell me what I am missing or change |
|
I don't know if Also, I don't know if this could be an issue but on line 1197 there is an assert that the destination of the copy has a cell (https://github.com/seahorn/sea-dsa/blob/master/src/DsaLocal.cc#L1197) but then it is not used, a new cell is created: https://github.com/seahorn/sea-dsa/blob/master/src/DsaLocal.cc#L1203 |
|
@priyasiddharth can you provide more information about what is known about the node in question. It is likely that the node in question is not collapsed. This would be an expected result. A node is collapsed if its fields are used in some complex way. This node probably has no fields, so there is no reason to collapse it. The node might be labeled as a sequence/array. It is possible that the node is not marked as anything since DSA mostly cares about memory that stores pointers, but this node might not have any pointers in it. In summary, we need to refine when we classify a node as aligned. One simple addition is to check whether it is a destination of any unaligned memcpy, for example. |
|
@priyasiddharth you can run the to see memory looks like. |
|
This is one instruction This is the associated |
|
great. it is marked as |
|
I don't know how to answer that question unambiguously. Perhaps you mean to ask if the compiler can statically infer the size of the data structure. The answer appears to be no since it is non deterministic. |
|
Use these API to check whether the node is an Array/Sequence, and, optionally, if the element size is 1: The rule is then,
You should be able to add this easily to the existing code you have to see if this solves the immediate problem. |
|
One insight (atleast for me) is that there is difference in semantics of memory defined using Problem definitionWhen copying bytes where source access is unaligned and dest access is aligned, in SolutionOne solution is to propagate the unaligned access property such that if one of source or dest is unaligned, the other is too. This would make sure that if one memory is unaligned then all memories interacting with are unaligned too. This is drastic and perf would likely be close to what it is today ... setting everything to Case 1 (src=unaligned (byte access), dst = aligned)After memory is joined and a A ite(cond,
array::select(dstarray, dst_index),
bv::concat(
array::select(srcarray, src_index),
array::select(srcarray, alu::add(src_index, 1),
array::select(srcarray, alu::add(src_index, 2),
array::select(srcarray, alu::add(src_index, 3))Case 2 (src=aligned, dst = unaligned)After memory is joined and a A ite(cond,
array::select(dstarray, dst_index),
bv::extract(array::select(srcarray,
getBase(src_index)),
alu::mult(getOffset(src_indx), 8) /* start extract (in bits) */,
8 /* len in bits */) ) The following is a distilled test that should pass once this logic is implemented. It is also a useful artifact to study what is happening under-the-hood. #include <stdbool.h>
#include <stdint.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include "seahorn/seahorn.h"
extern bool nd_bool();
extern uint32_t nd_uint32();
extern char nd_char();
extern size_t nd_size();
extern void memhavoc(void *ptr, size_t size);
extern void sea_printf(const char *format, ...);
typedef struct {
char *data;
size_t len;
} Buffer;
/**
* This program copies data from one buffer to another using memcpy.
* The source access is unaligned. The dest access is aligned.
**/
int main() {
// create Buffer b with havoc'ed data
size_t len = nd_size();
char *data = (char *) malloc(len);
assume(len < 16);
memhavoc(data, len);
Buffer b = {.data = data, .len = len};
// choose an unaligned offset to copy from
size_t offset = nd_size();
size_t copylen = nd_size();
// The copylen is a multiple of word size
assume (copylen % 8 == 0);
size_t hot_idx = nd_size();
assume (hot_idx < copylen);
assume (offset < len);
assume (copylen < len);
assume (offset + copylen < len);
// create Buffer b2 with havoc'ed data
size_t len2 = nd_size();
assume (len < len2);
assume(len2 < 24);
char *data2 = (char *) malloc(len2);
memhavoc(data2, len2);
Buffer b2 = {.data = data2, .len = len2};
// non deterministically record a byte from source address
char oldbyte = *(b.data + offset + hot_idx);
// operation under verification
// src access is unaligned
// dst access is aligned
memcpy(b2.data, b.data + offset, copylen);
// record same byte from dest address
char newbyte = *(b2.data + 0 + hot_idx);
sea_printf("len:%ld len2:%ld: offset:%ld copylen:%ld hotidx: %ld", len, len2, offset, copylen, hot_idx);
sassert(oldbyte == newbyte);
} |
|
Lets talk. If there is a difference in semantics, it is unintentional. sea-dsa treats sea-dsa does not care about alignment of memcpy. BvOpSem should support all forms of alignment (eventually). When it was written, there was only one alignment mark for memcpy that applied to both source and destination. Now, there are separate alignment for source and dest. |
Is your feature request related to a problem? Please describe.
Today, we use a single word size for all memory. This is not optimal. A memory region may only be accessed in an aligned (word) granularity or may need to support byte-wise access. For such situations, we degrade to using byte access for all memories leading to more complex VC. We would like to keep word accesses VCs wherever it is correct.
Describe the solution you'd like
Infer an alignment type for each memory region and compute access strategy based on that.
For more discussion see (private) post in: https://seahornteam.slack.com/archives/C042CLDJDA7/p1667577583935569
The text was updated successfully, but these errors were encountered: