How to make OCaml (or Coq) code from the llvmir code using vellvm framework

Question

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.

Answer 1

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:

• VST: this is a program logic in Coq for C that can be used to verify properties about C programs. If you want to use Coq to do proofs about C programs, this is probably what you want!
• CN: seems like a more automated proof for verifying properties about C programs using SAT solvers.

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.