[GSOC 2018] Integrate with Z3 SMT solver

classic Classic list List threaded Threaded
12 messages Options
Reply | Threaded
Open this post in threaded view
|

[GSOC 2018] Integrate with Z3 SMT solver

Louis Dionne via cfe-dev
Hello,

I looked at the references on this mail http://lists.llvm.org/pipermail/cfe-dev/2018-March/057054.html and then looked at Z3ConstraintManager.cpp and I have some questions regarding the solver:

1) Right now we are not letting Z3 manage memory. Will it be a good idea to do that?
2) Can we flush the cache memory in the destructor of Z3Solver https://github.com/llvm-mirror/clang/blob/master/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp#L834 class?

Thank you very much,
Ashish Kumar Gahlot

--
Ashish Kumar Gahlot
IV year, UG
Govt. Engg. College, Ajmer, India

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: [GSOC 2018] Integrate with Z3 SMT solver

Louis Dionne via cfe-dev
I’m not sure what you mean by letting Z3 manage memory. Unless something has changed significantly since I looked at the source, the Z3 C++ API simply wraps memory management functions from the lower-level Z3 C API using C++ objects. Since the constraint manager is using the C API, due to compatibility issues with RTTI and exceptions, it needs to call the appropriate memory management functions.

Likewise, I’m not sure what cache memory you’re referring to. There was some discussion of a SMT query cache in CSA, but I don’t believe that was ever implemented.

Dominic

On Mar 8, 2018, at 5:01 AM, Ashish Gahlot via cfe-dev <[hidden email]> wrote:

Hello,

I looked at the references on this mail http://lists.llvm.org/pipermail/cfe-dev/2018-March/057054.html and then looked at Z3ConstraintManager.cpp and I have some questions regarding the solver:

1) Right now we are not letting Z3 manage memory. Will it be a good idea to do that?
2) Can we flush the cache memory in the destructor of Z3Solver https://github.com/llvm-mirror/clang/blob/master/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp#L834 class?

Thank you very much,
Ashish Kumar Gahlot

--
Ashish Kumar Gahlot
IV year, UG
Govt. Engg. College, Ajmer, India
_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev


_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: [GSOC 2018] Integrate with Z3 SMT solver

Louis Dionne via cfe-dev
Hi,

On 8 March 2018 at 19:00, Dominic Chen via cfe-dev
<[hidden email]> wrote:
> I’m not sure what you mean by letting Z3 manage memory. Unless something has
> changed significantly since I looked at the source, the Z3 C++ API simply
> wraps memory management functions from the lower-level Z3 C API using C++
> objects. Since the constraint manager is using the C API, due to
> compatibility issues with RTTI and exceptions, it needs to call the
> appropriate memory management functions.

I think he probably means the reference counting Z3_context. Z3
provides two ways to create a context.
`Z3_mk_context()` makes a context where the reference counting of
Z3_ast objects is done automatically, but the reference counting of
other objects (e.g. Z3_model) still need to be done manually.
`Z3_mk_context_rc()` makes a context where everything (including
`Z3_ast` objects) must be manually reference counted.

The Z3 C++ API actually now supports being used with exceptions and
RTTI. However I still think the C API is the better choice because its
more stable.

In KLEE we use `Z3_mk_context_rc()` because we want to be able to
cache expressions but we don't want to do so indefinitely (i.e. we
want to control when the reference counts goes to zero and memory gets
freed).

>
> Likewise, I’m not sure what cache memory you’re referring to. There was some
> discussion of a SMT query cache in CSA, but I don’t believe that was ever
> implemented.

@Ashish: I'm not sure what you mean either. Perhaps you mean Z3's
internal expression cache that it uses when `Z3_mk_context()`? is
used. This gets cleared when the created expressions go out of scope
when `Z3_solver_pop()` gets used.


@Dominic: On a related note. If you remember, a while back we spoke
about `Z3_mk_simple_solver()` vs `Z3_mk_solver()` and how their
performance characteristics and radically different (Z3_mk_solver()
being much faster most of the time for us in KLEE [1]).
I've just noticed that you're using `Z3_solver_push()` and
`Z3_solver_pop()`. We don't use that in KLEE and that might be we why
you had performance regressions when you tried switching to
`Z3_mk_solver()`. When you use Z3_solver_push(),
Z3 switches to a slower incremental solver internally [2,3]. You might
find that if you remove the pushes and pops and use `Z3_mk_solver()`
that things work better.

Actually there is a third way... If you create your own custom tactic
you will by-pass Z3's internal logic for trying to set up own solving
strategy. I think if you use push/pop with a custom tactic you'll
by-pass incremental solving
and likely get better performance.

