smack icon indicating copy to clipboard operation
smack copied to clipboard

Memory instructions from the SplitAggregateValue pass are unnecessarrily checked in memory-safety mode

Open keram88 opened this issue 3 years ago • 0 comments

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
  ...

keram88 avatar Mar 17 '21 23:03 keram88