Welcome to seahorn Discussions!

[agurfinkel]

👋 Welcome!

We’re using Discussions as a place to connect with other members of our community. We hope that you:

• Ask questions you’re wondering about.
• Share ideas.
• Engage with other community members.
• Welcome others and are open-minded. Remember that this is a community we
  build together 💪.

To get started, comment below with an introduction of yourself and tell us about what you do with this community.

[Luweicai]

Hello.
I wonder about how to add annotations to llvm ir files directly. As that some works based on the llvm ir levels. I try by compiling c files with and without annotations to observe the difference. Sometimes the difference between them is not trivial. I wonder how to add them precisely and correctly. (It will be quite good if some documents exist to explian the translation of annotations between c/c++ files and llvm ir files).

[agurfinkel]

What precisely do you mean by annotations?

If you want to modify LLVM IR files directly, LLVM itself provides good support for manipulating IR files.
I have also had good experience using llvmlite: https://github.com/numba/llvmlite

[Luweicai]

Hi, agurfinkel. Thank for your respond.
"Annotations" are the instructions like "sassert(expression)" and "assume(expression)" supported by seahorn. I want to set the assert and assume in the IR files directly.

[caballa]

Look at https://github.com/seahorn/seahorn/blob/dev10/lib/Transforms/Instrumentation/SimpleMemoryCheck.cc for an example.
This is a LLVM instrumentation pass that adds assertions and assumes. For assertions, instead of sassert(c) the instrumentation adds if (!c) verifier.error() where verifier.error is a special function that SeaHorn understands.

[Luweicai]

Thanks!

[Luweicai]

Hello,
I come accross a problem: I want to use some structure more complex than interger(for example array) to be non-deterministically input for verification. Here is a c demo :

#include "seahorn/seahorn.h"
#include "stdio.h"
struct st{
int a[16];
};
extern struct st getst();
extern int getint();
int main(){
struct st demo = getst();
int a = demo.a[14];
printf("%d\n",a);
a = a - 10;
sassert(a != 0);
return 0;
}

Then I verify it with:
sea pf -m64 xx.c --cex=xx.ll
sea exe -m64 xx.c xx.ll -o xx.exe
./xx.exe

It shows sat but the result shows in screen is 0. However if I get a from getint(), it works well and the result is 10. I wonder what is the problem and how can I get the non-deterministically input correctly.

[agurfinkel]

Your program has undefined behavior -- read from uninitialized variable. This is not what you want.

There isn't a good way to non-deterministically set many memory locations.

One trick to at least hide this from the compiler is to create an external function like memset and use it to initialize the array. Since seahorn will not know the body of this function it will consider the array uninitialized.

This is a bit of a hack, so it may behave strangely.

[Luweicai]

Thanks for your reply!
I am a little bit confuesed because seahorn says that if I set a variable of type ty with return value of an external function with return type ty, just like:

external ty getvalue(); // declaration of an external function. 
...
int main(){
     ty var = getvalue(); 
     puts(var);
     ...     
     sassert(some_constrain(var));
}

Then the generated cex files will give a value to the var.

sea exe-cex xxx.c -o xxx.exe
./xxx.exe

Then I get a value of var as a counter example I want. It works well when the ty is int. Why it does not work if ty is a struct(with a array as it's menber).

[agurfinkel]

Sorry, I misunderstood your example. You are right to expect this to work. But it does not. I believe our executable counterexample generation is limited to scalars in this mode.

BTW: are you interested in invariants or precise bit-reasoning and counterexamples? Our BMC engine might have a better support for counterexamples.

[caballa]

Yes, I tried the example and it doesn't reproduce correctly the cex. We do have a very limited support for memory if option --alloc-mem is enabled but it doesn't seem enough for this example.

[nano-o]

Hello, I'm seemingly having a similar problem. I tried seahorn on a small C program inspired by a smart contract: https://github.com/nano-o/racket-soroban-pool-model/blob/b22631481caecda86213ee26e1140f7092b53d46/seahorn-test/amm.c
sea pf --cex=cex.bc amm.c says sat, but when I link withcex.bc and run the program, no assert fails.
Is there a way to make this work?
I'm using the seahorn-llvm10:nightly docker image.

[nano-o]

It looks like my expectations were a bit unrealistic, as even this simple test exhibits the behavior:

#include "seahorn/seahorn.h"
extern int nd();
int main(void) {
    int x = nd();
    assume (x > 0 && x <= 1);
    x = x*x;
    sassert (x > 0);
}

I presume seahorn does not support non-linear arithmetic and considers the result of the multiplication arbitrary. Is that the case?

[caballa]

The command sea pf will translate the program to Constrained Horn Clauses (CHC) and it will infer automatically safe inductive invariants. Because of that, solving CHC is limited mostly to arrays and linear arithmetic. If you care about non-linear arithmetic then use the Bounded Model-Checking engine by using the command sea bpf

[caballa]

https://github.com/seahorn/seahorn/blob/dev14/test/cex/cex_nonlinear_arith.c

[agurfinkel]

@nano-o your examples are better suited to our BMC engine (command bpf). BMC engine is bit-precise, and, therefore, can handle non-linear arithmetic. We do not target non-linear arithmetic specifically, so I would expect SeaHorn to not scale too well in these cases.

The best way to see how to use BMC engine is to look at our repo https://github.com/seahorn/verify-c-common
Specifically, the options we typically used are captured in this config file: https://github.com/seahorn/verify-c-common/blob/master/seahorn/sea_base.yaml

You can use these options with the following command

sea yama -y URL_OR_PATH_TO_OPTIONS bpf INPUT.c

[nano-o]

Thanks! That works much better.

[KennethAdamMiller]

If I wanted to parse the output invariant using a library that supports that, how would I do it? I badly need to import the invariants to a separate tool from seahorn, or else I can't use them. Furthermore, I'm having a lot of difficulty interpreting what gets printed.