Note in KLEE we end up creating a new `Z3_solver()` object for every
solver query. This isn't great but you have to do this (or use
`Z3_solver_reset()`) to clear the assertion stack without using
push/pop.
Because we don't use push/pop this necessitates that we do reference
counting manually (otherwise we'd never free Z3_asts until the
Z3_context gets destroyed).

[1] https://github.com/Z3Prover/z3/issues/1035
[2] https://github.com/Z3Prover/z3/issues/1459
[3] https://github.com/Z3Prover/z3/issues/1053

Thanks,
Dan.
_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: [GSOC 2018] Integrate with Z3 SMT solver

Louis Dionne via cfe-dev
Yes, I recall Nuno Lopes made a similar comment about the effect of
pushes and pops on the internal solver state, and that the performance
can differ depending on the workload. In fact, the initial
implementation did recreate the solver for each satisfiability query,
but it ended up being slower than the current version that reuses the
solver state.

Dominic

On 3/8/2018 4:46 PM, Dan Liew wrote:

> Hi,
>
> On 8 March 2018 at 19:00, Dominic Chen via cfe-dev
> <[hidden email]> wrote:
>> I’m not sure what you mean by letting Z3 manage memory. Unless something has
>> changed significantly since I looked at the source, the Z3 C++ API simply
>> wraps memory management functions from the lower-level Z3 C API using C++
>> objects. Since the constraint manager is using the C API, due to
>> compatibility issues with RTTI and exceptions, it needs to call the
>> appropriate memory management functions.
> I think he probably means the reference counting Z3_context. Z3
> provides two ways to create a context.
> `Z3_mk_context()` makes a context where the reference counting of
> Z3_ast objects is done automatically, but the reference counting of
> other objects (e.g. Z3_model) still need to be done manually.
> `Z3_mk_context_rc()` makes a context where everything (including
> `Z3_ast` objects) must be manually reference counted.
>
> The Z3 C++ API actually now supports being used with exceptions and
> RTTI. However I still think the C API is the better choice because its
> more stable.
>
> In KLEE we use `Z3_mk_context_rc()` because we want to be able to
> cache expressions but we don't want to do so indefinitely (i.e. we
> want to control when the reference counts goes to zero and memory gets
> freed).
>
>> Likewise, I’m not sure what cache memory you’re referring to. There was some
>> discussion of a SMT query cache in CSA, but I don’t believe that was ever
>> implemented.
> @Ashish: I'm not sure what you mean either. Perhaps you mean Z3's
> internal expression cache that it uses when `Z3_mk_context()`? is
> used. This gets cleared when the created expressions go out of scope
> when `Z3_solver_pop()` gets used.
>
>
> @Dominic: On a related note. If you remember, a while back we spoke
> about `Z3_mk_simple_solver()` vs `Z3_mk_solver()` and how their
> performance characteristics and radically different (Z3_mk_solver()
> being much faster most of the time for us in KLEE [1]).
> I've just noticed that you're using `Z3_solver_push()` and
> `Z3_solver_pop()`. We don't use that in KLEE and that might be we why
> you had performance regressions when you tried switching to
> `Z3_mk_solver()`. When you use Z3_solver_push(),
> Z3 switches to a slower incremental solver internally [2,3]. You might
> find that if you remove the pushes and pops and use `Z3_mk_solver()`
> that things work better.
>
> Actually there is a third way... If you create your own custom tactic
> you will by-pass Z3's internal logic for trying to set up own solving
> strategy. I think if you use push/pop with a custom tactic you'll
> by-pass incremental solving
> and likely get better performance.
>
> Note in KLEE we end up creating a new `Z3_solver()` object for every
> solver query. This isn't great but you have to do this (or use
> `Z3_solver_reset()`) to clear the assertion stack without using
> push/pop.
> Because we don't use push/pop this necessitates that we do reference
> counting manually (otherwise we'd never free Z3_asts until the
> Z3_context gets destroyed).
>
> [1] https://github.com/Z3Prover/z3/issues/1035
> [2] https://github.com/Z3Prover/z3/issues/1459
> [3] https://github.com/Z3Prover/z3/issues/1053
>
> Thanks,
> Dan.

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: [GSOC 2018] Integrate with Z3 SMT solver

Louis Dionne via cfe-dev
In reply to this post by Louis Dionne via cfe-dev
Hello,

Thank you for the detailed explanation.

On Fri, Mar 9, 2018 at 3:16 AM, Dan Liew <[hidden email]> wrote:

