About the examples of this project

[Jerry-zhxf]

1. I've done the conversion from C code to LLVM IR to CL myself, but some cases have failed. And I find that you can compile only one of these functions when you convert C code to LLVM IR. How do you do that?
   Example:
   curve25519.c -> curve25519_fe51_add.ll
   But I only can get the curve25519.ll by using the command (clang -S -emit-llvm curve25519.c), and get a error "fatal error: 'ec_lcl.h' file not found". So I decide to annotate this line of code, then I can generate a .ll file successfully, but when I translate it, I get a message like "IR file is corrupted or does not exist.".
   So I want to ask you what command do you use to compile only the specified function?

2. I found that you have two .cl files to verify the function, xxx_auto.cl is converted from LLVM IR, and after you add pre- and postcondition to the xxx_auto.cl, it becomes the xxx_tuned.cl. However, after I translate the .ll to .cl by myself, the file does not have the auto suffix. So I wonder if you have changed the suffix by yourself, or does the tool have other support that I do not use?

3. I found some problem in the translation detail.
   C code:

int main() {
    int a = 10, i = 20;
    
    for ( i = 0; i < 10; i++ ) {
        a = a *2;
    }
    return 0;
}

LLVM IR:

; ModuleID = 'test_for.c'
source_filename = "test_for.c"
target datalayout = "e-m:e-i64:64-f80:128-n8:16:32:64-S128"
target triple = "x86_64-unknown-linux-gnu"

; Function Attrs: noinline nounwind optnone uwtable
define dso_local i32 @main() #0 {
  %1 = alloca i32, align 4
  %2 = alloca i32, align 4
  %3 = alloca i32, align 4
  store i32 0, i32* %1, align 4
  store i32 10, i32* %2, align 4
  store i32 20, i32* %3, align 4
  store i32 0, i32* %3, align 4
  br label %4

; <label>:4:                                      ; preds = %10, %0
  %5 = load i32, i32* %3, align 4
  %6 = icmp slt i32 %5, 10
  br i1 %6, label %7, label %13

; <label>:7:                                      ; preds = %4
  %8 = load i32, i32* %2, align 4
  %9 = mul nsw i32 %8, 2
  store i32 %9, i32* %2, align 4
  br label %10

; <label>:10:                                     ; preds = %7
  %11 = load i32, i32* %3, align 4
  %12 = add nsw i32 %11, 1
  store i32 %12, i32* %3, align 4
  br label %4

; <label>:13:                                     ; preds = %4
  ret i32 0
}

attributes #0 = { noinline nounwind optnone uwtable "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "less-precise-fpmad"="false" "no-frame-pointer-elim"="true" "no-frame-pointer-elim-non-leaf" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="false" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" }

!llvm.module.flags = !{!0}
!llvm.ident = !{!1}

!0 = !{i32 1, !"wchar_size", i32 4}
!1 = !{!"clang version 7.0.1 (tags/RELEASE_701/final)"}

Cryptoline:

proc main () =
{
  true
  &&
  true
}



(*   %1 = alloca i32, align 4 *)
(*   %2 = alloca i32, align 4 *)
(*   %3 = alloca i32, align 4 *)
(*   store i32 0, i32* %1, align 4 *)
(*   store i32 10, i32* %2, align 4 *)
(*   store i32 20, i32* %3, align 4 *)
(*   store i32 0, i32* %3, align 4 *)
(*   br label %4 *)


{
  true
  &&
  true
}

The Cryptoline code only translates the first eight line(br label %4) in the LLVM IR. And this truncation occurs in the IR code because of the if judgment or for loop. Therefore, I want to ask you, is the validation code not allowed to contain these keywords? Or I have some problems using the translate command.

If you have free time, please give me some help. I am so interested in this. Thank you very much.

[jiaxiangliu]

Thank you very much for trying our tool! Sorry for this late reply.

1. But I only can get the curve25519.ll by using the command (clang -S -emit-llvm curve25519.c), and get a error "fatal error: 'ec_lcl.h' file not found". So I decide to annotate this line of code, then I can generate a .ll file successfully, but when I translate it, I get a message like "IR file is corrupted or does not exist.".

Annotating the line is not a good idea, since curve25519.c depends on the file ec_lcl.h. You may refer to Makefile to find the correct dependencies required to compile curve25519.c.
Also remember that the LLVM version used for compiling llvm2cryptoline should be the same as the one generating the IR code. Otherwise you may also get "IR file is corrupted or does not exist".

So I want to ask you what command do you use to compile only the specified function?

In fact, as you know, we can only compile a whole file. The .ll files for single functions (e.g. curve25519_fe51_add.ll) are extracted manually from the generated .ll file (curve25519.ll).

2. So I wonder if you have changed the suffix by yourself, or does the tool have other support that I do not use?

The suffixes are added manually by ourselves.

3. The Cryptoline code only translates the first eight line(br label %4) in the LLVM IR. And this truncation occurs in the IR code because of the if judgment or for loop. Therefore, I want to ask you, is the validation code not allowed to contain these keywords? Or I have some problems using the translate command.

Yes, you are right. As stated in our ASE paper (Verifying Arithmetic in Cryptographic C Programs), llvm2cryptoline targets arithmetic functions in cryptographic programs. These functions are normally sequential programs. Sometimes they contain trivial loops which can be unwound. So, yes, llvm2cryptoline currently does not support branching or loops. At the LLVM IR level, precisely speaking, llvm2cryptoline can only translate a single basic block.

Here is some more information that might be helpful. The syntax of the CryptoLine language has changed. The syntax used in examples of this repository is not updated yet. Precisely, the openssl examples use the legacy syntax of CryptoLine, the boringssl/curve25519 examples use the untyped syntax of CryptoLine, and the nss examples use the latest syntax. The dev branch of llvm2cryptoline generates .cl file in the latest syntax. But we have no time to update all the examples yet. To verify the .cl files in deprecated syntax, you can use the CryptoLine version before commit c366621a6ea1407830340fdd9be5df1e250761e5. Option "-legacy" or "-untyped" is needed.