`crucible-llvm`: Support varargs

[RyanGlScott]

A large number of SV-COMP bechmarks make use of functions defined with varargs in C. In terms of LLVM, supporting varargs would be tantamount to adding overrides for the following three intrinsics:

• void @llvm.va_start(i8* <arglist>), which initializes arglist with the varargs of the calling function.
• void @llvm.va_copy(i8* <destarglist>, i8* <srcarglist>), which copies srcarglist to destarglist.
• void @llvm.va_end(i8* <arglist>), which destroys an arglist that was initialized by @llvm.va_start or @llvm.va_copy.

@llvm.va_start seems like the trickiest one to add, since it requires figuring out information about the calling function somehow.

[robdockins]

Looks like varargs functions are used extensively (and exclusively?) in the Juliet benchmarks.

In addition to the intrinsics mentioned above, we would need to add support for the VaArg instruction as well, which actually extracts an argument from the arglist.

[langston-barrett]

It might be worth noting that Clang doesn't always seem to access va_lists through the va_arg instruction:

https://godbolt.org/z/Wq4Gb7bKa

C

```c // https://www.gnu.org/software/libc/manual/html_node/Variadic-Example.html#Variadic-Example #include #include int add_em_up(int count, ...) { va_list ap; int i, sum; va_start(ap, count); /* Initialize the argument list. */ sum = 0; for (i = 0; i < count; i++) sum += va_arg(ap, int); /* Get the next argument value. */ va_end(ap); /* Clean up. */ return sum; } int main(void) { printf("%d\n", add_em_up(3, 5, 5, 6)); printf("%d\n", add_em_up(10, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10)); typeof(add_em_up) *add_em_up_ptr = add_em_up; printf("%d\n", add_em_up_ptr(4, 1, 2, 3, 4)); return 0; } ```

LLVM code