@Dominic: On a related note. If you remember, a while back we spoke
about `Z3_mk_simple_solver()` vs `Z3_mk_solver()` and how their
performance characteristics and radically different (Z3_mk_solver()
being much faster most of the time for us in KLEE [1]).
I've just noticed that you're using `Z3_solver_push()` and
`Z3_solver_pop()`. We don't use that in KLEE and that might be we why
you had performance regressions when you tried switching to
`Z3_mk_solver()`. When you use Z3_solver_push(),
Z3 switches to a slower incremental solver internally [2,3]. You might
find that if you remove the pushes and pops and use `Z3_mk_solver()`
that things work better.
 
I read the issue [2] and it explains that it when we use (push), z3 tries to
use the second solver. I think it would be a good idea to remove Solver.push()
from Z3ConstraintManager.

[1] https://github.com/Z3Prover/z3/issues/1035
[2] https://github.com/Z3Prover/z3/issues/1459
[3] https://github.com/Z3Prover/z3/issues/1053

Sorry for a noob question but is it possible to test the changes that I make to
Z3ConstraintManager.cpp without having to compile the whole clang every time?

Thank you very much,
Ashish Kumar Gahlot

--
Ashish Kumar Gahlot
IV year, UG
Govt. Engg. College, Ajmer, India

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: [GSOC 2018] Integrate with Z3 SMT solver

Louis Dionne via cfe-dev


On Mar 9, 2018, at 7:22 AM, Ashish Gahlot via cfe-dev <[hidden email]> wrote:

Hello,

Thank you for the detailed explanation.

On Fri, Mar 9, 2018 at 3:16 AM, Dan Liew <[hidden email]> wrote:

@Dominic: On a related note. If you remember, a while back we spoke
about `Z3_mk_simple_solver()` vs `Z3_mk_solver()` and how their
performance characteristics and radically different (Z3_mk_solver()
being much faster most of the time for us in KLEE [1]).
I've just noticed that you're using `Z3_solver_push()` and
`Z3_solver_pop()`. We don't use that in KLEE and that might be we why
you had performance regressions when you tried switching to
`Z3_mk_solver()`. When you use Z3_solver_push(),
Z3 switches to a slower incremental solver internally [2,3]. You might
find that if you remove the pushes and pops and use `Z3_mk_solver()`
that things work better.
 
I read the issue [2] and it explains that it when we use (push), z3 tries to
use the second solver. I think it would be a good idea to remove Solver.push()
from Z3ConstraintManager.

[1] https://github.com/Z3Prover/z3/issues/1035
[2] https://github.com/Z3Prover/z3/issues/1459
[3] https://github.com/Z3Prover/z3/issues/1053

Sorry for a noob question but is it possible to test the changes that I make to
Z3ConstraintManager.cpp without having to compile the whole clang every time?

It does not recompile everything, whenever you type “ninja clang” (or “make clang”)
from the build folder it only recompiles the changed file and does the relinking.
Headers are a different story — then it has to recompile all the files that transitively include that header,
unfortunately, nothing that can be done there.


Thank you very much,
Ashish Kumar Gahlot

--
Ashish Kumar Gahlot
IV year, UG
Govt. Engg. College, Ajmer, India
_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev


_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: [GSOC 2018] Integrate with Z3 SMT solver

Louis Dionne via cfe-dev
Hello,

I am having some doubts regarding the z3 constraint manager:

1) what is the correct way of invoking the z3 constraint on a c++/c file. Right now I am using clang -cc1 -analyzer-constraints=z3 -analyze -analyzer-checker=core,unix,debug.ExprInspection -verify /root/clang-llvm/llvm/tools/clang/test/Analysis/region-store.c which reports WARNING: unknown parameter 'timeout'
Legal parameters are:
  auto_config (bool) (default: true)
  debug_ref_count (bool) (default: false)
                 ...<snip>...

I also tried the syntax mentioned in the last comment here but it gives the same error mentioned above.

2) when I remove timeout option from Z3Config(), the output is null. Is it the correct behavior?
3) how can I test the performance of the analyzer when I make changes in Z3ConstraintManager.cpp?


Thank you very much,
Ashish Kumar Gahlot

On Sat, Mar 10, 2018 at 1:13 AM, George Karpenkov <[hidden email]> wrote:


On Mar 9, 2018, at 7:22 AM, Ashish Gahlot via cfe-dev <[hidden email]> wrote:

Hello,

Thank you for the detailed explanation.

On Fri, Mar 9, 2018 at 3:16 AM, Dan Liew <[hidden email]> wrote:

