About CNF DIMACS

[douglas schroeder]

Hello.
So, I am analysing the DIMACS output.
When I try to output the CNF of a small function like:
char foo(char a){
     return a;
}

I got no output.
I made this, because I was wondering what are the variables that have not relation with the C program variables.
for example:
p cnf 915 2536
1 3 0
2 3 0
1 2 3 0
1 5 0
2 5 0
4 5 0
1 2 4 5 0
1 7 0

I know that these first variables (1,2,3,4,5...) are not directly linked to the C program. Where they come from, and
what is their purpose?
Thanks everyone.

[Martin Brain]

On Thu, 2014-09-18 at 11:25 -0700, douglas schroeder wrote:
> Hello.
> So, I am analysing the DIMACS output.
> When I try to output the CNF of a small function like:
> char foo(char a){
> return a;
> }
>
> I got no output.

CBMC generates the CNF of the SAT encoding of the verification
conditions. If there are no verification conditions, i.e. there is
nothing you are trying to prove, then no CNF will be generated.

> I made this, because I was wondering what are the variables that have
> not relation with the C program variables.
> for example:
> p cnf 915 2536
> 1 3 0
> 2 3 0
> 1 2 3 0
> 1 5 0
> 2 5 0
> 4 5 0
> 1 2 4 5 0
> 1 7 0
>
> I know that these first variables (1,2,3,4,5...) are not directly
> linked to the C program. Where they come from, and
> what is their purpose?

There are various other variables that encode global variables and our
models of process state including threads, heap, etc. There will also
be variables used to reason about flow of control. Using --show-vcc
might give you some idea of what is being encoded. --slice-formula will
remove things that can be trivially shown to not influence the
verification conditions that are being proven.

One word of caution -- the DIMACS output is not intended to be human
readable and the comments that link variables in the CNF and the program
are mainly for debugging. What are you aiming to do? There may well be
a better way of doing it.

Cheers,
- Martin

[douglas schroeder]

Thanks Martin.
Now I have another question.
I observed that when I have a conditional jump. (if then else) there apears in the comments something like this:
c 1 goto_symex::\guard#1
What means that *1* in the beginning.
Or better, what this means in the context of the verification.
Is that *1* related to the dimacs encoded variable *1*?
Thanks

[Michael Tautschnig]

Hello,

Yes, 1 will be the dimacs encoding of the single Boolean variable that
goto_symex::\guard#1 gives rise to.

Best,
Michael

[douglas schroeder]

Thanks Michael.
Another question.
When I have a very little program like

void foo(char a){
   a = 'a';
}

I know that no CNF is generated because there are no VCCs.
But Is there a point in the CBMC source that I could print out the CNF?
I'm debugging the source code.
Thank you

[Daniel Kroening]

Hello,

with CBMC trunk you can generate CNF for this with the command-line

cbmc foo.c --dimacs --program-only --function foo

With best regards,

Daniel

[douglas schroeder]

Em quinta-feira, 16 de outubro de 2014 15h14min54s UTC-3, Daniel Kroening escreveu:

Hello,

with CBMC trunk you can generate CNF for this with the command-line

cbmc foo.c --dimacs --program-only --function foo

With best regards,

Daniel

Thank you Daniel.

I have another question.
I made the following program to verify with the options --dimacs and --outfile
void foo(char a, char b){
   char result;
   result = a+b;
   assert(result);
}

It generates a full adder in Tseitin encoding, right?
But at the end of the file it appends the folowing constraints that I do not understand.
Could you explain it?

-50 -52 -54 0
50 52 -54 0
-50 52 54 0
50 -52 54 0
-51 -53 -55 0
51 53 -55 0
-51 53 55 0
51 -53 55 0
-54 -56 0
-55 -56 0
54 55 56 0
-1 56 0
1 -56 0

Thanks

[Michael Tautschnig]

Hello,

On Mon, Oct 27, 2014 at 13:40:23 -0700, douglas schroeder wrote:
[...]

> I have another question.
> I made the following program to verify with the options --dimacs and
> --outfile
> void foo(char a, char b){
> char result;
> result = a+b;
> assert(result);
> }
>
> It generates a full adder in Tseitin encoding, right?

Yes.

> But at the end of the file it appends the folowing constraints that I do
> not understand.
> Could you explain it?
>
> -50 -52 -54 0
> 50 52 -54 0
> -50 52 54 0
> 50 -52 54 0
> -51 -53 -55 0
> 51 53 -55 0
> -51 53 55 0
> 51 -53 55 0
> -54 -56 0
> -55 -56 0
> 54 55 56 0
> -1 56 0
> 1 -56 0
>

If you look at the output of cbmc --function foo --program-only, you will find
the constraint

__CPROVER_threads_exited#1 == ARRAY_OF(FALSE)

among all the others. This (here: unused) constraint requires additional array
equality constraints, which are encoded after all the program constraints. And
that is precisely what is being encoded here.

Best,
Michael