smack
smack copied to clipboard
Memory instructions from the SplitAggregateValue pass are unnecessarrily checked in memory-safety mode
We model accesses to aggregate values by adding load/store
instructions to the IR to match corresponding store/load
instructions. This requires pointer arithmetic which is later instrumented for checking by the MemorySafety
pass. Metadata annotations my be able to mark these operations to bypass checking, but there may be a better approach.
Below is an example of these checks being added:
bb18:
%26 = call { i8*, i64 } @fun()
store { i8*, i64 } %26, { i8*, i64 }* %2
br label %bb19
The SplitAggregateValue
pass adds the following:
bb18:
%26 = call { i8*, i64 } @fun()
%27 = extractvalue { i8*, i64 } %26, 0
%28 = getelementptr { i8*, i64 }, { i8*, i64 }* %2, i32 0, i32 0
store i8* %27, i8** %28
...
And a memory safety check is added to the getelementptr
:
bb18: ; preds = %bb16
%26 = call { i8*, i64 } @fun()
%27 = extractvalue { i8*, i64 } %26, 0
%28 = getelementptr { i8*, i64 }, { i8*, i64 }* %2, i32 0, i32 0
%bi1 = bitcast i8** %28 to i8*
%bi2 = bitcast i8* inttoptr (i64 8 to i8*) to i8*
call void @__SMACK_check_memory_safety(i8* %bi1, i8* %bi2)
store i8* %27, i8** %28
...