@Dominic: On a related note. If you remember, a while back we spoke
about `Z3_mk_simple_solver()` vs `Z3_mk_solver()` and how their
performance characteristics and radically different (Z3_mk_solver()
being much faster most of the time for us in KLEE [1]).
I've just noticed that you're using `Z3_solver_push()` and
`Z3_solver_pop()`. We don't use that in KLEE and that might be we why
you had performance regressions when you tried switching to
`Z3_mk_solver()`. When you use Z3_solver_push(),
Z3 switches to a slower incremental solver internally [2,3]. You might
find that if you remove the pushes and pops and use `Z3_mk_solver()`
that things work better.
 
I read the issue [2] and it explains that it when we use (push), z3 tries to
use the second solver. I think it would be a good idea to remove Solver.push()
from Z3ConstraintManager.

[1] https://github.com/Z3Prover/z3/issues/1035
[2] https://github.com/Z3Prover/z3/issues/1459
[3] https://github.com/Z3Prover/z3/issues/1053

Sorry for a noob question but is it possible to test the changes that I make to
Z3ConstraintManager.cpp without having to compile the whole clang every time?

It does not recompile everything, whenever you type “ninja clang” (or “make clang”)
from the build folder it only recompiles the changed file and does the relinking.
Headers are a different story — then it has to recompile all the files that transitively include that header,
unfortunately, nothing that can be done there.


Thank you very much,
Ashish Kumar Gahlot

--
Ashish Kumar Gahlot
IV year, UG
Govt. Engg. College, Ajmer, India
_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev




--
Ashish Kumar Gahlot
IV year, UG
Govt. Engg. College, Ajmer, India

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: [GSOC 2018] Integrate with Z3 SMT solver

Louis Dionne via cfe-dev
In reply to this post by Louis Dionne via cfe-dev
The implementation of the incremental stuff has improved in Z3 in the past
year. Now the "fast" SAT solver supports a bit of incrementally. So the
major difference now is that with push() you switch to the SMT solver that
does lazy bit-blasting and the new solver does it eagerly for the whole
formula.
BTW, there's a 3rd option which is to reset the solver.

I agree that going with a custom tactic is the way to go. Otherwise you are
exposed to changes in the internals of Z3 and you never know what's running
underneath. Also, you can tune the set of tactics for the formulas that
clang generates.  I can help with this if there's interest.

Nuno

-----Original Message-----
From: Dominic Chen via cfe-dev
Sent: Thursday, March 8, 2018 10:13 PM
Subject: Re: [cfe-dev] [GSOC 2018] Integrate with Z3 SMT solver

Yes, I recall Nuno Lopes made a similar comment about the effect of
pushes and pops on the internal solver state, and that the performance
can differ depending on the workload. In fact, the initial
implementation did recreate the solver for each satisfiability query,
but it ended up being slower than the current version that reuses the
solver state.

Dominic

On 3/8/2018 4:46 PM, Dan Liew wrote:

> Hi,
>
> On 8 March 2018 at 19:00, Dominic Chen via cfe-dev
> <[hidden email]> wrote:
>> I’m not sure what you mean by letting Z3 manage memory. Unless something
>> has
>> changed significantly since I looked at the source, the Z3 C++ API simply
>> wraps memory management functions from the lower-level Z3 C API using C++
>> objects. Since the constraint manager is using the C API, due to
>> compatibility issues with RTTI and exceptions, it needs to call the
>> appropriate memory management functions.
> I think he probably means the reference counting Z3_context. Z3
> provides two ways to create a context.
> `Z3_mk_context()` makes a context where the reference counting of
> Z3_ast objects is done automatically, but the reference counting of
> other objects (e.g. Z3_model) still need to be done manually.
> `Z3_mk_context_rc()` makes a context where everything (including
> `Z3_ast` objects) must be manually reference counted.
>
> The Z3 C++ API actually now supports being used with exceptions and
> RTTI. However I still think the C API is the better choice because its
> more stable.
>
> In KLEE we use `Z3_mk_context_rc()` because we want to be able to
> cache expressions but we don't want to do so indefinitely (i.e. we
> want to control when the reference counts goes to zero and memory gets
> freed).
>
>> Likewise, I’m not sure what cache memory you’re referring to. There was
>> some
>> discussion of a SMT query cache in CSA, but I don’t believe that was ever
>> implemented.
> @Ashish: I'm not sure what you mean either. Perhaps you mean Z3's
> internal expression cache that it uses when `Z3_mk_context()`? is
> used. This gets cleared when the created expressions go out of scope
> when `Z3_solver_pop()` gets used.
>
>
> @Dominic: On a related note. If you remember, a while back we spoke
> about `Z3_mk_simple_solver()` vs `Z3_mk_solver()` and how their
> performance characteristics and radically different (Z3_mk_solver()
> being much faster most of the time for us in KLEE [1]).
> I've just noticed that you're using `Z3_solver_push()` and
> `Z3_solver_pop()`. We don't use that in KLEE and that might be we why
> you had performance regressions when you tried switching to
> `Z3_mk_solver()`. When you use Z3_solver_push(),
> Z3 switches to a slower incremental solver internally [2,3]. You might
> find that if you remove the pushes and pops and use `Z3_mk_solver()`
> that things work better.
>
> Actually there is a third way... If you create your own custom tactic
> you will by-pass Z3's internal logic for trying to set up own solving
> strategy. I think if you use push/pop with a custom tactic you'll
> by-pass incremental solving
> and likely get better performance.
>
> Note in KLEE we end up creating a new `Z3_solver()` object for every
> solver query. This isn't great but you have to do this (or use
> `Z3_solver_reset()`) to clear the assertion stack without using
> push/pop.
> Because we don't use push/pop this necessitates that we do reference
> counting manually (otherwise we'd never free Z3_asts until the
> Z3_context gets destroyed).
>
> [1] https://github.com/Z3Prover/z3/issues/1035
> [2] https://github.com/Z3Prover/z3/issues/1459
> [3] https://github.com/Z3Prover/z3/issues/1053
>
> Thanks,
> Dan.

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: [GSOC 2018] Integrate with Z3 SMT solver

