Summary:
I hear that this scheduler is better. I want the best scheduler
possible. Also pulse's join is a bit complex so it might matter one day.
whydididothis
Reviewed By: mbouaziz
Differential Revision: D12958131
fbshipit-source-id: 3bd77ccba
Summary:
This may help running the id map bookkeeping on its own in the future
and makes the code slightly more readable in my opinion.
Reviewed By: mbouaziz
Differential Revision: D12858066
fbshipit-source-id: fea4aea63
Summary:
HIL wanted to do its own HTML printing, causing code duplication and hacks to
avoid double opening/closing files. Instead, pass a hook to print SIL
instructions or not.
This also makes the debug HTML be printed even in case of raised exceptions,
which is invaluable to debug crashes or even just reports in the case of
checkers that can raise `Stop_analysis` (pulse only for now).
This also print intermediate abstract states between instructions instead of
only at the start and end of nodes, for moar debugging.
Reviewed By: mbouaziz
Differential Revision: D12857425
fbshipit-source-id: 4ee6c88d6
Summary: Make the whole type private, introduce constructors for each variant, and deal with the consequences.
Reviewed By: da319
Differential Revision: D12825810
fbshipit-source-id: a01922812
Summary:
Having the `Node` module including in the `CFG` one is confusing.
Let's keep it separate.
Reviewed By: ngorogiannis
Differential Revision: D8185754
fbshipit-source-id: 62077e6
Summary:
Change the license of the source code from BSD + PATENTS to MIT.
Change `checkCopyright` to reflect the new license and learn some new file
types.
Generated with:
```
git grep BSD | xargs -n 1 ./scripts/checkCopyright -i
```
Reviewed By: jeremydubreil, mbouaziz, jberdine
Differential Revision: D8071249
fbshipit-source-id: 97ca23a
Summary:
Upgrade ocamlformat, and base which needs to be done in sync in order to build
ocamlformat, and the other deps can come for the ride.
Reviewed By: jvillard
Differential Revision: D7663537
fbshipit-source-id: 3e90970
Summary:
Now that everything can run at the same time and we have preanalyses, it can be quite hard to read debug sessions.
Here come session names!
Depends on D7607336
Reviewed By: sblackshear
Differential Revision: D7607481
fbshipit-source-id: 676af86
Summary: More preparation for extending HIL with dereference and address of. We need left hand side of the assignment to also include dereference and address of.
Reviewed By: sblackshear
Differential Revision: D6976150
fbshipit-source-id: 47d1d76
Summary: Preparing to extend HIL with Dereference and AddressOf expressions. Next steps: (1) change SIL -> HIL translation to preserve address of and dereference; (2) adapt analyses based on HIL to make use access expressions.
Reviewed By: jeremydubreil
Differential Revision: D6961928
fbshipit-source-id: 51da919
Summary:
Upgrade ocamlformat to 0.3, and (necessarily) base to v0.10.0.
- Fix accumulated mis-formatting
- Update opam.lock to unbreak clean build
- Update to base v0.10.0
- Update opam.lock for base
- Update offline opam repo
- Everyone should already have removed their ocamlformat pin
- ocamlformat 0.3 supports output to stdout natively
- bump version of ocamlformat
Reviewed By: jeremydubreil
Differential Revision: D6636741
fbshipit-source-id: 41a56a8
Summary:
It seems that the abstraction instructions were not previously added the the CFG.
This is a functional changes to make sure that the abstraction state is always added. We can simplify the code later and just run this step before storing the CFG instead of after loading them.
Reviewed By: sblackshear, jvillard
Differential Revision: D6383672
fbshipit-source-id: cedcb8a
Summary:
Change ocamlformat installation procedure to use opam instead of
pinning.
Reformat all code with v0.2, which has a few improvements.
Reviewed By: jvillard
Differential Revision: D6292057
fbshipit-source-id: 759967f
Summary: More general version of the fix in D6138749. This diff moves RacerD's lock modeling into a separate module and uses the module in the HIL translation to check when a function has lock/unlock semantics.
Reviewed By: jberdine, da319
Differential Revision: D6191886
fbshipit-source-id: 6e1fdc3
Summary:
If you write
```
boolean readUnderLockOk() {
synchronized (mLock) {
return mField;
}
}
```
it will be turned into
```
lock()
irvar0 = mField
unlock()
return irvar0
```
in the bytecode. Since HIL eliminates reads/writes to temporaries, it will make the above code appear to perform a read of `mField` outside of the lock.
This diff fixes the problem by forcing HIL to perform all pending reads/writes before you exit a critical section.
Reviewed By: jberdine
Differential Revision: D6138749
fbshipit-source-id: e8ad9a0
Summary:
Before this change, analyses using HIL needed to pass `IdAcessPathMapDomain.empty` to abstract interpreter, and would get back the map as part of the post.
This is a confusing API and was a pain point for Dino in trying to use HIL.
This diff adds a HIL wrapper around the abstract interpreter that hides these details.
It replaces `LowerHIL.makeDefault` as the new "simplest possible way" to use HIL.
Reviewed By: jberdine
Differential Revision: D6125597
fbshipit-source-id: 560856b
Summary:
Install ocamlformat from github as part of `make devsetup`, and use it
for formatting OCaml (and jbuild) code.
Reviewed By: jvillard
Differential Revision: D6092464
fbshipit-source-id: 4ba0845
Summary:
Record the list of access paths (if any) used in the index expression for each array access.
This will make it possible to use array accesses as sinks in Quandary
Reviewed By: jeremydubreil
Differential Revision: D5531356
fbshipit-source-id: 8204909
Summary:
Conversion and reformat of infer source using ocamlformat
auto-formatting tool.
Current status:
- Because Reason does not handle docstrings, the output of the
conversion is not 'Warning 50'-clean, meaning that there are
docstrings with ambiguous placement. I'll need to manually fix
them just before landing.
Reviewed By: jvillard
Differential Revision: D5225546
fbshipit-source-id: 3bd2786
Nikos Gorogiannis
Jules Villard
Mehdi Bouaziz
Josh Berdine
Daiva Naudziuniene
Sam Blackshear
Jeremy Dubreil