get SAT or SMT using cbmc

[Jimmy Cai]

Hello, 

   

    Is there any way I can get the SAT ot SMT of a program using CBMC?

    It seems that the options --smt1, --smt2 is what I want, but when I add this option, the result is just the same as I didn't add the option. 

     

    This is the way I use it:

   

           cbmc --smt1 filea.c

    So, is my way using the option wrong? and how can I get the SMT or SAT of a program?

Thanks!

[Ruben Martins]

Dear Jimmy,

If you want to output subgoals in SMT1, SMT2, or CNF format you should use the option --outfile filename.

This option will write the subgoals to the file 'filename' with the specified format.

For example, for outputting the subgoals in CNF format use the following command:

./cbmc --dimacs --outfile filename filea.c

Best regards,

Ruben Martins

[Martin Brain]

On Tue, 2014-07-08 at 03:59 -0700, Jimmy Cai wrote:
> Hello,
>
> Is there any way I can get the SAT ot SMT of a program using CBMC?

What do you mean by the "SAT or SMT of a program"? CBMC can give you a
SAT or SMT formula for a fixed depth or number of unwindings with
functions inlined. There are a number of other ways of producing a
formula that over or under approximates a program, for example
k-induction. There are other tools in the CProver framework that can
supply some of these.

Also, depending what you want to do, extracting the formula and working
with it outside the tools may not be the best way. What do you want to
do with the formula?

> It seems that the options --smt1, --smt2 is what I want, but when I add
> this option, the result is just the same as I didn't add the option.

Exactly the same? --smt1 and --smt2 change the decision procedure to
use an SMT1 or SMT2 solver and this should be reflected in the output of
the tool.

> This is the way I use it:
>
> cbmc --smt1 filea.c
>
> So, is my way using the option wrong? and how can I get the SMT or SAT
> of a program?

The --outfile option outputs the SAT or SMT formula to a file rather
than calling a solver.

Cheers,
- Martin

[Daniel Kroening]

Hello,

you can use the option

--outfile file-name

to write the formula generated into a file. This works for SMT1 and SMT2. For propositional SAT, use --dimacs.

This will give you the verification conditions, i.e., the formula will be with respect to assertions in the program.

To get just the program with a particular unwinding, use the option --program-only. The formula you then get will have a satisfying assignment for every execution of the program.

With best regards,

Daniel

On Tuesday, July 8, 2014 11:59:32 AM UTC+1, Jimmy Cai wrote:

[Jimmy Cai]

Dear Ruben,

Thanks for your reply, I try the command, and it works well.

[Jimmy Cai]

Hello,

Thanks for your reply first,

yes, I got the CNF with options --program-only  --dimacs --outfile .

Can I get the CNF of program that didn't translate to bit vector, for example, what I want to get is like this:

and see how the program translate to CNF of bit vector equation.

[Jimmy Cai]

On Tuesday, July 8, 2014 9:20:59 PM UTC+8, martin...@cs.ox.ac.uk wrote:

On Tue, 2014-07-08 at 03:59 -0700, Jimmy Cai wrote:
> Hello,
>    
>     Is there any way I can get the SAT ot SMT of a program using CBMC?

What do you mean by the "SAT or SMT of a program"?  CBMC can give you a
SAT or SMT formula for a fixed depth or number of unwindings with
functions inlined.  There are a number of other ways of producing a
formula that over or under approximates a program, for example
k-induction.  There are other tools in the CProver framework that can
supply some of these.

Also, depending what you want to do, extracting the formula and working
with it outside the tools may not be the best way.  What do you want to
do with the formula?

Actually, I want to learn how the translated program(like below image) is translated to a CNF format of bit vector.

And is there any way I can get the translated program(like the image)?

>     It seems that the options --smt1, --smt2 is what I want, but when I add
> this option, the result is just the same as I didn't add the option.

Exactly the same?  --smt1 and --smt2 change the decision procedure to
use an SMT1 or SMT2 solver and this should be reflected in the output of
the tool.