Louis Dionne via cfe-dev
Hi,

In our experiments (we convert about 9000 C program to SMT almost daily), disabling relevancy gives a massive speed up in the verification time (we, however, don't use the incremental mode); maybe that's something to try on clang.

Thank you,

2018-03-11 12:57 GMT+00:00 Nuno Lopes via cfe-dev <[hidden email]>:
The implementation of the incremental stuff has improved in Z3 in the past year. Now the "fast" SAT solver supports a bit of incrementally. So the major difference now is that with push() you switch to the SMT solver that does lazy bit-blasting and the new solver does it eagerly for the whole formula.
BTW, there's a 3rd option which is to reset the solver.

I agree that going with a custom tactic is the way to go. Otherwise you are exposed to changes in the internals of Z3 and you never know what's running underneath. Also, you can tune the set of tactics for the formulas that clang generates.  I can help with this if there's interest.

Nuno


-----Original Message-----
From: Dominic Chen via cfe-dev
Sent: Thursday, March 8, 2018 10:13 PM
Subject: Re: [cfe-dev] [GSOC 2018] Integrate with Z3 SMT solver

Yes, I recall Nuno Lopes made a similar comment about the effect of
pushes and pops on the internal solver state, and that the performance
can differ depending on the workload. In fact, the initial
implementation did recreate the solver for each satisfiability query,
but it ended up being slower than the current version that reuses the
solver state.

Dominic

On 3/8/2018 4:46 PM, Dan Liew wrote:
Hi,

On 8 March 2018 at 19:00, Dominic Chen via cfe-dev
<[hidden email]> wrote:
I’m not sure what you mean by letting Z3 manage memory. Unless something has
changed significantly since I looked at the source, the Z3 C++ API simply
wraps memory management functions from the lower-level Z3 C API using C++
objects. Since the constraint manager is using the C API, due to
compatibility issues with RTTI and exceptions, it needs to call the
appropriate memory management functions.
I think he probably means the reference counting Z3_context. Z3
provides two ways to create a context.
`Z3_mk_context()` makes a context where the reference counting of
Z3_ast objects is done automatically, but the reference counting of
other objects (e.g. Z3_model) still need to be done manually.
`Z3_mk_context_rc()` makes a context where everything (including
`Z3_ast` objects) must be manually reference counted.

The Z3 C++ API actually now supports being used with exceptions and
RTTI. However I still think the C API is the better choice because its
more stable.

In KLEE we use `Z3_mk_context_rc()` because we want to be able to
cache expressions but we don't want to do so indefinitely (i.e. we
want to control when the reference counts goes to zero and memory gets
freed).

Likewise, I’m not sure what cache memory you’re referring to. There was some
discussion of a SMT query cache in CSA, but I don’t believe that was ever
implemented.
@Ashish: I'm not sure what you mean either. Perhaps you mean Z3's
internal expression cache that it uses when `Z3_mk_context()`? is
used. This gets cleared when the created expressions go out of scope
when `Z3_solver_pop()` gets used.


