I'm studying vellvm framework.
How can I verify simple function on C with vellvm?
I know that I can use assertions inside .ll code
; ASSERT EQ: i32 0 = call i32 @foo(i32 0)
but I want more
This is the function I need to verify:
int foo() {
return 3;
}
This is .ll version of my code
; ModuleID = 'return3.c'
source_filename = "return3.c"
target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128"
target triple = "x86_64-pc-linux-gnu"
; Function Attrs: noinline nounwind optnone uwtable
define dso_local i32 @foo() #0 {
ret i32 3
}
attributes #0 = { noinline nounwind optnone uwtable "frame-pointer"="all" "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" }
!llvm.module.flags = !{!0, !1, !2, !3, !4}
!llvm.ident = !{!5}
!0 = !{i32 1, !"wchar_size", i32 4}
!1 = !{i32 7, !"PIC Level", i32 2}
!2 = !{i32 7, !"PIE Level", i32 2}
!3 = !{i32 7, !"uwtable", i32 1}
!4 = !{i32 7, !"frame-pointer", i32 2}
!5 = !{!"Ubuntu clang version 14.0.0-1ubuntu1.1"}
and this is Internal Coq representation of the AST (got it after interpretation by vellvm)
Internal Coq representation of the ast :
(TLE_Source_filename "return3.c")
(TLE_Datalayout "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128")
(TLE_Target "x86_64-pc-linux-gnu")
(TLE_Definition
(mk_definition _
(mk_declaration (Name "foo") (TYPE_Function ((TYPE_I 32)) []false)
([], [])
[(FNATTR_Attr_grp (0)%Z)]
[ANN_preemption_specifier PREEMPTION_Dso_local]
[]
((mk_block (Anon (0)%Z) [] [] (TERM_Ret ((TYPE_I 32), (EXP_Integer (3)%Z))) None), [])
)
)
(TLE_Attribute_group (0)%Z [FNATTR_Noinline; FNATTR_Nounwind; FNATTR_Optnone; FNATTR_UwtableNone;
(FNATTR_Key_value ("frame-pointer", "all"));
(FNATTR_Key_value ("min-legal-vector-width", "0"));
(FNATTR_Key_value ("no-trapping-math", "true"));
(FNATTR_Key_value ("stack-protector-buffer-size", "8"));
(FNATTR_Key_value ("target-cpu", "x86-64"));
(FNATTR_Key_value ("target-features", "+cx8,+fxsr,+mmx,+sse,+sse2,+x87"));
(FNATTR_Key_value ("tune-cpu", "generic"))]
)
(TLE_Metadata
(Name "llvm.module.flags")
(METADATA_Node
[ (METADATA_Id (Anon (0)%Z));
(METADATA_Id (Anon (1)%Z));
(METADATA_Id (Anon (2)%Z));
(METADATA_Id (Anon (3)%Z));
(METADATA_Id (Anon (4)%Z))
]
)
)
(TLE_Metadata
(Name "llvm.ident")
(METADATA_Node [(METADATA_Id (Anon (5)%Z))])
)
(TLE_Metadata
(Anon (0)%Z)
(METADATA_Node
[(METADATA_Const ((TYPE_I 32), (EXP_Integer (1)%Z)));
(METADATA_String "wchar_size");
(METADATA_Const ((TYPE_I 32), (EXP_Integer (4)%Z)))
]
)
)
(TLE_Metadata (Anon (1)%Z) (METADATA_Node [(METADATA_Const ((TYPE_I 32), (EXP_Integer (7)%Z))); (METADATA_String "PIC Level"); (METADATA_Const ((TYPE_I 32), (EXP_Integer (2)%Z)))]))
(TLE_Metadata (Anon (2)%Z) (METADATA_Node [(METADATA_Const ((TYPE_I 32), (EXP_Integer (7)%Z))); (METADATA_String "PIE Level"); (METADATA_Const ((TYPE_I 32), (EXP_Integer (2)%Z)))]))
(TLE_Metadata (Anon (3)%Z) (METADATA_Node [(METADATA_Const ((TYPE_I 32), (EXP_Integer (7)%Z))); (METADATA_String "uwtable"); (METADATA_Const ((TYPE_I 32), (EXP_Integer (1)%Z)))]))
(TLE_Metadata (Anon (4)%Z) (METADATA_Node [(METADATA_Const ((TYPE_I 32), (EXP_Integer (7)%Z))); (METADATA_String "frame-pointer"); (METADATA_Const ((TYPE_I 32), (EXP_Integer (2)%Z)))]))
(TLE_Metadata (Anon (5)%Z) (METADATA_Node [(METADATA_String "Ubuntu clang version 14.0.0-1ubuntu1.1")]))
What can I do with this AST?
I need to prove (using Coq) something about my function, for example that function always returns 3
How this can be achieved?
What options to consider if I need to verify C code using vellvm?
Thank you.
You can definitely prove that your function always returns 3 using Vellvm, for instance there are a few examples of these kinds of proofs here.
These examples compare the itrees from denoting individual blocks of
code in the LLVM semantics using the denote_block
function, but in
theory you could use the interpreter
function instead to interpret an AST into an itree, though you would currently
have to copy the AST manually into a Coq file. The type of the AST
should match up with the interpreter
function, so you will have to
take each of the TLE_*
values from the internal representation and
put them in a list in Coq. One you've interpreted your AST into an itree you can then compare it against a specific itree (e.g., one which just returns 3) using itree relations like eutt.
While you can do this, there currently isn't much of a framework for doing these kinds of proofs in Vellvm. Ideally you would have a program logic that you would use for these proofs. Irene Yoon has done some work on this in the context of Vellvm (https://euisuny.github.io/note/dissertation.pdf), but it is not currently incorporated into the main version of Vellvm. If your goal is to prove things about C programs in particular you may want to check out these projects instead:
Also, in response to this:
I know that I can use assertions inside .ll code ; ASSERT EQ: i32 0 = call i32 @foo(i32 0)
It's worth noting that these assertions are for the test framework using the executable interpreter. They're not relevant for proofs in Coq about LLVM programs.