Summary:
Since we don't yet support `.sig` files for fields, hardcoding this in Ocaml
for now.
Reviewed By: jvillard
Differential Revision: D23627390
fbshipit-source-id: 8df78068d
Summary: Polynomial category zero corresponds to unreachable but "zero" is a misnomer and rather confusing. Let's fix it.
Reviewed By: skcho
Differential Revision: D23597735
fbshipit-source-id: f0c96ed26
Summary:
Eliminate the need to serialise procnames when sending work from the restart scheduler to the workers, by sending the proc_uid instead. This is (much) shorter than the byte representation of the proc_name and it's the primary DB key of the procedures table, so it can be used by the worker to obtain the full procname.
Also, reduce GC churn by using folds in the scheduler startup instead of copying lists over and over.
Reviewed By: jberdine
Differential Revision: D23566131
fbshipit-source-id: 1472aa990
Summary:
- freshen up /docs/next/absint-framework to give sensible advice, and
delete outdated bits that are now in the API docs so they remain fresh
- delete SimpleChecker.ml as it's just a source of bitrot
- delete the "adding checkers" page as it's completely outdated and
subsumed by the "AI framework" page + the labs.
Reviewed By: jberdine
Differential Revision: D23597271
fbshipit-source-id: 78b541746
Summary:
We defined cost's plus as "zero+unreachable = unreachable" for the operation cost. The meaning of
the zero cost is that no statment is analyzed yet, and the unreachable(bottom) cost means a program
point is analyzed as unreachable. We thought "zero+unreachable" happens in very specific cases we
need to check, or due to an analyzer bug. For debugging purpose, we defined it to return more
specific unreachable cost.
However, in allocation/autoreleasepool costs, the zero cost is not very special value. If there is
no alloc/autorelease calls, they can have the zero cost. "zero+unreachable = unreachable" doesn't
make sense there.
This diff changes the plus as "zero+unreachable = zero" for the non-operation costs.
Reviewed By: ezgicicek
Differential Revision: D23578869
fbshipit-source-id: 5392eca1c
Summary: This diff adds some tests run with ARC/non-ARC compiled objective-c sources.
Reviewed By: ezgicicek
Differential Revision: D23542135
fbshipit-source-id: 8e089666b
Summary:
This would previously print that we ran out of fuel even if we didn't
and we simply reached a normal form.
Reviewed By: ezgicicek
Differential Revision: D23575571
fbshipit-source-id: 37d02ca8d
Summary:
This diff adds a new experimental checker for detecting size of objects in autorelease pool in ObjC. The basic mechanism is almost the same with the previous cost calculation:
* Autorelease pool size is increased at explicit `autorelease` call
* Autorelease pool size is set as zero by the `autoreleasepool` block.
While it only supports the explicit calls as of now, we will extend the checker to handle more cases in the following diffs.
Reviewed By: ezgicicek
Differential Revision: D23473145
fbshipit-source-id: 416488176
Summary:
This diff extends the cost_item json format to print the autoreleasepool_size field. Not yet, there
is no semantics for that code kind, so the results will always be zero with no traces.
Reviewed By: ezgicicek
Differential Revision: D23540665
fbshipit-source-id: 94442e376
Summary:
Limit communication bandwidth and serialisation burden by sending procedure filename strings (which are bounded at ~100 bytes) instead of serialising procnames through the socket to the scheduler (which are unbounded and have been seen to reach ~30kB in the worst case for templated procedures).
Context:
Under the restart scheduler, a worker working on a procedure X that discovers a race on a dependency Y it needs fails the computation of X and sends to the scheduler the procname Y. The next time X is about to be rescheduled, the scheduler checks whether Y is still being analysed, by checking if the lock for Y still exists. This check uses the procedure filename already, so we can send that instead.
Reviewed By: jvillard
Differential Revision: D23554995
fbshipit-source-id: 9828e71a2
Summary: Most of the time, when the procdesc of a callee is requested, all that is really required is the procedure attributes. However, requesting the procdesc may return `None` when the procedure is undefined (in Java, and soon for Clang too). So, change all callsites to using attributes instead, where possible.
Reviewed By: jvillard
Differential Revision: D23539422
fbshipit-source-id: 3b1a52d48
Summary: Given the brittleness of DB-indexing over marshalled values (one example exposed in D23191601), the serializer "for comparison" must be removed. Its only use is for source files, and these have an obvious, trivial (and possibly faster and less space hungry) protocol.
Reviewed By: jberdine
Differential Revision: D23499481
fbshipit-source-id: 57ad0ced6
Summary: Given the brittleness of DB-indexing over marshalled values (one example exposed in D23191601), the serializer "for comparison" must be removed. Serialized procnames are no longer used as keys, so their serializer can be converted to the one which preserves sharing (saving some space in the process).
Reviewed By: jberdine
Differential Revision: D23425123
fbshipit-source-id: 9c82da778
Summary:
Store model summaries in the `model_specs` database table instead of in spec files.
This table is populated when a new database is created by loading a dump of the `specs` table in the models database. This avoids the perf and reliability implications of ATTACHing the same, non-read-only models-DB by many processes.
- `BiabductionModels` is moved into `IR` so that `JsonReports` can access it.
- The binary `sqlite3` is now required on the host compiling infer.
Reviewed By: skcho
Differential Revision: D23191601
fbshipit-source-id: 1532481ee
Summary: Since the unique string ID used as a key is also human-readable, remove the now-redundant `proc_name_hum` field, which is only used for debug purposes anyway.
Reviewed By: jberdine
Differential Revision: D23446223
fbshipit-source-id: 5027066ee
Summary: There is still a bug in using marshalled values as keys (exposed up the diff stack) where structurally equal procnames get serialised to distinct keys. This diff addresses that bug by using the existing functionality for string unique IDs.
Reviewed By: ezgicicek
Differential Revision: D23133761
fbshipit-source-id: 3cbafb51b
Summary: There is no reason to write back to the database here, as the resulting procdesc is anyway stored in the summary. This is a source of non-determinism.
Reviewed By: skcho
Differential Revision: D23500220
fbshipit-source-id: 7434e6239
Summary: We don't report and IO Cost and are not planning to do so in the near future. Let's remove it from cost kinds.
Reviewed By: ngorogiannis
Differential Revision: D23499160
fbshipit-source-id: 7281da3af
Summary:
As title.
Facebook
Found this case by examining db.
>
D23394545
Time complexity of `_registerTabPreloadables` has **decreased** from `Top` to `O(1)`. Please make sure this is an expected change. You can inspect the trace to understand the complexity increase:
Reviewed By: ezgicicek
Differential Revision: D23448099
fbshipit-source-id: 108fd1ef2
Summary:
This diff adds translation of `dictionaryWithObjects:forKeys:count:`. In the previous implementation it was
translated as if it was `dictionaryWtihObjectsAndKeys:`, but their function parameters are different.
In this diff, it translates an array literal `NSDictionary* a = @ [ @"firstName": @"Foo", @"lastName":@"Bar" ];` to
```
n$1=NSString.stringWithUTF8:(@"firstName")
n$2=NSNumber.stringWithUTF8:(@"Foo")
n$3=NSNumber.stringWithUTF8:(@"lastName")
n$4=NSNumber.stringWithUTF8:(@"Bar")
temp1[0]:objc_object*=n$1
temp1[1]:objc_object*=n$3
temp2[0]:objc_object*=n$2
temp2[1]:objc_object*=n$4
n$3=NSDictionary.dictionaryWithObjects:forKeys:count:(temp2:objc_object* const [2*8], temp1:objc_object*const [2*8], 2:int)
```
where `temp` is an additional local variable declared as array.
See,
https://developer.apple.com/documentation/foundation/nsdictionary/1574184-dictionarywithobjects?language=objchttps://developer.apple.com/documentation/foundation/nsdictionary/1574181-dictionarywithobjectsandkeys
{F316854542}
Reviewed By: skcho
Differential Revision: D23447042
fbshipit-source-id: 14b7c3f2b
Summary: Added a model for copy constructor for `std::function`. In most cases, the SIL instruction `std::function::function(&dest, &src)` gives us pointers to `dest` and `src`, hence, we model the copy constructor as a shallow copy. However, in some cases, e.g. `std::function f = lambda_literal`, SIL instruction contains the closure itself `std::function::function(&dest, (operator(), captured_vars)`, hence, we need to make sure we copy the right value.
Reviewed By: ezgicicek
Differential Revision: D23396568
fbshipit-source-id: 0acb8f6bc
Summary:
Move Sqlite registered statements inside the functions that use them, since these are only ever used in one place.
Also, reformat some SQL.
Also, make `mark_all_source_files_stale` use an un-prepared statement, as it is used at most once per run, wasting resources if registered.
Reviewed By: skcho
Differential Revision: D23423844
fbshipit-source-id: 07362d19c
Summary: We only added suffix-stripped prefixes of props but this causes FPS if a component declares props that actually contain suffixes since we strip them when we are adding builder calls. The fix is to add both normal and stripped versions.
Reviewed By: skcho, Katalune
Differential Revision: D23375405
fbshipit-source-id: e99cb4dd8
Summary:
This diff finishes the migration from the specialization of methods that take blocks as arguments. Here we delete all the old code and change the way we model dispatch functions so that the tests pass.
- Remove the code for specializing the methods in biabduction.
- Remove the call flags `cf_with_block_parameters` that was only used in this algorithm.
- Removes models for dispatch functions.
- Adds models for dispatch functions as program transformation only in biabduction. To be added in other checkers in the future.
Reviewed By: ngorogiannis
Differential Revision: D23345342
fbshipit-source-id: b5e8542ce
Summary:
This preanalysis in general aims to create specialized clones of methods that have blocks as arguments and that are called with concrete closures, and then call these clone methods instead of the original ones.
One complication is what happens with the captured variables in the closure. What we do is we add them to the formals of the cloned method and passed them through to the concrete blocks.
We do this transformation in two steps:
1. Go through all the callers of methods with blocks as parameters, and create the clone methods. In this preanalysis we only create the attributes for the new method, not the code. We also update the call instructions in the callers to represent a call to the cloned method with updated arguments: we don't need to pass closures arguments anymore, we instead pass the captured variables as new arguments.
2. We add the corresponding code to the newly created clones: this means swapping the call to the block variable with a call to the corresponding block. Moreover, we add some of the new formals (that correspond to the captured variables) to the arguments of the call.
This diff implements step 1 of the analysis. The next diff D23216021 implements step 2.
Reviewed By: ngorogiannis
Differential Revision: D23109204
fbshipit-source-id: 91a5eb16b
Summary: There was a mismatch between formals and actuals in `std::function::operator()` because we were not passing the first argument corresponding to the closure.
Reviewed By: ezgicicek
Differential Revision: D23372104
fbshipit-source-id: d0f9b27d6
Summary: When we evaluate lambdas in pulse, we create a closure object with `fake` fields to store captured variables. However, during the function call we were not linking the captured values from the closure object. We address this missing part here.
Reviewed By: jvillard
Differential Revision: D23316750
fbshipit-source-id: 14751aa58
Summary:
Report errors found by running Topl on top of Pulse, when using
--topl-pulse. Topl tests now run on top of Pulse.
Reviewed By: jvillard
Differential Revision: D23030771
fbshipit-source-id: 8770c2902
Summary:
Two issues are fixed
1. For this diff, when the condition `curr_langauge_is Java` is removed in some part of the analysis, some c bufferoverrun tests are broken. This is fixed in this diff by inspecting if we are dealing with a `Size` alias referring to an `objc_internal_collection_array`.
2. Previously, when we are modifying mutable array in a loop, e.g. adding element to the array or removing element from the array, we are unable to give an estimable size of the array after exiting the loop. This is now fixed, and the corresponding FPs are resolved.
Reviewed By: skcho
Differential Revision: D23342350
fbshipit-source-id: 200f5261c
Summary:
This diff fixes `--reanalyze` option that is to reanalyze specific procedures by removing their
summaries. It was broken because it tried to store an empty summary with `Status.Analyzed`.
Reviewed By: ezgicicek
Differential Revision: D23344633
fbshipit-source-id: 1c4eca6c0
Summary:
The generated code used to contain Prune statements that had boolean
connectives in their conditions. After this commit, all conditions
should have no boolean connective (LNot, LOr, LAnd) at top-level; that
is, prune conditions should be atomic.
The main motivation behind this change is that (a) frontends follow this
convention, and (b) Pulse assumes this convention.
Reviewed By: jvillard
Differential Revision: D23022273
fbshipit-source-id: 1313328e4
Summary:
In the previous diffs, we implement enumerator in order to estimate the cost of for-each loop in ObjC, but when we have FP case when enumerator is used not in for-each loop. For example, the following code has top cost before the fix.
```
void nsarray_enumerator_linear_FP(NSArray* array) {
id obj;
NSInteger sum = 0;
NSEnumerator* enumerator = [array objectEnumerator];
while (obj = [enumerator nextObject]) {
sum += (NSInteger)obj;
}
}
```
Reviewed By: skcho
Differential Revision: D23294895
fbshipit-source-id: 50c7b359f
Summary:
When normalizing discovers new linear arithmetic facts in
`normalize_linear_eqs` we go around once more. Do the same when atoms
become linear equalities.
Reviewed By: skcho
Differential Revision: D23264425
fbshipit-source-id: b355875f3
Summary:
Mostly cosmetic except for a change in [solve_eq] to try harder at
normalization (improves unit tests!). Add more comments and do minor
renamings.
Reviewed By: skcho
Differential Revision: D23243629
fbshipit-source-id: 55bdaf8a8
Summary:
This function had become a bit hard to read and the part about embedded
atoms was not very clear and also a bit incomplete (need to handle "= 1"
and "≠ 1" too).
Reviewed By: skcho
Differential Revision: D23242216
fbshipit-source-id: 239fade97
Summary:
This does a bunch of things at once (sorry):
- Refactor atom/term normalisation so that terms that are really just
atoms become atoms.
- Use this to not bother adding special cases in the functions exported
in the .mli: `and_less_than`, `and_equal_binop`, `prune_binop`, etc.
all had special cases to avoid introducing terms that could be atoms.
That's not great because the same smarts wasn't applied to terms that
would only become atom-like after some normalisation, and led to weird
and duplicated code. Now it's much cleaner: just add the most
straighforward fact and normalise!
- Fix a bug: adding a new equality `x = linear` should *not* be done
using `Normalizer.merge_var_linarith` as this is an internal function
that assumes that `x` is the right representative in `x - linear`.
Instead, for abitrary equations of that form, `solve_eq` should be used.
- When `normalize_linear_eqs` discovers new linear equalities, normalize
again. Add fuel there too to avoid spending too much time doing that.
It could be that we don't need/want fuel there but then we'd need to
think very hard about why there's no infinite recursion possible and
that seems harder.
Reviewed By: skcho
Differential Revision: D23241282
fbshipit-source-id: e5b8c4759
Summary:
This is used for variable substitution and will often be a no-op when
normalising terms over and over again (after the first normalisation,
the expression should stay the same). The equivalent function for terms
was already being careful about not re-allocating identical terms so
extend that care to linear expression.
Reviewed By: skcho
Differential Revision: D23241601
fbshipit-source-id: b365eb87a
Summary:
This allows further normalisation now that terms contain linear
expressions in normal form.
Reviewed By: skcho
Differential Revision: D23241499
fbshipit-source-id: f8e4e759c
Summary:
Linear arithmetic is able to simplify more atoms, eg `x+y <= x+y`
becomes `True` by normalising to "lhs - rhs <= 0". This does the first
step of normalisation, but to get True in this example we also need to
substitute inside atoms according to the linear equalities, which is the
next diff (for now we only substitute variables inside atoms for other
variables or for constants).
Reviewed By: skcho
Differential Revision: D23241457
fbshipit-source-id: 0da0b545c
Summary:
More scaffolding, nothing creates `Linear _` terms yet. Some changes to
variables substitution to allow substituting variables for linear terms
(as well as constants and other variables).
Reviewed By: skcho
Differential Revision: D23241461
fbshipit-source-id: fc870255e
Summary:
This is needed for the rest of the stack that introduces a `Linear of
LinArith.t` variant in `Term.t` to enable more normalisation inside of
terms.
Reviewed By: skcho
Differential Revision: D23241353
fbshipit-source-id: ad765cd13
Summary:
Make term simplification a bit more structured and separate the
"simplification" phase from the "evaluating constant expressions" phase.
Also implement the latter for all possible terms.
Reviewed By: skcho
Differential Revision: D23241334
fbshipit-source-id: 2964aa477
Summary: Not much to see here, extracted to make further changes more readable.
Reviewed By: da319
Differential Revision: D23241335
fbshipit-source-id: 81181f23a
Summary:
`delete` works exactly like `free` so merge both models together. Also
move the `free(0)` test to nullptr.cpp as it seems more appropriate.
Reviewed By: da319
Differential Revision: D23241297
fbshipit-source-id: 20a32ac54
Summary:
Since this is where almost all of the reasoning is concentrated, let's
make sure we use it at every opportunity!
Reviewed By: skcho
Differential Revision: D23194224
fbshipit-source-id: fedb2811e
Summary:
Fix the FP when iterating through constant collection.
facebook
This fix is a hack for now.
Reviewed By: ezgicicek, skcho
Differential Revision: D23241338
fbshipit-source-id: e2e0c05f8
Summary:
As title.
This diff is co-authored by SungKeun Cho and me.
facebook
This diff is co-authored by skcho and me.
Original comments from skcho
"For the record:
1. Rory and I tried to write models for ObjC iterator.
2. We could not use Java's iterator semantics: In Java's, `hasNext` returns the size of collection, rather than a boolean, and which is used as a control variable. On the other hand, in ObjC, it calls only `nextObject`, not calling `hasNext`, and the return value of which is being checked as `null`.
3. We added an artificial field `objc_iterator_offset` to keep the index of the iterator, and the models added in this diff are handling that integer value.
A problem is that `array.objc_iterator_offset` is not included in the control variables, since the condition of the loop is `nextObject() != null` that does not include the iterator offset. We need to make `array.objc_iterator_offset` as a control variable, by changing the part collecting control variables.
"
Reviewed By: ezgicicek, skcho
Differential Revision: D22944278
fbshipit-source-id: 7e71b79c1
Summary:
`Obj.reachable_words` can be very slow on large values, so only call it in debug mode.
Also, measure the time we spend for compressing/storing the global type environment.
Reviewed By: jvillard
Differential Revision: D23264532
fbshipit-source-id: 4a9456ab7
Summary: Use `SqliteUtils.exec` where appropriate, reformat some queries for readability.
Reviewed By: ezgicicek
Differential Revision: D23240945
fbshipit-source-id: 24d921a3a
Summary:
Reset the state before each test so that adding tests doesn't affect
other tests by shifting the ids of their anonymous variables.
Reviewed By: skcho
Differential Revision: D23194171
fbshipit-source-id: 7b717f160
Summary:
Before: 3 modes: (where "lenient" build has warnings not crash the
build, while "strict" build errors on warning):
- opt (default): flambda optimisations + lenient build
- dev (recommand for dev): lenient build, no flambda
- test: strict build (used in tests), no flambda
Now:
- dev (default): *strict* build, no flambda
- opt: lenient build, flambda
- dev-noerror: lenient build, no flambda (use when you want to test
infer but there are build warnings)
The goal is to give faster feedback to infer developers and reduce the
amount of times diffs are sent with build warnings. Also it's now faster
to alternate between changing infer and running unit tests since test
mode is just dev mode.
Reviewed By: ngorogiannis
Differential Revision: D23167416
fbshipit-source-id: d663b6054
Summary: Moving specs to the DB missed out cleaning out all specs when reanalysing. This is the fix.
Reviewed By: jvillard
Differential Revision: D23188958
fbshipit-source-id: 5b50fdda8
Summary:
These are the only ones we need, it turns out the other types (string,
proc names, ...) were dead code. The changes the integer constants to
rational constants, to match the domain of the linear arithmetic engine.
Reviewed By: skcho
Differential Revision: D23164136
fbshipit-source-id: 755c3f526
Summary: In the frontend captured variables for blocks are added as formal parameters in procdesc at the beginning.
Reviewed By: dulmarod
Differential Revision: D23163619
fbshipit-source-id: 2bcbe9b9c
Summary:
There was a syntax error in the comment as `[code]` is interpreted as
code but backticks were used instead. This made `ocamlformat` produce a
warning but no error.
Reviewed By: skcho
Differential Revision: D23167273
fbshipit-source-id: a7fad10d5
Summary:
Instead of alternating between a normal form and a tree structure,
always keep a normal form. Except the normal form is not always fully
normalized. Overall, it's a bit faster than the previous iteration,
while being more precise! In particular, linear arithmetic aims at being
much more complete.
Reviewed By: skcho
Differential Revision: D23134209
fbshipit-source-id: 5f9ec6ece
Summary:
When implementing iterator, we find out that because some semantics of inferbo is Java-specific, we cannot simply use Java's `Collection` model for `NSCollection`.
So this diff writing `NSCollection` model separately.
This diff also extracts the common parts of `NSCollection` and `Collection` into `AbstractCollection` to combine the duplicate the parts.
Reviewed By: ezgicicek
Differential Revision: D22975159
fbshipit-source-id: daed3f99f
Summary:
We already take into account inheritance if the method inherits a known
modelled initializer method (e.g. Activity.onCreate()).
But if the method is explicitly marked as Initializer, we require its
overrides to be also marked.
This diffs fixes the behavior and makes it consistent, now this is
enough to annotate only parent class.
Reviewed By: jvillard
Differential Revision: D23135177
fbshipit-source-id: a21ff4a0e
Summary:
This is part of work aimed to reduce usage of language-agnostics modules
in Java-specific parts of nullsafe.
Reviewed By: ngorogiannis
Differential Revision: D23075333
fbshipit-source-id: 4029732b4
Summary:
This is one of two files in nullsafe that remains interface-less.
Let's fix it!
Reviewed By: jvillard
Differential Revision: D23056324
fbshipit-source-id: a6592f7ae
Summary: Before we were modelling `vector.end()` as returning a fresh pointer every time is was called. It is common to check if an iterator is not the `end()` iterator and proceed to dereference the iterator in that case. In such code pattern `vector.end()` is called twice and returns different fresh values which causes false positives. To fix this, we add a special internal field `__infer_model_backing_array_pointer_to_last_element` to a vector to denote its end. Now, every time we call `vector.end()` we return the value of this field. We introduce a new attribute `EndOfCollection` to mark `end` iterator as the existing `EndIterator` invalidation is not suitable when we need to read the same value multiple times.
Reviewed By: jvillard
Differential Revision: D23101185
fbshipit-source-id: fa8a33b58
Summary:
Constructing the report is done by reading all the summaries, and using certain parts thereof. However, the payloads, which typically account for the greatest size, are not used (with the exception of costs).
This diff splits the storage of summaries into analysis and report summaries, and only reads and deserialises the latter for the report phase. This makes a big difference for runs with a large number of procedures.
Reviewed By: jvillard
Differential Revision: D23105072
fbshipit-source-id: 359067a0f
Summary:
As preparation for splitting summaries into some of their components, and then iterating over only those when reporting (thus gaining performance) we need procnames in the table.
Also, this fixes the now-broken use case of `infer report` with spec files, by using `--procedures-filter` to restrict printing of summaries accordingly.
Reviewed By: skcho
Differential Revision: D23101853
fbshipit-source-id: 1ae878d8e
Summary: Implement specs storage in DB, apart from biabduction models which are still left in specs files.
Reviewed By: skcho
Differential Revision: D22795638
fbshipit-source-id: 140801d3f
Summary: Extra info helps in debugging frontend issues and such.
Reviewed By: ngorogiannis
Differential Revision: D23101854
fbshipit-source-id: 27024675d
Summary:
At the end of analysing a procedure we call `simplify
~keep:vars_live_in_pre_post`. Any variable not in
`vars_live_in_pre_post` is not mentioned anywhere else in the state and
therefore is not going to contribute constraints in callers of the
procedure (in other words: they're dead). We want to also forget
arithmetic facts about these variables as this is a good opportunity to
make the path condition smaller, sometimes by a lot!
The main issue is that dead variables may be useful intermediate terms
in the formula, eg trying to keep only facts about `x` in `y = x + 1 &&
y = 0` is going to lose a lot of precision. But, if a variable not in
`keep` is only mentioned in a simple atom `z = 42` atom, for example,
it's safe to forget about it, eg it's safe to remember only `x=0` in
`x=0 && z=42` (if only `x` is live).
In other words, we can get rid of all atoms containing variables not
transitively involved in other atoms that eventually involve live
variables. A graph problem! This is guaranteed not to forget anything
important and can still trim a lot of atoms in certain situations.
Reviewed By: skcho
Differential Revision: D22921313
fbshipit-source-id: 6d5db7cbe
Summary:
Perhaps a bit overkill to introduce all this extra complexity but it
makes the unit tests much more readable. In fact, this uncovered a bug
in the dead variable elimination!
Reviewed By: dulmarod
Differential Revision: D22925548
fbshipit-source-id: d1f411683
Summary:
Do not always add parens around sub-terms, and add more parens around
terms in atoms and normal forms when they can be confused with the atom
or normal form structure.
Reviewed By: skcho
Differential Revision: D22925549
fbshipit-source-id: 8646e96a5
Summary: These will change to more interesting outputs in the next diff.
Reviewed By: dulmarod
Differential Revision: D22921349
fbshipit-source-id: c58c6240a
Summary:
Add unit tests to pulse in order to write tests for the arithmetic
solver, because it is a pain to write programs to do that end to end.
Reviewed By: ezgicicek
Differential Revision: D22864607
fbshipit-source-id: 0a20a3593
Summary:
This is needed to make dune auto-updating of unit tests introduced in
the next diff cohabit peacefully with our tests to make sure code stays
correctly formatted wrt ocamlformat.
Also, more auto-formatting = better.
Reviewed By: da319
Differential Revision: D22865004
fbshipit-source-id: 91c47ab08
Summary:
Normalization is potentially expensive and its result should be
remembered if the formula keeps being used. In the future we might use
this to make normalization more incremental.
Also rename PathCondition.satisfiable -> is_unsat to match
PulseFormula.is_unsat.
Reviewed By: skcho
Differential Revision: D22728264
fbshipit-source-id: 7759b33ac
Josh Berdine
Mitya Lyubarskiy
Ezgi Çiçek
Nikos Gorogiannis
Sungkeun Cho
Jules Villard
Qianyi Shu
Daiva Naudziuniene
Dulma Churchill
Radu Grigore
Artem Pianykh