@Dominic: On a related note. If you remember, a while back we spoke
about `Z3_mk_simple_solver()` vs `Z3_mk_solver()` and how their
performance characteristics and radically different (Z3_mk_solver()
being much faster most of the time for us in KLEE [1]).
I've just noticed that you're using `Z3_solver_push()` and
`Z3_solver_pop()`. We don't use that in KLEE and that might be we why
you had performance regressions when you tried switching to
`Z3_mk_solver()`. When you use Z3_solver_push(),
Z3 switches to a slower incremental solver internally [2,3]. You might
find that if you remove the pushes and pops and use `Z3_mk_solver()`
that things work better.

Actually there is a third way... If you create your own custom tactic
you will by-pass Z3's internal logic for trying to set up own solving
strategy. I think if you use push/pop with a custom tactic you'll
by-pass incremental solving
and likely get better performance.

Note in KLEE we end up creating a new `Z3_solver()` object for every
solver query. This isn't great but you have to do this (or use
`Z3_solver_reset()`) to clear the assertion stack without using
push/pop.
Because we don't use push/pop this necessitates that we do reference
counting manually (otherwise we'd never free Z3_asts until the
Z3_context gets destroyed).

[1] https://github.com/Z3Prover/z3/issues/1035
[2] https://github.com/Z3Prover/z3/issues/1459
[3] https://github.com/Z3Prover/z3/issues/1053

Thanks,
Dan.

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev



--

Mikhail Ramalho.

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: [GSOC 2018] Integrate with Z3 SMT solver

Louis Dionne via cfe-dev
In reply to this post by Louis Dionne via cfe-dev
Interesting, thanks for the update. I'm not actively working on
Z3ConstraintManager, so anyone interested should go for it. There's
plenty of room for performance improvements.

Dominic

On 3/11/2018 8:57 AM, Nuno Lopes wrote:

> The implementation of the incremental stuff has improved in Z3 in the
> past year. Now the "fast" SAT solver supports a bit of incrementally.
> So the major difference now is that with push() you switch to the SMT
> solver that does lazy bit-blasting and the new solver does it eagerly
> for the whole formula.
> BTW, there's a 3rd option which is to reset the solver.
>
> I agree that going with a custom tactic is the way to go. Otherwise
> you are exposed to changes in the internals of Z3 and you never know
> what's running underneath. Also, you can tune the set of tactics for
> the formulas that clang generates.  I can help with this if there's
> interest.
>
> Nuno
>
> -----Original Message-----
> From: Dominic Chen via cfe-dev
> Sent: Thursday, March 8, 2018 10:13 PM
> Subject: Re: [cfe-dev] [GSOC 2018] Integrate with Z3 SMT solver
>
> Yes, I recall Nuno Lopes made a similar comment about the effect of
> pushes and pops on the internal solver state, and that the performance
> can differ depending on the workload. In fact, the initial
> implementation did recreate the solver for each satisfiability query,
> but it ended up being slower than the current version that reuses the
> solver state.
>
> Dominic
_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: [GSOC 2018] Integrate with Z3 SMT solver

Louis Dionne via cfe-dev
In reply to this post by Louis Dionne via cfe-dev
Hello,

Hi,