`-emit-llvm -fno-discard-value-names -g0 -O1` ```llvm %struct.__va_list_tag = type { i32, i32, i8*, i8* } @.str = private unnamed_addr constant [4 x i8] c"%d\0A\00", align 1 define dso_local i32 @add_em_up(i32 %count, ...) local_unnamed_addr #0 { entry: %ap = alloca [1 x %struct.__va_list_tag], align 16 %0 = bitcast [1 x %struct.__va_list_tag]* %ap to i8* call void @llvm.lifetime.start.p0i8(i64 24, i8* nonnull %0) #5 call void @llvm.va_start(i8* nonnull %0) %gp_offset_p = getelementptr inbounds [1 x %struct.__va_list_tag], [1 x %struct.__va_list_tag]* %ap, i64 0, i64 0, i32 0 %overflow_arg_area_p = getelementptr inbounds [1 x %struct.__va_list_tag], [1 x %struct.__va_list_tag]* %ap, i64 0, i64 0, i32 2 %1 = getelementptr inbounds [1 x %struct.__va_list_tag], [1 x %struct.__va_list_tag]* %ap, i64 0, i64 0, i32 3 %reg_save_area = load i8*, i8** %1, align 16 %cmp9 = icmp sgt i32 %count, 0 br i1 %cmp9, label %for.body, label %for.end for.body: ; preds = %entry, %vaarg.end %sum.011 = phi i32 [ %add, %vaarg.end ], [ 0, %entry ] %i.010 = phi i32 [ %inc, %vaarg.end ], [ 0, %entry ] %gp_offset = load i32, i32* %gp_offset_p, align 16 %fits_in_gp = icmp ult i32 %gp_offset, 41 br i1 %fits_in_gp, label %vaarg.in_reg, label %vaarg.in_mem vaarg.in_reg: ; preds = %for.body %2 = sext i32 %gp_offset to i64 %3 = getelementptr i8, i8* %reg_save_area, i64 %2 %4 = add i32 %gp_offset, 8 store i32 %4, i32* %gp_offset_p, align 16 br label %vaarg.end vaarg.in_mem: ; preds = %for.body %overflow_arg_area = load i8*, i8** %overflow_arg_area_p, align 8 %overflow_arg_area.next = getelementptr i8, i8* %overflow_arg_area, i64 8 store i8* %overflow_arg_area.next, i8** %overflow_arg_area_p, align 8 br label %vaarg.end vaarg.end: ; preds = %vaarg.in_mem, %vaarg.in_reg %vaarg.addr.in = phi i8* [ %3, %vaarg.in_reg ], [ %overflow_arg_area, %vaarg.in_mem ] %vaarg.addr = bitcast i8* %vaarg.addr.in to i32* %5 = load i32, i32* %vaarg.addr, align 4 %add = add nsw i32 %5, %sum.011 %inc = add nuw nsw i32 %i.010, 1 %exitcond.not = icmp eq i32 %inc, %count br i1 %exitcond.not, label %for.end, label %for.body, !llvm.loop !3 for.end: ; preds = %vaarg.end, %entry %sum.0.lcssa = phi i32 [ 0, %entry ], [ %add, %vaarg.end ] call void @llvm.va_end(i8* %0) call void @llvm.lifetime.end.p0i8(i64 24, i8* nonnull %0) #5 ret i32 %sum.0.lcssa } declare void @llvm.lifetime.start.p0i8(i64 immarg, i8* nocapture) #1 declare void @llvm.va_start(i8*) #2 declare void @llvm.va_end(i8*) #2 declare void @llvm.lifetime.end.p0i8(i64 immarg, i8* nocapture) #1 define dso_local i32 @main() local_unnamed_addr #3 { entry: %call = call i32 (i32, ...) @add_em_up(i32 3, i32 5, i32 5, i32 6) %call1 = call i32 (i8*, ...) @printf(i8* nonnull dereferenceable(1) getelementptr inbounds ([4 x i8], [4 x i8]* @.str, i64 0, i64 0), i32 %call) %call2 = call i32 (i32, ...) @add_em_up(i32 10, i32 1, i32 2, i32 3, i32 4, i32 5, i32 6, i32 7, i32 8, i32 9, i32 10) %call3 = call i32 (i8*, ...) @printf(i8* nonnull dereferenceable(1) getelementptr inbounds ([4 x i8], [4 x i8]* @.str, i64 0, i64 0), i32 %call2) %call4 = call i32 (i32, ...) @add_em_up(i32 4, i32 1, i32 2, i32 3, i32 4) %call5 = call i32 (i8*, ...) @printf(i8* nonnull dereferenceable(1) getelementptr inbounds ([4 x i8], [4 x i8]* @.str, i64 0, i64 0), i32 %call4) ret i32 0 } declare dso_local noundef i32 @printf(i8* nocapture noundef readonly, ...) local_unnamed_addr #4 attributes #0 = { nofree nosync nounwind uwtable "frame-pointer"="none" "min-legal-vector-width"="0" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" } attributes #1 = { argmemonly mustprogress nofree nosync nounwind willreturn } attributes #2 = { mustprogress nofree nosync nounwind willreturn } attributes #3 = { nofree nounwind uwtable "frame-pointer"="none" "min-legal-vector-width"="0" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" } attributes #4 = { nofree nounwind "frame-pointer"="none" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" } attributes #5 = { nounwind } ```

EDIT: In case anyone is curious about what's in that struct, this blog post discusses it. The post contains some outdated information about how LLVM handles va_arg though. https://blog.nelhage.com/2010/10/amd64-and-va_arg/

[robdockins]

Oh, great. Looks like we'll have to reverse-engineer a bunch of ABI details to do this correctly.

[langston-barrett]

In fact, I just double-checked on a bunch of open-source programs and it seems that at least some versions of Clang on some platforms never use va_arg.

Script

```bash #!/usr/bin/env bash declare -a bcs=( nano/nano.bc nano/bin/nano.bc gawk/gawk.bc git/git-shell.bc git/git.bc git/libexec/git-core/git-http-backend.bc git/bin/git.bc file/file.bc bash/bash.bc bash/bin/bash.bc patch/patch.bc tmux/tmux.bc openssh/ssh-add.bc openssh/ssh-keygen.bc openssh/ssh.bc openssh/ssh-keyscan.bc openssh/scp.bc openssh/ssh-agent.bc openssh/sshd.bc openssh/sftp.bc ) for f in "${bcs[@]}"; do cp ~/code/nixpkgs-blight/out/bitcode/$f . llvm-dis $(basename $f) done for f in "${bcs[@]}"; do ll=$(basename ${f%.bc}.ll) start=$(grep --count "@llvm\.va_start" $ll) end=$(grep --count "@llvm\.va_start" $ll) arg=$(grep --count "va_arg" $ll) printf "\n\n$ll:" printf "\n- start: $start" printf "\n- end: $end" printf "\n- arg: $arg" done ```

I wonder if this is related to this note in the documentation:

Note that the code generator does not yet fully support va_arg on many targets.