Support the llvm.experimental.noalias.scope.decl intrinsic

[RyanGlScott]

C has a restrict mechanism that lets you indicate whether two pointers cannot alias. Here is an example based off of these slides:

// p0 will not alias with p1
void foo(int* restrict p0, int* restrict p1) {
	*p0 = *p1;
}

Prior to LLVM 12, restrict would compile to a noalias annotation, which crucible-llvm ignores¹:

define dso_local void @foo(i32* noalias nocapture %0, i32* noalias nocapture readonly %1) local_unnamed_addr #0 !dbg !7 {
  call void @llvm.dbg.value(metadata i32* %0, metadata !14, metadata !DIExpression()), !dbg !16
  call void @llvm.dbg.value(metadata i32* %1, metadata !15, metadata !DIExpression()), !dbg !16
  %3 = load i32, i32* %1, align 4, !dbg !17, !tbaa !18
  store i32 %3, i32* %0, align 4, !dbg !22, !tbaa !18
  ret void, !dbg !23
}

In LLVM 12 or later, however, the noalias annotation was replaced with a dedicated llvm.experimental.noalias.scope.decl intrinsic. Here is a standalone program that can be used to make Clang emit this intrinsic:

void foo(int* restrict p0, int* restrict p1) {
	*p0 = *p1;
}

__attribute__((noinline)) void test_inline_foo(int* p0, int* p1) {
	foo(p0, p1);
}

int main(void) {
    int p0 = 0;
    int p1 = 1;
    test_inline_foo(&p0, &p1);
    return 0;
}

Clang 14.0.0 will compile this to:

; Function Attrs: mustprogress nofree norecurse nosync nounwind uwtable willreturn
define dso_local void @foo(i32* noalias nocapture noundef writeonly %0, i32* noalias nocapture noundef readonly %1) local_unnamed_addr #0 !dbg !9 {
  call void @llvm.dbg.value(metadata i32* %0, metadata !16, metadata !DIExpression()), !dbg !18
  call void @llvm.dbg.value(metadata i32* %1, metadata !17, metadata !DIExpression()), !dbg !18
  %3 = load i32, i32* %1, align 4, !dbg !19, !tbaa !20
  store i32 %3, i32* %0, align 4, !dbg !24, !tbaa !20
  ret void, !dbg !25
}

; Function Attrs: mustprogress nofree noinline nosync nounwind uwtable willreturn
define dso_local void @test_inline_foo(i32* nocapture noundef writeonly %0, i32* nocapture noundef readonly %1) local_unnamed_addr #1 !dbg !26 {
  call void @llvm.dbg.value(metadata i32* %0, metadata !30, metadata !DIExpression()), !dbg !32
  call void @llvm.dbg.value(metadata i32* %1, metadata !31, metadata !DIExpression()), !dbg !32
  call void @llvm.experimental.noalias.scope.decl(metadata !33), !dbg !36
  call void @llvm.experimental.noalias.scope.decl(metadata !37), !dbg !36
  call void @llvm.dbg.value(metadata i32* %0, metadata !16, metadata !DIExpression()), !dbg !39
  call void @llvm.dbg.value(metadata i32* %1, metadata !17, metadata !DIExpression()), !dbg !39
  %3 = load i32, i32* %1, align 4, !dbg !41, !tbaa !20, !alias.scope !37, !noalias !33
  store i32 %3, i32* %0, align 4, !dbg !42, !tbaa !20, !alias.scope !33, !noalias !37
  ret void, !dbg !43
}

Unfortunately, crucible-llvm cannot handle this intrinsic out of the box:

$ ~/Software/crux-llvm-0.8/bin/crux-llvm test.c 
[Crux] Using pointer width: 64 for file crux-build/crux~test.bc
[Crux] Simulating function main
[Crux] Attempting to prove verification conditions.
[Crux] *** debug executable: results/test/debug-6
[Crux] *** break on line: 6
[Crux] Found counterexample for verification goal
[Crux]   test.c:6:2: error: in test_inline_foo
[Crux]   unsupported LLVM value: ValMd (ValMdNode [Just (ValMdRef 24)]) of type metadata
[Crux] Goal status:
[Crux]   Total: 1
[Crux]   Proved: 0
[Crux]   Disproved: 1
[Crux]   Incomplete: 0
[Crux]   Unknown: 0
[Crux] Overall status: Invalid.

The problem is revealed in the unsupported LLVM value: ValMd (ValMdNode [Just (ValMdRef 24)]) of type metadata part of the error: the llvm.experimental.noalias.scope.decl intrinsic takes a metadata value as an argument, and crucible-llvm currently does not support any intrinsics that accept metadata values as arguments². In fact, crucible-llvm doesn't even support translating metadata values, which is what leads to the error message above.

The most expedient course of action would be to figure out how to make crucible-llvm treat calls to this intrinsic as a no-op. The main barrier is figuring out how to translate metadata values. Perhaps these can be translated to a trivial Crucible representation (e.g., UnitRepr).

---

¹Perhaps crucible-llvm shouldn't ignore this, but that's a discussion for another issue.
²Strictly speaking, crucible-llvm does handle some llvm.dbg.* intrinsics that accept metadata values as arguments, but these are done in a very ad hoc, special-cased fashion. See this code.

[thinkmoore]

FWIW, there are some interesting things that handling metadata during symbolic execution can enable, such as checking validity of debug info a la this work: https://convolv.es/talks/testing-debug-info/

I don't think it should weigh too much on our deliberations about this issue, but it could be a gentle point in favor of leaving the door open for processing metadata.

It also occurs to me that actually processing these declarations might help by allowing things like under-constrained symbolic execution to respect/check aliasing requirements.

[sauclovian-g]

Sooner or later there'll be a spec you can't prove unless you can reason about (non)aliasing of pointers, so I'd agree with the last part. FWIW

[RyanGlScott]

Thinking about this some more, I don't think that encoding metadata values as Crucible simulator values is a good idea, mainly because it would be annoying to figure out how to mux everything that can appear inside a metadata value. Moreover, if we do want to reason about the behavior of llvm.experimental.noalias.scope.decl later, then a better way to do it would be to extend LLVMStmt with a data constructor that handles llvm.experimental.noalias.scope.decl. (Perhaps we could call it LLVM_NoAlias or something similar.) This mirrors the way we handle certain llvm.dbg.* statements by having a dedicated LLVM_Dbg data constructor for LLVMStmt.

That being said, crucible-llvm doesn't yet do this sort of reasoning, and I don't yet have a pressing need for it—rather, my primary objective is to support recent versions of LLVM. As such, the most expedient fix is to add llvm.experimental.noalias.scope.decl to the list of LLVM intrinsics to skip here. This means that we can avoid needing to translate metadata values into Crucible simulator values, which is nice.

I'm going to pursue the aforementioned expedient fix in an upcoming patch. If we want to support no-alias reasoning at a deeper level in the future, we can implement the LLVM_NoAlias idea.