In our experiments (we convert about 9000 C program to SMT almost daily), disabling relevancy gives a massive speed up in the verification time (we, however, don't use the incremental mode); maybe that's something to try on clang.

Can you tell me how do you perform those tests?

Thank you,
Ashish Kumar Gahlot

On Mon, Mar 12, 2018 at 1:09 AM, Mikhail Ramalho via cfe-dev <[hidden email]> wrote:
Hi,

In our experiments (we convert about 9000 C program to SMT almost daily), disabling relevancy gives a massive speed up in the verification time (we, however, don't use the incremental mode); maybe that's something to try on clang.

Thank you,

2018-03-11 12:57 GMT+00:00 Nuno Lopes via cfe-dev <[hidden email]>:
The implementation of the incremental stuff has improved in Z3 in the past year. Now the "fast" SAT solver supports a bit of incrementally. So the major difference now is that with push() you switch to the SMT solver that does lazy bit-blasting and the new solver does it eagerly for the whole formula.
BTW, there's a 3rd option which is to reset the solver.

I agree that going with a custom tactic is the way to go. Otherwise you are exposed to changes in the internals of Z3 and you never know what's running underneath. Also, you can tune the set of tactics for the formulas that clang generates.  I can help with this if there's interest.

Nuno


-----Original Message-----
From: Dominic Chen via cfe-dev
Sent: Thursday, March 8, 2018 10:13 PM
Subject: Re: [cfe-dev] [GSOC 2018] Integrate with Z3 SMT solver

Yes, I recall Nuno Lopes made a similar comment about the effect of
pushes and pops on the internal solver state, and that the performance
can differ depending on the workload. In fact, the initial
implementation did recreate the solver for each satisfiability query,
but it ended up being slower than the current version that reuses the
solver state.

Dominic

On 3/8/2018 4:46 PM, Dan Liew wrote:
Hi,

On 8 March 2018 at 19:00, Dominic Chen via cfe-dev
<[hidden email]> wrote:
I’m not sure what you mean by letting Z3 manage memory. Unless something has
changed significantly since I looked at the source, the Z3 C++ API simply
wraps memory management functions from the lower-level Z3 C API using C++
objects. Since the constraint manager is using the C API, due to
compatibility issues with RTTI and exceptions, it needs to call the
appropriate memory management functions.
I think he probably means the reference counting Z3_context. Z3
provides two ways to create a context.
`Z3_mk_context()` makes a context where the reference counting of
Z3_ast objects is done automatically, but the reference counting of
other objects (e.g. Z3_model) still need to be done manually.
`Z3_mk_context_rc()` makes a context where everything (including
`Z3_ast` objects) must be manually reference counted.

The Z3 C++ API actually now supports being used with exceptions and
RTTI. However I still think the C API is the better choice because its
more stable.

In KLEE we use `Z3_mk_context_rc()` because we want to be able to
cache expressions but we don't want to do so indefinitely (i.e. we
want to control when the reference counts goes to zero and memory gets
freed).

Likewise, I’m not sure what cache memory you’re referring to. There was some
discussion of a SMT query cache in CSA, but I don’t believe that was ever
implemented.
@Ashish: I'm not sure what you mean either. Perhaps you mean Z3's
internal expression cache that it uses when `Z3_mk_context()`? is
used. This gets cleared when the created expressions go out of scope
when `Z3_solver_pop()` gets used.


@Dominic: On a related note. If you remember, a while back we spoke
about `Z3_mk_simple_solver()` vs `Z3_mk_solver()` and how their
performance characteristics and radically different (Z3_mk_solver()
being much faster most of the time for us in KLEE [1]).
I've just noticed that you're using `Z3_solver_push()` and
`Z3_solver_pop()`. We don't use that in KLEE and that might be we why
you had performance regressions when you tried switching to
`Z3_mk_solver()`. When you use Z3_solver_push(),
Z3 switches to a slower incremental solver internally [2,3]. You might
find that if you remove the pushes and pops and use `Z3_mk_solver()`
that things work better.

Actually there is a third way... If you create your own custom tactic
you will by-pass Z3's internal logic for trying to set up own solving
strategy. I think if you use push/pop with a custom tactic you'll
by-pass incremental solving
and likely get better performance.

Note in KLEE we end up creating a new `Z3_solver()` object for every
solver query. This isn't great but you have to do this (or use
`Z3_solver_reset()`) to clear the assertion stack without using
push/pop.
Because we don't use push/pop this necessitates that we do reference
counting manually (otherwise we'd never free Z3_asts until the
Z3_context gets destroyed).

[1] https://github.com/Z3Prover/z3/issues/1035
[2] https://github.com/Z3Prover/z3/issues/1459
[3] https://github.com/Z3Prover/z3/issues/1053

Thanks,
Dan.

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev



--

Mikhail Ramalho.

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev




--
Ashish Kumar Gahlot
IV year, UG
Govt. Engg. College, Ajmer, India

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: [GSOC 2018] Integrate with Z3 SMT solver

Louis Dionne via cfe-dev
Hello all,

I was looking at Klee source and found that there was an API change in Z3 4.4.1 in function Z3_get_error_msg().
Since Z3 4.6.0 is already released, would it be useful to provide backward compatibility?

Thank you,
Ashish Kumar Gahlot

On Mon, Mar 12, 2018 at 12:48 PM, Ashish Gahlot <[hidden email]> wrote:
Hello,

Hi,

