Z3 fixes and enhancements #658

delcypher · 2017-05-24T18:01:44Z

This upstreams a bunch of enhancements for working with Z3 from my fork.

@ccadar This includes the Z3 API logging I mentioned to you (see -z3-log-interaction option).

It also starts to address #653. I won't continue doing that until this PR is merged.

to guess it means timeout but I'm not 100% sure about this.

into `Z3Builder.cpp` so they can be called from in gdb.

andreamattavelli

@delcypher thanks for your work!
Besides some small changes I would apply, looks good to me.

andreamattavelli · 2017-05-25T08:38:47Z

lib/Solver/Z3Builder.cpp

+  if (z3LogInteractionFileArg)
+    this->z3LogInteractionFile = std::string(z3LogInteractionFileArg);
+  if (z3LogInteractionFile.length() > 0) {
+    llvm::errs() << "Logging Z3 API interaction to \"" << z3LogInteractionFile


I would use klee_message for consistency with other messages.

The Z3Solver is also used in the kleaver tool. Are you sure you want this change? Same applies for the other comments.

Well, if I'm not wrong we already use klee_warning in both STPSolver.cpp and Z3Solver.cpp.

So we do. I didn't put them there though...
I'll go ahead and make the changes then.

andreamattavelli · 2017-05-25T08:40:52Z

include/klee/Internal/Support/FileHandling.h

+#include <string>
+
+namespace klee {
+llvm::raw_fd_ostream *klee_open_file(std::string &path, std::string &error);


I belive that we can now use this new functionality in many other places.

@delcypher this is just a comment btw

Thanks for clarifying.

andreamattavelli · 2017-05-25T08:41:29Z

lib/Solver/Z3Solver.cpp

+    std::string error;
+    dumpedQueriesFile = klee_open_file(Z3QueryDumpFile, error);
+    if (!error.empty()) {
+      llvm::errs() << "Error creating file for dumping Z3 queries:" << error


I would use klee_error for consistency.

andreamattavelli · 2017-05-25T08:46:33Z

@delcypher I forgot to mention that 84464e9 and bcb498a should me squashed together in my opinion.

delcypher · 2017-05-25T09:38:23Z

@andreamattavelli

@delcypher I forgot to mention that 84464e9 and bcb498a should me squashed together in my opinion

Agreed. I'll do that once we've reached a decision on your other suggested changes.

`klee_open_output_file()` function so that it can be used by the Z3Solver.

delcypher · 2017-05-25T10:53:40Z

@andreamattavelli I've made your suggested changes. I also renamed klee_open_file() to klee_open_output_file() to make it clear the opened file is for writing, not reading.

andreamattavelli · 2017-05-25T13:57:17Z

@delcypher Great! I don't have any more comments. I give @ccadar the opportunity to comment before merging.

ccadar · 2017-05-25T14:41:23Z

This looks ok, but it would be useful to describe the new options in the documentation before merging.

delcypher · 2017-05-25T15:17:27Z

@ccadar Not all of these options are permanent. -z3-query-dump= for example is a hack that will be removed if the work I started and gave up on in #629 ever gets accepted.

ccadar · 2017-05-25T19:30:41Z

If they change, the documentation will change with them. I don't see this as a reason not to document them. Also, the unwritten convention is to name validation/debugging techniques using the prefix debug-, would you be happy with this?

delcypher · 2017-05-25T21:51:30Z

If they change, the documentation will change with them. I don't see this as a reason not to document them.

I don't want people to rely on something that is likely to change quite soon.

Also, the unwritten convention is to name validation/debugging techniques using the prefix debug-, would you be happy with this?

Not really but for selfish reasons

The -z3-* options appear at the end of -help which makes finding them super convenient.
Changing the names will cause me problems the next time I rebase on master.

If you insist I can change them.

delcypher · 2017-05-25T21:52:28Z

Documentation written: klee/klee.github.io#85

It documents options as they are now and also a bunch of options for the other solver backends too.

is useful for getting access to the constraints being stored in the Z3 solver in the SMT-LIBv2.5 format.

This can be enabled by passing the command line option `-debug-z3-validate-models`. Although Z3 has a global parameter `model_validate` (off by default) I don't trust it so do the validation manually. This also means we can potentially do validation on a per Z3Solver instance basis rather than globally. When failing to validate a Z3 model the solver state and model are dumped to standard error.

Add `-debug-z3-log-api-interaction` option to allow Z3 API calls to be logged to a file. The files logged by this option can be replayed by the `z3` binary (using its `-log` option). This is incredibly useful because it allows to exactly replay Z3's behaviour outside of KLEE.

solver. This is to avoid tampering with the cache of the builder the solver is using.

My discussions [1] with the Z3 team have revealed that `Z3_mk_simple_solver()` is the wrong solver to use. That solver basically runs the `simplify` tactic and then the `smt` tactic. This by-passes Z3's attempt to probe for different logics and apply its own specialized tactic. Using `Z3_mk_solver()` should be closer to the behaviour of the Z3 binary. This partially addresses klee#653. We still need to try rolling our own custom tactic. [1] Z3Prover/z3#1035

…:<N>` option. This lets us see what Z3 is doing execution (e.g. which tactic is being applied) which is very useful for debugging.

options in klee/klee#658

delcypher · 2017-05-26T08:14:27Z

@ccadar Options have been renamed.

options in klee/klee#658

andreamattavelli · 2017-06-01T06:44:56Z

@delcypher @ccadar I think we are ready to merge as I don't see any reason to not do it.

ccadar · 2017-06-01T10:31:14Z

This LGTM too. I think @delcypher wanted to squash some commits, otherwise we're ready to merge.

delcypher · 2017-06-01T10:36:04Z

@ccadar I've already done all the squashing I wanted. Merging now.

options for the Z3 solver from klee/klee#658

Dan Liew added 3 commits May 24, 2017 18:27

[Z3] Support another solver failure reason that Z3 might give. I'm going

f4cce58

to guess it means timeout but I'm not 100% sure about this.

[Z3] Add assertions in Z3 builder to catch underflow with bad widths.

cb2209a

[Z3] Move the dump() methods of the Z3NodeHandle<> specializations

80d5eec

into `Z3Builder.cpp` so they can be called from in gdb.

delcypher mentioned this pull request May 24, 2017

Z3 debugging #467

Closed

andreamattavelli requested changes May 25, 2017

View reviewed changes

Refactor file opening code out of main.cpp and into

ccab52d

`klee_open_output_file()` function so that it can be used by the Z3Solver.

delcypher force-pushed the z3_fixes_and_enhancements branch from 528fc39 to 8a56389 Compare May 25, 2017 10:52

delcypher mentioned this pull request May 25, 2017

[WIP] Sketch Z3 custom tactic #659

Closed

delcypher mentioned this pull request May 25, 2017

Document solver specific options klee/klee.github.io#85

Merged

Dan Liew added 7 commits May 26, 2017 08:47

[Z3] Add the -debug-z3-dump-queries=<path> command line option. This

676e816

is useful for getting access to the constraints being stored in the Z3 solver in the SMT-LIBv2.5 format.

[Z3] In getConstraintLog() use a separate builder from that of the

a541e84

solver. This is to avoid tampering with the cache of the builder the solver is using.

[Z3] Add -debug-z3-verbosity=<N> option which behaves like Z3's `-v…

b38e9bf

…:<N>` option. This lets us see what Z3 is doing execution (e.g. which tactic is being applied) which is very useful for debugging.

[Z3] Remove unused include.

540a3e5

delcypher force-pushed the z3_fixes_and_enhancements branch from 8a56389 to 540a3e5 Compare May 26, 2017 08:13

delcypher pushed a commit to delcypher/klee.github.io that referenced this pull request May 26, 2017

Document solver specific options including the new Z3 specific

9669a45

options in klee/klee#658

delcypher pushed a commit to delcypher/klee.github.io that referenced this pull request May 31, 2017

Document solver specific options including the new Z3 specific

66ab0f1

options in klee/klee#658

andreamattavelli approved these changes Jun 1, 2017

View reviewed changes

delcypher merged commit 641bc46 into klee:master Jun 1, 2017

delcypher pushed a commit to delcypher/klee.github.io that referenced this pull request Jun 1, 2017

Document core solver options including the new

1cdf5a8

options for the Z3 solver from klee/klee#658

ccadar pushed a commit to ccadar/klee.github.io that referenced this pull request Sep 14, 2018

Document core solver options including the new

9e7ca92

options for the Z3 solver from klee/klee#658

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Z3 fixes and enhancements #658

Z3 fixes and enhancements #658

delcypher commented May 24, 2017

andreamattavelli left a comment

andreamattavelli May 25, 2017

delcypher May 25, 2017

andreamattavelli May 25, 2017

delcypher May 25, 2017

andreamattavelli May 25, 2017

andreamattavelli May 25, 2017

delcypher May 25, 2017

andreamattavelli May 25, 2017

andreamattavelli commented May 25, 2017

delcypher commented May 25, 2017

delcypher commented May 25, 2017

andreamattavelli commented May 25, 2017

ccadar commented May 25, 2017

delcypher commented May 25, 2017

ccadar commented May 25, 2017

delcypher commented May 25, 2017 •

edited

delcypher commented May 25, 2017

delcypher commented May 26, 2017

andreamattavelli commented Jun 1, 2017

ccadar commented Jun 1, 2017

delcypher commented Jun 1, 2017

Z3 fixes and enhancements #658

Z3 fixes and enhancements #658

Conversation

delcypher commented May 24, 2017

andreamattavelli left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

andreamattavelli commented May 25, 2017

delcypher commented May 25, 2017

delcypher commented May 25, 2017

andreamattavelli commented May 25, 2017

ccadar commented May 25, 2017

delcypher commented May 25, 2017

ccadar commented May 25, 2017

delcypher commented May 25, 2017 • edited

delcypher commented May 25, 2017

delcypher commented May 26, 2017

andreamattavelli commented Jun 1, 2017

ccadar commented Jun 1, 2017

delcypher commented Jun 1, 2017

delcypher commented May 25, 2017 •

edited