I think The reason why my result is the same is: 0 VCC, and when I add --program-only, it output the subgoals in CNF formats

[Daniel Kroening]

Hello,

this is covered in chapter 6 of the Decision Procedures book. You could look at the slides that come with it:

http://www.decision-procedures.org/slides/bit-vectors.pdf

Daniel

[Jimmy Cai]

Hello,

Thanks very much, it helps me a lot.

Jimmy

[Dio de Niz]

Hi, I am trying to use this command to get the CNF to experiment with some model counters but if my program does not have any assetion it does not produce a CNF. Am I missing something?

[Daniel Kroening]

Hello,

are you quite sure you gave the options --program-only and --dimacs?

This will produce CNF even if there are no assertions at all.

Daniel

[Sebastian]

Hi,

I'm also trying to use CBMC 4.5 on Ubuntu 14.04, to get the CNF with:

$ cbmc --unwind 5 --program-only --dimacs --outfile bphash-progam-only.cnf bphash-assert.c

It does not generate any output file. It only prints the text given below, on stdout. I must be doing something wrong. Can someone please help me get a CNF file with the --proram-only option?

Thanks,

Sebastian

file bphash-assert.c: Parsing

Converting

Type-checking bphash-assert

Generating GOTO Program

Adding CPROVER library

Function Pointer Removal

Partial Inlining

Generic Property Instrumentation

Starting Bounded Model Checking

Unwinding loop c::main.0 iteration 1 file bphash-assert.c line 22 function main thread 0

Unwinding loop c::main.0 iteration 2 file bphash-assert.c line 22 function main thread 0

Unwinding loop c::main.0 iteration 3 file bphash-assert.c line 22 function main thread 0

Unwinding loop c::main.0 iteration 4 file bphash-assert.c line 22 function main thread 0

Unwinding loop c::main.0 iteration 5 file bphash-assert.c line 22 function main thread 0

Unwinding loop c::BPHash.0 iteration 1 file bphash-assert.c line 10 function BPHash thread 0

Unwinding loop c::BPHash.0 iteration 2 file bphash-assert.c line 10 function BPHash thread 0

Unwinding loop c::BPHash.0 iteration 3 file bphash-assert.c line 10 function BPHash thread 0

Unwinding loop c::BPHash.0 iteration 4 file bphash-assert.c line 10 function BPHash thread 0

Unwinding loop c::BPHash.0 iteration 5 file bphash-assert.c line 10 function BPHash thread 0

size of program expression: 135 steps

simple slicing removed 6 assignments

Program constraints:

(1) __CPROVER_threads_exited#1 == ARRAY_OF(FALSE)

(2) __CPROVER_next_thread_id#1 == 0ul

(3) __CPROVER_deallocated#1 == NULL

(4) __CPROVER_malloc_object#1 == NULL

(5) __CPROVER_malloc_size#1 == 0ul

(6) __CPROVER_malloc_is_new_array#1 == FALSE

(7) __CPROVER_pipe_count#1 == 0u

(8) __CPROVER_rounding_mode!0#1 == 0

(9) argv'#1 == argv'#0 WITH [argc'#0:=((char *)NULL)]

(10) argc!0@1#1 == argc'#0

(11) argv!0@1#1 == argv'

(12) str!0@1#2 == (unsigned char *)argv'#1[1l]

(13) s!0@1#2 == (const char *)str!0@1#2

(14) len!0@1#2 == 0ul

(15) \guard#1 == !((signed int)invalid_object0#0 == 0)

(16) len!0@1#3 == 1ul

     guard: \guard#1

(17) \guard#2 == !((signed int)invalid_object1#0 == 0)

(18) len!0@1#4 == 2ul

     guard: \guard#1 && \guard#2

(19) \guard#3 == !((signed int)invalid_object2#0 == 0)

(20) len!0@1#5 == 3ul

     guard: \guard#1 && \guard#2 && \guard#3