In our experiments (we convert about 9000 C program to SMT almost daily), disabling relevancy gives a massive speed up in the verification time (we, however, don't use the incremental mode); maybe that's something to try on clang.

Can you tell me how do you perform those tests?

Thank you,
Ashish Kumar Gahlot

On Mon, Mar 12, 2018 at 1:09 AM, Mikhail Ramalho via cfe-dev <[hidden email]> wrote:
Hi,

In our experiments (we convert about 9000 C program to SMT almost daily), disabling relevancy gives a massive speed up in the verification time (we, however, don't use the incremental mode); maybe that's something to try on clang.

Thank you,

2018-03-11 12:57 GMT+00:00 Nuno Lopes via cfe-dev <[hidden email]>:
The implementation of the incremental stuff has improved in Z3 in the past year. Now the "fast" SAT solver supports a bit of incrementally. So the major difference now is that with push() you switch to the SMT solver that does lazy bit-blasting and the new solver does it eagerly for the whole formula.
BTW, there's a 3rd option which is to reset the solver.

I agree that going with a custom tactic is the way to go. Otherwise you are exposed to changes in the internals of Z3 and you never know what's running underneath. Also, you can tune the set of tactics for the formulas that clang generates.  I can help with this if there's interest.

Nuno


-----Original Message-----
From: Dominic Chen via cfe-dev
Sent: Thursday, March 8, 2018 10:13 PM
Subject: Re: [cfe-dev] [GSOC 2018] Integrate with Z3 SMT solver

Yes, I recall Nuno Lopes made a similar comment about the effect of
pushes and pops on the internal solver state, and that the performance
can differ depending on the workload. In fact, the initial
implementation did recreate the solver for each satisfiability query,
but it ended up being slower than the current version that reuses the
solver state.

Dominic

On 3/8/2018 4:46 PM, Dan Liew wrote:
Hi,

On 8 March 2018 at 19:00, Dominic Chen via cfe-dev
<[hidden email]> wrote:
I’m not sure what you mean by letting Z3 manage memory. Unless something has
changed significantly since I looked at the source, the Z3 C++ API simply
wraps memory management functions from the lower-level Z3 C API using C++
objects. Since the constraint manager is using the C API, due to
compatibility issues with RTTI and exceptions, it needs to call the
appropriate memory management functions.
I think he probably means the reference counting Z3_context. Z3
provides two ways to create a context.
`Z3_mk_context()` makes a context where the reference counting of
Z3_ast objects is done automatically, but the reference counting of
other objects (e.g. Z3_model) still need to be done manually.
`Z3_mk_context_rc()` makes a context where everything (including
`Z3_ast` objects) must be manually reference counted.

The Z3 C++ API actually now supports being used with exceptions and
RTTI. However I still think the C API is the better choice because its
more stable.

In KLEE we use `Z3_mk_context_rc()` because we want to be able to
cache expressions but we don't want to do so indefinitely (i.e. we
want to control when the reference counts goes to zero and memory gets
freed).

Likewise, I’m not sure what cache memory you’re referring to. There was some
discussion of a SMT query cache in CSA, but I don’t believe that was ever
implemented.
@Ashish: I'm not sure what you mean either. Perhaps you mean Z3's
internal expression cache that it uses when `Z3_mk_context()`? is
used. This gets cleared when the created expressions go out of scope
when `Z3_solver_pop()` gets used.


@Dominic: On a related note. If you remember, a while back we spoke
about `Z3_mk_simple_solver()` vs `Z3_mk_solver()` and how their
performance characteristics and radically different (Z3_mk_solver()
being much faster most of the time for us in KLEE [1]).
I've just noticed that you're using `Z3_solver_push()` and
`Z3_solver_pop()`. We don't use that in KLEE and that might be we why
you had performance regressions when you tried switching to
`Z3_mk_solver()`. When you use Z3_solver_push(),
Z3 switches to a slower incremental solver internally [2,3]. You might
find that if you remove the pushes and pops and use `Z3_mk_solver()`
that things work better.

Actually there is a third way... If you create your own custom tactic
you will by-pass Z3's internal logic for trying to set up own solving
strategy. I think if you use push/pop with a custom tactic you'll
by-pass incremental solving
and likely get better performance.

Note in KLEE we end up creating a new `Z3_solver()` object for every
solver query. This isn't great but you have to do this (or use
`Z3_solver_reset()`) to clear the assertion stack without using
push/pop.
Because we don't use push/pop this necessitates that we do reference
counting manually (otherwise we'd never free Z3_asts until the
Z3_context gets destroyed).

[1] https://github.com/Z3Prover/z3/issues/1035
[2] https://github.com/Z3Prover/z3/issues/1459
[3] https://github.com/Z3Prover/z3/issues/1053

Thanks,
Dan.

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev



--

Mikhail Ramalho.

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev




--
Ashish Kumar Gahlot
IV year, UG
Govt. Engg. College, Ajmer, India



--
Ashish Kumar Gahlot
IV year, UG
Govt. Engg. College, Ajmer, India

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev