| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
This patch introduces nested let-abbreviations in the ExprSMTLIBPrinter
to reduce the size of the SMTLIBv2 queries and the corresponding processing
time (bugfix for #170).
The current implementation of the let abbreviation mode does not consider
expression intra-dependencies and prints all abbreviations in the same
let scope. For a (simplified) example, it prints
(assert (let ( (?B1 (A + B)) (?B2 (A + B + C)) ) (= ?B1 ?B2) ) ).
This is extremely inefficient if the expressions (and there many of these!)
extensively reuse their subexpressions. Therefore, it's better to print
the query with nested let-expressions by reusing existing expression bindings
in the new let scope:
(assert (let ( (?B1 (A + B)) ) (let ( (?B2 (?B1 + C)) ) (= ?B1 ?B2) ) ) ).
This patch adds a new function ExprSMTLIBPrinter::scanBindingExprDeps() that
scans bindings for expression dependencies. The result is a vector of
new bindings (orderedBindings) that represents the expression dependency tree.
When printing in the let-abbreviation mode, the new code starts with
abbreviating expressions that have no dependencies and then gradually makes
these new bindings available in the upcoming let-scopes where expressions
with dependencies reuse them.
The effect of nested let-abbreviations is comparable to :named abbreviations.
However, the latter mode is not supported by the majority of the solvers.
|
|
Fix overshift check
|
|
Shifting by bitwidth-1 is valid
|
|
|
|
|
|
|
|
single method with two different implementations.
There is one version of this method for human readability
(printHumanReadableQuery()) and a version for machine consumption
(printMachineReadableQuery()).
The reason for having two versions is because different behaviour is
needed in different scenarios
* In machine readable mode the entire query is printed inside a single
``(assert ...)``. This is done to allow ``(let ...)`` to abbreviate
as much as possible.
* In human readable mode each constraint and query expression is printed
inside its own ``(assert ...)`` unless the abbreviation mode is
ABBR_LET in which case all constraints and query expr are printed
inside a single ``(assert ...)`` much like in the machine readable mode
Whilst I was here I also fixed a bug handling identation when printing
``(let ...)`` expressions in printAssert()
|
|
* Set the default abbreviation mode to let (ExprSMTLIBPrinter::ABBR_LET)
* Remove the now defunct ExprSMTLIBLetPrinter
* Improve performance of ExprSMTLIBPrinter::scan() by keeping
track of visited Expr to avoid visiting them again
* Rename ExprSMTLIBPrinter::printQuery() to ExprSMTLIBPrinter::printQueryExpr()
|
|
Removed XFAIL tag from the Feature/VarArgLongDouble.c test
Fixed Executor to (more) correctly handle the alignment of types larger than 64bit (such as long double) when those are passed in var_args on x86_64.
Specifically:
From http://www.x86-64.org/documentation/abi.pdf
AMD64-ABI 3.5.7p5: Step 7.
Align l->overflow_arg_area upwards to a 16 byte boundary if alignment needed by type exceeds 8 byte boundary.
|
|
by @hpalikareva).
|
|
assertion entirely?
|
|
Also use bold green text when KLEE finishes. This is done by taking
advantage of llvm::raw_ostream's nice API for controlling the console
text colour.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
- Mostly fixed by removing unnecessary references.
|
|
|
|
|
|
|
|
- KCachegrind appears to expect the first function name to be preceeded by the
name of the file it appears in. Otherwise, it will end up creating two
different records for the function, one of which has no file name and won't
have any statistics.
|
|
- This makes KCachegrind output look nicer, as otherwise it assumes
instructions without debug info were inlined and shows some message to that
effect.
- This does however we might be lying a bit about the source line that an
instruction came from.
- This also adds a test case for our istats output, yay!
|
|
- I suspect no one is using this feature, and I'm not sure it is well conceived
either. Ripping it out for now in lieu of bothering to maintain it.
|
|
FloatingPointOps.ll).
|
|
- See comment, this is a gross workaround for Darwin's very small default limit
on shared memory size. I'm not sure how big of a counterexample users can
actually expect STP to solve in practice -- if there is a practical use for
larger ones it would probably be good for us to write a fallback strategy.
|
|
not asserts.
|
|
|
|
- This allows us to build in +Asserts mode even when LLVM isn't (by disabling
the checks in that mode).
- Eventually it would be nice to just move off of LLVM's DEBUG infrastructure
entirely and just have our own copy, but this works for now.
- Fixes #150.
|
|
|
|
- The change in 6829fb9 caused us to not allocation InstructionInfo objects for
instructions without source-level debug info, however, that means that all
such instructions end up sharing the one dummy InstructionInfo object, which
really breaks statistics tracking.
- This commit basically reverts that change, and also changes the code so we
don't ever use the dummy InstructionInfo object for instructions, so that
this problem can't be hit in other ways (e.g., if someone modifies the module
after the InstructionInfoTable construction). There is a FIXME for checking
the same thing for functions.
- Fixes #144.
|
|
unordered_{map,set} includes.
- I'm not sure what the status of libstdcxx's c++11 support is. It may be we
can just move over to <unordered_map> everywhere, but I don't have a Linux
test machine handy at the moment.
|
|
config.h files.
- There seems to be a better solution for this by defining a macro prefix, per:
http://www.gnu.org/software/autoconf-archive/ax_prefix_config_h.html
but I have no experience with that and it looks like it might involve
rewriting a bunch of our macro checks.
|
|
|
|
|
|
(independently).
In our recently switch to llvm::raw_ostream (and friends) (I think this
is d934d983692c8952cdb887cbcd59f2df0001b9c0) we forgot to flush the
llvm::raw_string_ostream to the underlying string used for error report
files (e.g. test000001.overshift.err) so we would end up writing an
empty string to error report files.
Also added a test case to catch this.
|
|
Add SimplifyExpressions command line option
|
|
|
|
|
|
|
|
iostream injects static constructor function into every compilation unit.
Remove this to avoid it.
|
|
According to LLVM: lightweight and simpler implementation of streams.
|
|
|
|
Allow users to bypass ConstraintManager::simplifyExpr(ref<Expr>).
|
|
This now corresponds to the sorts of the operations we emit, as far as I
can tell.
Read is one example of an operation that now works correctly (with 1-bit
array ranges).
It's also possible (but not very useful, and I don't think KLEE can
produce it) for other operations such as Add to operate on 1-bit values,
and this patch also fixes those.
|
|
|
|
MetaSMTBuilder.
|