(21) \guard#4 == !((signed int)invalid_object3#0 == 0)

(22) len!0@1#6 == 4ul

     guard: \guard#1 && \guard#2 && \guard#3 && \guard#4

(23) \guard#5 == !((signed int)invalid_object4#0 == 0)

(24) len!0@1#7 == 5ul

     guard: \guard#1 && \guard#2 && \guard#3 && \guard#4 && \guard#5

(25) ASSERT(!(\guard#1 && \guard#2 && \guard#3 && \guard#4 && \guard#5)) 

     guard: \guard#1 && \guard#2 && \guard#3 && \guard#4 && \guard#5

(26) len!0@1#8 == 4ul

(27) len!0@1#9 == (!\guard#4 ? 3ul : 4ul)

(28) len!0@1#10 == (!\guard#3 ? 2ul : len!0@1#9)

(29) len!0@1#11 == (!\guard#2 ? 1ul : len!0@1#10)

(30) len!0@1#12 == (!\guard#1 ? 0ul : len!0@1#11)

(31) return_value_strlen$1!0@1#2 == len!0@1#12

     guard: \guard#1 && (\guard#2 && (\guard#3 && (\guard#4 && !\guard#5 || !\guard#4) || !\guard#3) || !\guard#2) || !\guard#1

(32) len!0@1#14 == len!0@1#12

(33) str!0@1#1 == (char *)str!0@1#2

     guard: \guard#1 && (\guard#2 && (\guard#3 && (\guard#4 && !\guard#5 || !\guard#4) || !\guard#3) || !\guard#2) || !\guard#1

(34) len!0@1#1 == (unsigned int)return_value_strlen$1!0@1#2

     guard: \guard#1 && (\guard#2 && (\guard#3 && (\guard#4 && !\guard#5 || !\guard#4) || !\guard#3) || !\guard#2) || !\guard#1

(35) hash!0@1#2 == 0u

     guard: \guard#1 && (\guard#2 && (\guard#3 && (\guard#4 && !\guard#5 || !\guard#4) || !\guard#3) || !\guard#2) || !\guard#1

(36) i!0@1#2 == 0u

     guard: \guard#1 && (\guard#2 && (\guard#3 && (\guard#4 && !\guard#5 || !\guard#4) || !\guard#3) || !\guard#2) || !\guard#1

(37) i!0@1#3 == 0u

     guard: \guard#1 && (\guard#2 && (\guard#3 && (\guard#4 && !\guard#5 || !\guard#4) || !\guard#3) || !\guard#2) || !\guard#1

(38) \guard#6 == len!0@1#1 > 0u

(39) hash!0@1#3 == (unsigned int)str$object#0

     guard: (\guard#1 && (\guard#2 && (\guard#3 && (\guard#4 && !\guard#5 || !\guard#4) || !\guard#3) || !\guard#2) || !\guard#1) && \guard#6

(40) str!0@1#2 == 1l + str!0@1#1

     guard: (\guard#1 && (\guard#2 && (\guard#3 && (\guard#4 && !\guard#5 || !\guard#4) || !\guard#3) || !\guard#2) || !\guard#1) && \guard#6

(41) i!0@1#4 == 1u

     guard: (\guard#1 && (\guard#2 && (\guard#3 && (\guard#4 && !\guard#5 || !\guard#4) || !\guard#3) || !\guard#2) || !\guard#1) && \guard#6

(42) \guard#7 == len!0@1#1 > 1u

(43) hash!0@1#4 == (hash!0@1#3 << 7 ^ (unsigned int)str$object#0)

     guard: (\guard#1 && (\guard#2 && (\guard#3 && (\guard#4 && !\guard#5 || !\guard#4) || !\guard#3) || !\guard#2) || !\guard#1) && \guard#6 && \guard#7

(44) str!0@1#3 == 1l + str!0@1#2

     guard: (\guard#1 && (\guard#2 && (\guard#3 && (\guard#4 && !\guard#5 || !\guard#4) || !\guard#3) || !\guard#2) || !\guard#1) && \guard#6 && \guard#7

(45) i!0@1#5 == 2u

     guard: (\guard#1 && (\guard#2 && (\guard#3 && (\guard#4 && !\guard#5 || !\guard#4) || !\guard#3) || !\guard#2) || !\guard#1) && \guard#6 && \guard#7

(46) \guard#8 == len!0@1#1 > 2u

(47) hash!0@1#5 == (hash!0@1#4 << 7 ^ (unsigned int)str$object#0)

     guard: (\guard#1 && (\guard#2 && (\guard#3 && (\guard#4 && !\guard#5 || !\guard#4) || !\guard#3) || !\guard#2) || !\guard#1) && \guard#6 && \guard#7 && \guard#8

(48) str!0@1#4 == 1l + str!0@1#3

     guard: (\guard#1 && (\guard#2 && (\guard#3 && (\guard#4 && !\guard#5 || !\guard#4) || !\guard#3) || !\guard#2) || !\guard#1) && \guard#6 && \guard#7 && \guard#8

(49) i!0@1#6 == 3u

     guard: (\guard#1 && (\guard#2 && (\guard#3 && (\guard#4 && !\guard#5 || !\guard#4) || !\guard#3) || !\guard#2) || !\guard#1) && \guard#6 && \guard#7 && \guard#8

(50) \guard#9 == len!0@1#1 > 3u

(51) hash!0@1#6 == (hash!0@1#5 << 7 ^ (unsigned int)str$object#0)

     guard: (\guard#1 && (\guard#2 && (\guard#3 && (\guard#4 && !\guard#5 || !\guard#4) || !\guard#3) || !\guard#2) || !\guard#1) && \guard#6 && \guard#7 && \guard#8 && \guard#9

(52) str!0@1#5 == 1l + str!0@1#4

     guard: (\guard#1 && (\guard#2 && (\guard#3 && (\guard#4 && !\guard#5 || !\guard#4) || !\guard#3) || !\guard#2) || !\guard#1) && \guard#6 && \guard#7 && \guard#8 && \guard#9

(53) i!0@1#7 == 4u

     guard: (\guard#1 && (\guard#2 && (\guard#3 && (\guard#4 && !\guard#5 || !\guard#4) || !\guard#3) || !\guard#2) || !\guard#1) && \guard#6 && \guard#7 && \guard#8 && \guard#9

(54) \guard#10 == len!0@1#1 > 4u

(55) hash!0@1#7 == (hash!0@1#6 << 7 ^ (unsigned int)str$object#0)

     guard: (\guard#1 && (\guard#2 && (\guard#3 && (\guard#4 && !\guard#5 || !\guard#4) || !\guard#3) || !\guard#2) || !\guard#1) && \guard#6 && \guard#7 && \guard#8 && \guard#9 && \guard#10

(56) str!0@1#6 == 1l + str!0@1#5

     guard: (\guard#1 && (\guard#2 && (\guard#3 && (\guard#4 && !\guard#5 || !\guard#4) || !\guard#3) || !\guard#2) || !\guard#1) && \guard#6 && \guard#7 && \guard#8 && \guard#9 && \guard#10

(57) i!0@1#8 == 5u

     guard: (\guard#1 && (\guard#2 && (\guard#3 && (\guard#4 && !\guard#5 || !\guard#4) || !\guard#3) || !\guard#2) || !\guard#1) && \guard#6 && \guard#7 && \guard#8 && \guard#9 && \guard#10

(58) ASSERT(!((\guard#1 && (\guard#2 && (\guard#3 && (\guard#4 && !\guard#5 || !\guard#4) || !\guard#3) || !\guard#2) || !\guard#1) && \guard#6 && \guard#7 && \guard#8 && \guard#9 && \guard#10)) 

     guard: (\guard#1 && (\guard#2 && (\guard#3 && (\guard#4 && !\guard#5 || !\guard#4) || !\guard#3) || !\guard#2) || !\guard#1) && \guard#6 && \guard#7 && \guard#8 && \guard#9 && \guard#10

(59) str!0@1#7 == str!0@1#5

(60) hash!0@1#8 == hash!0@1#6

(61) i!0@1#9 == 4u

(62) str!0@1#8 == (!\guard#9 ? str!0@1#4 : str!0@1#7)

(63) hash!0@1#9 == (!\guard#9 ? hash!0@1#5 : hash!0@1#8)

(64) i!0@1#10 == (!\guard#9 ? 3u : 4u)

(65) str!0@1#9 == (!\guard#8 ? str!0@1#3 : str!0@1#8)

(66) hash!0@1#10 == (!\guard#8 ? hash!0@1#4 : hash!0@1#9)

(67) i!0@1#11 == (!\guard#8 ? 2u : i!0@1#10)

(68) str!0@1#10 == (!\guard#7 ? str!0@1#2 : str!0@1#9)

(69) hash!0@1#11 == (!\guard#7 ? hash!0@1#3 : hash!0@1#10)

(70) i!0@1#12 == (!\guard#7 ? 1u : i!0@1#11)

(71) str!0@1#11 == (!\guard#6 ? str!0@1#1 : str!0@1#10)

(72) hash!0@1#12 == (!\guard#6 ? 0u : hash!0@1#11)

(73) i!0@1#13 == (!\guard#6 ? 0u : i!0@1#12)

(74) hash!0@1#2 == hash!0@1#12

     guard: (\guard#1 && (\guard#2 && (\guard#3 && (\guard#4 && !\guard#5 || !\guard#4) || !\guard#3) || !\guard#2) || !\guard#1) && (\guard#6 && (\guard#7 && (\guard#8 && (\guard#9 && !\guard#10 || !\guard#9) || !\guard#8) || !\guard#7) || !\guard#6)

(75) hash!0@1#14 == hash!0@1#12

(76) i!0@1#15 == i!0@1#13

(77) \guard#11 == (hash!0@1#2 == 1543172857u)

(78) ASSERT(!((\guard#1 && (\guard#2 && (\guard#3 && (\guard#4 && !\guard#5 || !\guard#4) || !\guard#3) || !\guard#2) || !\guard#1) && (\guard#6 && (\guard#7 && (\guard#8 && (\guard#9 && !\guard#10 || !\guard#9) || !\guard#8) || !\guard#7) || !\guard#6) && !\guard#11)) 

     guard: (\guard#1 && (\guard#2 && (\guard#3 && (\guard#4 && !\guard#5 || !\guard#4) || !\guard#3) || !\guard#2) || !\guard#1) && (\guard#6 && (\guard#7 && (\guard#8 && (\guard#9 && !\guard#10 || !\guard#9) || !\guard#8) || !\guard#7) || !\guard#6) && !\guard#11

(79) str!0@1#4 == str!0@1#2

(80) hash!0@1#4 == hash!0@1#2

(81) return_value_strlen$1!0@1#4 == return_value_strlen$1!0@1#2

PS: Source code of the C program I used is attached.

[Martin Brain]

On Tue, 2016-10-04 at 06:34 -0700, Sebastian wrote:
> Hi,
>
> I'm also trying to use CBMC 4.5 on Ubuntu 14.04, to get the CNF with:
>
> $ cbmc --unwind 5 --program-only --dimacs --outfile bphash-progam-only.cnf
> bphash-assert.c
>
> It does not generate any output file. It only prints the text given below,
> on stdout. I must be doing something wrong. Can someone please help me get
> a CNF file with the --proram-only option?

CBMC 4.5 is pretty old now. Can you try again with the latest version,
5.5:

http://www.cprover.org/cbmc/

or build from the mainline:

http://www.github.com/diffblue/cbmc/

Cheers,
- Martin