What to do when SAT solver runs out of memory

[Dinesh Kumar]

Dear all, 

I am using CBMC 5.12 and I am getting the following error. ("SAT runs out of memory")

Any idea about how we can increase the memory required for the SAT solver? 

Thanks in advance.

Regards,

Dinesh

[Martin Nyx Brain]

On Tue, 2021-07-27 at 20:54 -0700, Dinesh Kumar wrote:
> Dear all,
>
> I am using CBMC 5.12 and I am getting the following error. ("SAT runs
> out
> of memory")
> Any idea about how we can increase the memory required for the SAT
> solver?
> Thanks in advance.

Hi Dinesh,

Without knowing anything about the code or what you are trying to prove
it is a little hard to say but some general things that might work:

A. Increase the capability of the solver to handle things
- Compile with one of the more modern SAT solvers, CaDiCaL or RiSS
would be good choices.
- Try using an SMT solver, Boolector/Bitwuzla, cvc4/cvc5 or z3 would be
good choices.

B. Reduce the size of the formula
- --slice-formula is almost always worth using

C. Analyze a smaller area of code
- Use --unwind or --depth to limit the amount of code that is examined
- Write test harnesses to verify parts of code at a time.
- Use the contracts support to abstract away some functions.

HTH

Cheers,
- Martin

[Dinesh Kumar]

Thank you Martin. 

I will try out point A as mentioned by you.

The code is not share-able here. apologies. 

I am trying to check the robustness properties like  --bounds-check ,  --pointer-check ,  --memory-leak-check ,  --div-by-zero-check  ,  --signed-overflow-check ,  --unsigned-overflow-check ,  --pointer-overflow-check ,  --conversion-check ,  --undefined-shift-check ,  --float-overflow-check ,  --nan-check. 

I am using -unwind option and slicing ( --slice-formula --partial-loops --unwind 25 )

Could you give some hint about this "Use the contracts support to abstract away some functions." ?

Thank you in advance.

Regards,

Dinesh

[Martin Nyx Brain]

On Wed, 2021-07-28 at 04:10 -0700, Dinesh Kumar wrote:
> Thank you Martin.
> I will try out point A as mentioned by you.
>
> The code is not share-able here. apologies.
>
> I am trying to check the robustness properties like --bounds-check
> ,
> --pointer-check , --memory-leak-check , --div-by-zero-check ,
> --signed-overflow-check , --unsigned-overflow-check ,
> --pointer-overflow-check , --conversion-check , --undefined-shift-
> check
> , --float-overflow-check , --nan-check.
>
> I am using -unwind option and slicing ( --slice-formula --partial-
> loops
> --unwind 25 )

I would try starting at --unwind 1 and then working upwards and see
what point you run into memory limits.

It is also worth using CBMC on a 64 bit processor if possible. Ideally
with as much RAM as you can get (I would avoid using swap for CBMC; it
likely won't help performance). You might also want to try a more
modern release than 5.12.

> Could you give some hint about this "Use the contracts support to
> abstract
> away some functions." ?

https://github.com/diffblue/cbmc/blob/develop/doc/cprover-manual/contracts.md

is the documentation for function contracts but without knowing
anything about your code it is very hard for me to say if that is
appropriate or how they can be best used.

Cheers,
- Martin

[Dinesh Kumar]

Thank you Martin,

Even unwind 1 or 2 brings me the same "SAT ran out of memory". It stays at the "Converting to Single Static Assignment" step for more than 15 minutes before erroring out as "SAT ran out of memory". I suspect the volume of C files that we feed to CBMC could be the issue. May be I should verify parts of the code first instead of verifying the integrated code. 

Yes my machine is x64 based i7 processor with 32GB RAM. I will try with a more recent version of CBMC as you suggested and get back.

My code would look similar to some code generated from tools like Matlab/Simulink with lot of structs, pointers (you can assume 30 c files like the below image)

Function contracts could be useful for us. Thank you for sharing the details. 

Regards,

Dinesh

[Martin Nyx Brain]

On Wed, 2021-07-28 at 20:58 -0700, Dinesh Kumar wrote:
> Thank you Martin,
>
> Even unwind 1 or 2 brings me the same "SAT ran out of memory". It
> stays at
> the "Converting to Single Static Assignment" step for more than 15
> minutes
> before erroring out as "SAT ran out of memory". I suspect the volume
> of C
> files that we feed to CBMC could be the issue.

Yes but if it gets as far as the SAT solver then it is not the case
that all hope is lost. Try other SAT or SMT solvers. You could also
try --refine and --refine-arithmetic which are mainly for performance
but might help you.

Another thing to try is using --depth instead of --unwind.

> May be I should verify parts
> of the code first instead of verifying the integrated code.

This is often a good idea if there is scope to do so.

> Yes my machine is x64 based i7 processor with 32GB RAM. I will try
> with a
> more recent version of CBMC as you suggested and get back.
>
> My code would look similar to some code generated from tools like
> Matlab/Simulink with lot of structs, pointers (you can assume 30 c
> files
> like the below image)
>
> [image: example.png]
>
>
> Function contracts could be useful for us. Thank you for sharing the
> details.

You are most welcome. I am sorry that I can't really help that much
more without access to the code.

Cheers,
- Martin

[Dinesh Kumar]

Dear Martin,

I am able to find "how to compile" CBMC using more modern SAT solvers in this documentation https://github.com/diffblue/cbmc/blob/cbmc-5.35.0/COMPILING.md 

Could you help me with the documentation/hint on how can I try out " SMT solver, Boolector/Bitwuzla, cvc4/cvc5 or z3" with CBMC ?

Thank you in advance.

Regards,

Dinesh

[Martin Nyx Brain]

On Thu, 2021-07-29 at 05:00 -0700, Dinesh Kumar wrote:
> Dear Martin,
>
> I am able to find "how to compile" CBMC using more modern SAT solvers
> in
> this
> documentation
> https://github.com/diffblue/cbmc/blob/cbmc-5.35.0/COMPILING.md

Yes; you can also try using --dimacs --outfile something.cnf to get a
feel for how large the CNF actually is.

> Could you help me with the documentation/hint on how can I try out "
> SMT
> solver, Boolector/Bitwuzla, cvc4/cvc5 or z3" with CBMC ?

Make sure cvc4, z3 or boolector is on your path and use --cvc4, --z3 or
--boolector. You can also use --smt2 --outfile something.smt2 to see
how big the file is and test out other solvers.

Note that it appears that support for solvers other than cvc4 and z3
has been broken in the most recent releases so you might have to try a
slightly older version.

Cheers,
- Martin