Summary:
Computing sledge's equality relation and normalising terms is costly. We
can avoid doing that most of the time by keeping the sledge path
condition lazily evaluated and only forcing it down to a value at two
critical points in the analysis:
1. Summary creation, to avoid storing unsatisfiable pre/posts that will have
to be needlessly executed by callers. This also saves us from having
to serialise the closures involved in the uncomputed form of lazy
values inside the pulse summaries.
2. Before reporting errors we check in the state is in fact satisfiable.
If not we just prune it away at that point.
This yields ~4x speedup on some targets.
Reviewed By: ezgicicek
Differential Revision: D21129759
fbshipit-source-id: a75fdd3bc
Summary:
This is mostly just a type change for now, more changes to come. This
doesn't make thing much faster yet because we force computations pretty
often to check for unsatisfiability (each function call and PRUNE node).
Next diff will build on that.
Reviewed By: skcho
Differential Revision: D21129758
fbshipit-source-id: 72200e2b1
Summary:
When encountering a constant, pulse creates an abstract value (a
variable) to represent it, and remembers that it's equal to it. The
problem is that pulse doesn't yet know how to deal with the fact that
some variables are going to be equal to each other.
This hacks around this issue in the case of constants, within the same
procedure, by remembering which constants have been assigned to which
place-holder variables, and serving those variables again when the same
constant is translated again.
Limitation: this doesn't work across procedure calls as the "constant
maps" are not saved in summaries.
Something to look out for: we don't want to make `if (p == NULL)` create
a path where `p` is invalid (we only make null invalid when we see an
assignment from 0, i.e. `p = NULL;`).
Reviewed By: ezgicicek
Differential Revision: D21089961
fbshipit-source-id: 5ebb85d0a
Summary:
1. Package will make the error too verbose.
2. We don't even need to say it is "class" because we say it in the error
description ("Class has 0 issues and can be marked Nullsafe").
Reviewed By: artempyanykh
Differential Revision: D21131998
fbshipit-source-id: 6ccca7615
Summary:
One source of false positives on container races is when the container member field is initialised to a concurrent version in a constructor, but the static type of the field doesn't reflect the thread safety of it.
This solution
- tracks flows from constructors of safe data structures to abstract addresses;
- initialises the initial attribute state when analysing a non-constructor method to that achieved by all constructors/class-initializers.
- checks for that attribute when recording container accesses.
Reviewed By: jvillard
Differential Revision: D21089428
fbshipit-source-id: 02a88f6e8
Summary:
As artempyanykh pointed out, `nullable` works much better for required fields
than `optional` in terms of x-plat.
Reviewed By: artempyanykh
Differential Revision: D21129614
fbshipit-source-id: b03c91b78
Summary: Modeling vector iterator with two internal fields: an internal array and an internal pointer. The internal array field points to the internal array field of a vector; the internal pointer field represents the current element of the array. For now `operator++` creates a fresh element inside the array.
Reviewed By: ezgicicek
Differential Revision: D21043304
fbshipit-source-id: db3be49ce
Summary:
The java source file parser should refuse to run on non
.java file. Also, as we expect some autogenerated source files to
break Java official syntax, we catch parsing error silently and
cancel location recording for them.
Reviewed By: jvillard
Differential Revision: D21089587
fbshipit-source-id: 35f1a1e28
Summary:
Now that only races rooted at formals or globals are reported, there is no point using the ownership domain to exclude accesses to locals, so remove the code that initialises the ownership of those.
Also, remove an accidentally quadratic use of `Map.bindings |> List.find` in `FormalMap` and simplify the analysis driver.
Reviewed By: skcho
Differential Revision: D21066855
fbshipit-source-id: 126080778
Summary:
Add a path condition to each symbolic state, represented in sledge's arithmetic domain. This gives a precise account of arithmetic constraints. In particular, it is relation and thus is more robust in the face of inter-procedural analysis.
This is gated behind a flag for now as there are performance issues with the new arithmetic.
Reviewed By: jberdine
Differential Revision: D20393947
fbshipit-source-id: b780de22a
Summary: Move state to summary conversion into the domain file, move a model matcher into the models file and simplify.
Reviewed By: skcho
Differential Revision: D21064351
fbshipit-source-id: bb5b07b6b
Summary:
There are two types of anonymous classes (not user defined classes):
- classic anonymous classes (defined as $<int> suffixes)
- lambda classes (corresponding to lambda expressions). Experimentally,
they all have form `$Lambda$_<int>_<int>`, but the code just uses
`$Lambda$` as a heuristic so it is potentially more robust.
# Problem this diff solves
When generate meta-issues for nullsafe, we are interested only in
user-defined classes, so we merge all nested anonymous stuff to
corresponding user-defined classes and hence aggregate the issues.
Without this diff, for each lambda in the code, we would report this as
a separate meta-issue, which would both screw up stats and be confusing
for the user (when we start reporting mode promo suggestions!).
Reviewed By: artempyanykh
Differential Revision: D21042928
fbshipit-source-id: a7be266af
Summary: In `PowLoc`, we focus on making every constructors of `PowLoc.t` return nomalized value. Thus, it is unnecessary to nomalize any `PowLoc.t` inputs.
Reviewed By: ezgicicek
Differential Revision: D21064893
fbshipit-source-id: d00a7f06b
Summary:
This diff revises how to handle the unknown location in inferbo in two ways:
* stop appending field to the `Unknown` location, e.g. `Unknown.x.a` is evaluated to `Unknown`
* redesign the abstract of multiple locations, like `Bottom` < `Unknown` < `Known` locations
I am doing them in one diff since applying only one of them showed bad results.
Background: `Unknown` was adopted for abstracting all unknown concrete locations, so we could avoid missing semantics of assignments to unknown locations. We tried to keep soundness. However, it brought some other problems related to precision and performance.
1. Sometimes especially when Inferbo failed to reason precise pointer values, `Unknown` may point to many other abstract locations.
2. At that time, value assignments to `*Unknown` makes the situation worse: many abstract locations are updated with imprecise values.
This problem harmed not only its precision, but also its performance since it introduced more location entries in the abstract memory.
Reviewed By: jvillard
Differential Revision: D21017789
fbshipit-source-id: 0bb6bd8b5
Summary: The flags `--biabduction-fallback-model-alloc-pattern` and `--biabduction-fallback-model-free-pattern` were unused because we removed the models from .inferconfig a while ago because of too many false positives. We are implementing a better memory leak check based on Pulse, and are adding the similar flags `--pulse-model-alloc-pattern` and `--pulse-model-free-pattern`.
Reviewed By: jvillard
Differential Revision: D21061511
fbshipit-source-id: 1b3476c22
Summary:
Instead of having to remember to update both the inferbo and the concrete
intervals domains of pulse, hide these details under a unified API. This
should help the transition to adding a third(!) numerical domain later
on (pudge!).
Reviewed By: ezgicicek
Differential Revision: D21022920
fbshipit-source-id: 783157464
Summary:
Now that the shape of the record type of AbductiveDomain.t is known, we
don't need this getter anymore. Keep `get_pre` and `get_post` as they
perform useful casting to `BaseDomain.t`.
Reviewed By: ezgicicek
Differential Revision: D21022924
fbshipit-source-id: 340f4edf8
Summary:
The "interface" modules define short forms for the internals of pulse
and also serve as a guide of which modules you are supposed to use at
which "level" in the pulse domains (base domain vs abductive domain vs
higher-level PulseOperations.ml). Make sure they are used.
Reviewed By: skcho
Differential Revision: D21022927
fbshipit-source-id: f890df245
Summary:
PulseAbductiveDomain.ml can be split into two distinct parts:
1. The definition of the "abductive domain" itself. This remains in that
file.
2. How to apply a given pre/post pair to the current state (during a
function call). This is about the same size as 1. in terms of lines
of code(!) and is now in PulseInterproc.ml.
Reviewed By: ezgicicek
Differential Revision: D21022921
fbshipit-source-id: 431fe061e
Summary:
I'm moving this code in the next diff and need this refactor. It should
be the same as before.
Reviewed By: ezgicicek
Differential Revision: D21022926
fbshipit-source-id: ebe644ef9
Summary:
See the code comment re: why don't we also recommend "strict" at this
stage. We can always change it later when we think users are happy with
strict.
Reviewed By: artempyanykh
Differential Revision: D21039553
fbshipit-source-id: 758ccf32c
Summary:
Having copypaste is painful to support. Lets make .mli the source of
truth.
Improved docs a bit, while I was here.
Reviewed By: artempyanykh
Differential Revision: D20948916
fbshipit-source-id: 1668dbc9c
Summary:
This diff is a step forward to the state when the list of type violations is
independent of the mode (and we use mode solely to decide re: whether to
report or not).
This fixes a case when we incorrectly defined possible promo mode (see
the test payload)
Reviewed By: artempyanykh
Differential Revision: D20948897
fbshipit-source-id: 616b96f96
Summary:
See the comments in the code why it makes logical sense.
This diff is a step forward the state when list of type violations is
independent of the mode (and we use mode solely to decide re: whether to
report or not).
This fixes majority of cases in ModePromotions.java
Reviewed By: artempyanykh
Differential Revision: D20948656
fbshipit-source-id: 82c0d530b
Summary:
Currently we exlude only if the method is based on deprecated config
packages.
Lets use the proper method, which covers both cases (config +
user-defined third party repo).
Reviewed By: artempyanykh
Differential Revision: D20946506
fbshipit-source-id: c3332667f
Summary:
Previously, we learned to detect if Default mode class can be made
Nullsafe(LOCAL).
Lets generalize it and calculate the precise mode.
NOTE 1: We don't distinct shades of "Trust some". We also don't
recommend trust some and recommend "Trust all" instead.
NOTE 2: As you can see from the test payload (see ModePromotions.java),
the precise calculation is not working as expected. This is due to a bug
in nullsafe implementation/design. See follow up diffs that will fix
this test.
Reviewed By: artempyanykh
Differential Revision: D20941345
fbshipit-source-id: 2255359ba
Summary:
The full inventory of everything in infer-out/. The main change is
around "issues directories": instead of registering them dynamically
they are now all declared statically (well, they kind of were already in
Config.ml).
Reviewed By: ngorogiannis
Differential Revision: D20894305
fbshipit-source-id: 1a06ec09d
Summary:
This is another entry in infer-out/, we want these to be predictable,
not user-defined.
Reviewed By: dulmarod
Differential Revision: D20894302
fbshipit-source-id: ee60ddbcf
Summary:
This is an entry in infer-out/, we want these to be predictable, not
user-defined.
Reviewed By: ngorogiannis
Differential Revision: D20894307
fbshipit-source-id: 332f85969
Summary:
This option allowed one to customise the name of the log file, but the
log file lives in infer-out/ so that flexibility is not needed and even
undesirable: we want entries in infer-out/ to be predictable.
Reviewed By: skcho
Differential Revision: D20894304
fbshipit-source-id: 760d91df3
Summary: Another entry to practice adding entries to ResultsDirEntryName.
Reviewed By: skcho
Differential Revision: D20894299
fbshipit-source-id: 9c387e0f3
Summary:
First real step to keep an inventory of all the entries in infer-out/ in
a single place, and associate meta-data to each entry. In particular, we
want to avoid adding things in infer-out/ without a clear idea of
whether they should be cleaned up before going into a cache, or before
an incremental analysis.
Migrate infer-out/tmp/ first just as an example and an excuse to write
the scaffolding code needed for all the other entries.
Reviewed By: skcho
Differential Revision: D20894300
fbshipit-source-id: f796fca55
Summary:
The only accurate entry it contains is the number of files analysed and
we can already get that information from the log file (and console
output).
Reviewed By: dulmarod
Differential Revision: D20894303
fbshipit-source-id: bc180015a
Summary: Needed for later: RunState needs to run files in ResultsDir.
Reviewed By: skcho
Differential Revision: D20894306
fbshipit-source-id: 259b7da69
Summary:
I wanted to change the order in which we try loading them but it changes
analysis results too much for the cost analysis.
Reviewed By: skcho
Differential Revision: D20891172
fbshipit-source-id: f972f314e
Summary:
Simplifies the models story. The model jar is still needed to look up
fields in modelled classes (we save the .class of each model!). This is
sad as we should be able to get these from the models' tenv, which
should be more compact, but that's a bigger change.
Reviewed By: skcho
Differential Revision: D20891117
fbshipit-source-id: fcb5104ae
Summary:
Parsing the standard output of buck is brittle. Instead, use the `--build-report` option, which generates a json file, with a mapping from target name to output path. This already contains all the information required.
This diff adapts the buck-java integration.
Reviewed By: artempyanykh
Differential Revision: D20942858
fbshipit-source-id: faf3f2078
Summary: Unify the models of malloc and for the Create and Copy functions for Core Graphics. This add the null case from the malloc model to the Core Graphics models.
Reviewed By: jvillard
Differential Revision: D20890956
fbshipit-source-id: 278ac9d2f
Summary:
- Open-source stubs are in a library with no dependencies
- That library is included in InferBase, but in facebook builds it
contains no modules
Reviewed By: ezgicicek
Differential Revision: D20922574
fbshipit-source-id: af918a687
Summary:
As soon as pulse detects an error, it completely stops the analysis and loses the state where the error occurred. This makes it difficult to debug and understand the state the program failed. Moreover, other analyses that might build on pulse (e.g. impurity), cannot access the error state.
This diff aims to restore and display the state at the time of the error in `PulseExecutionState` along with the diagnostic by extending it as follows:
```
type exec_state =
| represents the state at the program point that caused an error *)
```
As a result, since we don't immediately stop the analysis as soon as we find an error, we detect both errors in conditional branches simultaneously (see test result changes for examples).
NOTE: We need to extend `PulseOperations.access_result` to keep track of the failed state as follows:
```
type 'a access_result = ('a, Diagnostic.t * t [denoting the exit state] ) result
```
Reviewed By: jvillard
Differential Revision: D20918920
fbshipit-source-id: 432ac68d6
Summary: Consider functions that simply exit as impure by extending the impurity domain with `AbstractDomain.BooleanOr` that signifies whether the program exited.
Reviewed By: skcho
Differential Revision: D20941628
fbshipit-source-id: 19bc90e66
Summary: The pruning location of array size was dummy. This diff gives a right location to traces in the pruning.
Reviewed By: ezgicicek
Differential Revision: D20915167
fbshipit-source-id: 55cc583df
Summary:
Instead of looking up each proc name in models/, pre-compute the list of
models and do lookups there instead of in the filesystem.
Reviewed By: ngorogiannis
Differential Revision: D16603148
fbshipit-source-id: 5eb534a14
Summary:
Java bytecode format does not record the declarations location
for classes and fields. We set up a first infrastructure to recover this
information. Currently we only track location for classes and only gives
the first line of the corresponding source file. We will enhance this location
with source file (baby) parsing in a next diff.
Reviewed By: mityal
Differential Revision: D20868187
fbshipit-source-id: d355475e9
Summary:
This information can be useful for tooling responsible for further
processing (e.g. metric calculation and logging)
Reviewed By: artempyanykh
Differential Revision: D20914583
fbshipit-source-id: 61804d88f
Summary: The heuristics is to find a method in non-abstract sub-classes. See D20647101.
Reviewed By: jvillard
Differential Revision: D20491461
fbshipit-source-id: 759713ef4
Summary:
This diff distinguishes array declaration and size-setting in trace. For example, when there is an
assume statement on an array size, the array size can be pruned to another value. In which case, we
want to see "Set array size" in the trace, instead of "Array declaration".
Reviewed By: jvillard
Differential Revision: D20914930
fbshipit-source-id: 0253fb69e
Summary:
This diff lifts the `PulseAbductiveDomain.t` in `PulseExecutionState` by tracking whether the program continues the analysis normally or exits unusually (e.g. by calling `exit` or `throw`):
```
type exec_state =
| ContinueProgram of PulseAbductiveDomain.t (** represents the state at the program point *)
| ExitProgram of PulseAbductiveDomain.t
(** represents the state originating at exit/divergence. *)
```
Now, Pulse's actual domain is tracked by `PulseExecutionState` and as soon as we try to analyze an instruction at `ExitProgram`, we simply return its state.
The aim is to recover the state at the time of the exit, rather than simply ignoring them (i.e. returning empty disjuncts). This allows us to get rid of some FNs that we were not able to detect before. Moreover, it also allows the impurity analysis to be more precise since we will know how the state changed up to exit.
TODO:
- Impurity analysis needs to be improved to consider functions that simply exit as impure.
- The next goal is to handle error state similarly so that when pulse finds an error, we recover the state at the error location (and potentially continue to analyze?).
Disclaimer: currently, we handle throw statements like exit (as was the case before). However, this is not correct. Ideally, control flow from throw nodes follows catch nodes rather than exiting the program entirely.
Reviewed By: jvillard
Differential Revision: D20791747
fbshipit-source-id: df9e5445a
Summary:
Malloc returns either an allocated object or a null pointer if there is no memory available. Modelling that.
This has always been a bit contentious because this leads to NPEs that people often ignores because they don't care. But if we don't model this, then we have FPs when people do take this into account when freeing the memory.
Reviewed By: jvillard
Differential Revision: D20791692
fbshipit-source-id: 6fd259f12
Summary:
infer-out/tmp/ should be deleted before sending infer-out/ to any cache.
Also separate the list of directories to delete in `delete_capture_and_results_data` and in `scrub_for_caching` as it was only confusing to try to share them.
Reviewed By: ngorogiannis
Differential Revision: D20772512
fbshipit-source-id: b1e4e252c
Summary: This makes it similar to the other dir names in infer-out/.
Reviewed By: ngorogiannis
Differential Revision: D20795359
fbshipit-source-id: 88729d26d
Summary:
This diff limits the depth of abstract location by a constant.
problem: Inferbo generated too many of abstract locations, especially when struct types had many pointer fields and Inferbo was not able to analyze the objects precisely. Since the number of generated abstract locations were exponential to the number of fields, it resulted in OOM in the end.
(reported by zyh1121 in https://github.com/facebook/infer/issues/1246)
Reviewed By: jvillard
Differential Revision: D20818471
fbshipit-source-id: f8af27e5c
Summary:
Currenlty the cost issue is printed at the first node of a function, which is usually the first
statment of the function. This may give a wrong impression that the cost of the statement is
changed.
This diff re-locate where to print issues with heuristics. Going backward from the first node
lines, it looks up a line satisfying,
1. A line should start with <fname> or should include " <fname>".
2. The <fname> found in 1 should be followed by a space, '<', '(', or end of line.
Reviewed By: jvillard
Differential Revision: D20766876
fbshipit-source-id: b4fee3180
Summary:
It's easy to create large arrays in code, eg `int x[1UL << 16];`, but
these can generate huge nodes in SIL because zero-initialization is
translated by zero-ing structures element by element. Introduce a
builtin to use instead. Keep the naive method for small structures (with
a configurable limit on "small").
Reviewed By: dulmarod
Differential Revision: D20836836
fbshipit-source-id: 6bf5410f8
Summary: Modelling `CG.*Release ` and `CFRelease` as `free`. This is what we were doing in biabduction.
Reviewed By: skcho
Differential Revision: D20767174
fbshipit-source-id: c77c1cdc6
Summary:
This models all the Create and Copy functions from CoreGraphics, examples in the tests.
These functions all allocate memory that needs to be manually released.
The modelling of the release functions will happen in a following diff. Until then, we have some false positives in the tests.
This check is currently in biabduction, and we aim to move it to Pulse.
Reviewed By: jvillard
Differential Revision: D20626395
fbshipit-source-id: b39eae2d9
Summary: Sometimes buck hangs with the new integration and using pipes. Use a temp file for standard output and redirect stderr.
Reviewed By: jvillard
Differential Revision: D20856346
fbshipit-source-id: 13a5f90d5
Summary:
Fix all the docstrings that `odoc` or `ocamlformat` is not happy about.
Delete all `[@@ocamlformat "parse-docstring = false"]` pragmas as a
result.
Reviewed By: jberdine, ngorogiannis
Differential Revision: D20798913
fbshipit-source-id: 728d9e45c
Summary:
All dune libraries in infer/src/ were declared with their own public
names, each one needing its own .opam file. There's no need for that:
they can all be part of the `infer` library by calling them `infer.Foo`.
One wrinkle: now we need to explicitly point at their .mld files in the
generated documentation.
Reviewed By: jberdine
Differential Revision: D20798914
fbshipit-source-id: 64b64261c
Summary:
This avoids dune scanning 2000+ directories (according to its logs),
mostly due to scanning infer/tests/ I think.
Reviewed By: artempyanykh
Differential Revision: D20798915
fbshipit-source-id: 3764cd3fb
Summary:
- Add `no_return` models for Java's `exit(...)` methods (can be extended further later on)
- handle throw-catch better by short-cutting throw nodes to not exit node but to all **catch nodes** that are reachable by the node. If there is no catch node, we short-cut to the exit node as before.
This removes a FP from deadstore tests because before we simply were not able to handle CF from throw-> catch nodes at all.
Reviewed By: skcho
Differential Revision: D20769039
fbshipit-source-id: e978f6cdb
Summary:
To find a method in non-abstract sub-classes, this diff applies the
same heuristics of inferbo.
* If the class is an interface: Find its unique sub-class and apply the heuristics recursively.
* If the class is an abstract class: Find/use its own summary if possible. If not found, find
one (arbitrary but deterministic) summary from its sub-classes.
* Otherwise: Find its own summary.
Reviewed By: ezgicicek
Differential Revision: D20647101
fbshipit-source-id: 2f8f3ff81
Summary: When looking at some reports I realised that adding the place where the memory becomes unreachable to the trace makes it more readable.
Reviewed By: skcho
Differential Revision: D20790277
fbshipit-source-id: d5df69e68
Summary:
`IssueLog` is used by the file-level analysis callbacks to store reports outside error logs so as to avoid racing on spec files. Each file should generate a single issue log which is then written to an appropriate file. The starvation checker was breaking that contract because it ostensibly needs to write out multiple issue files when analysing a single source file.
This is unnecessary, because the existing mechanisms for deduplication ensure only one issue file needs to be written out.
The whole-program mode still needs that capability, but this is implemented outside the file-analysis callback.
Reviewed By: mityal
Differential Revision: D20736135
fbshipit-source-id: 620e5484d
Summary:
Sometimes buck emits a timestamp, leading to a crash
> External Error: Failed to parse `buck targets --show-output ...` line of output:
> 2020-03-30 20:03:51
Reviewed By: dulmarod
Differential Revision: D20766438
fbshipit-source-id: 47cc00150
Summary:
OCaml 4.10.0 flagged that the `Extension` functor argument was unused.
Delete it and remove one layer of module in the file too now that it
doesn't need to be a functor.
Reviewed By: mityal
Differential Revision: D20669652
fbshipit-source-id: 089043d7d
Summary:
1. The return value is annotated as Nullable in codebase
2. The second parameter can be null as well.
Reviewed By: artempyanykh
Differential Revision: D20766243
fbshipit-source-id: 9aad37a8c
Summary:
This was needed countless of times. We log current signature, but not
callees.
Reviewed By: dulmarod
Differential Revision: D20765107
fbshipit-source-id: 399926c65
Summary:
This declaration is heavily used in Guava library.
Quick inspection shows that majority of methods are annotated correctly.
This will hide previosly hidden unsoundness issues in the codebase.
Reviewed By: artempyanykh
Differential Revision: D20737104
fbshipit-source-id: aa048bfc1
Summary:
The attribute `[no_return]` signifies that a function doesn't return. Previously, pre-analysis had cut the links to successor nodes of such no-return function nodes. This was intended to help with suppressing reporting on unreachable paths for some analyses. However, this results in having these nodes as dangling, with no connection to exit nodes.
This diff additionally shortcuts these no-return function nodes to exit node. This would allow us to enhance inter-procedural analyses like pulse to kepp track of paths that do not return since we will be keeping their connections at exit node rather than completely cutting them of as before. It would also allow us to assume that all paths start at the one start node and end at the one exit node (at least syntactically in the CFG).
Reviewed By: skcho
Differential Revision: D20736043
fbshipit-source-id: 0eace1bdb
Summary:
D20416859 introduced a new utility
`Process.create_process_and_wait_with_output` that:
1. executes the process to completion
2. reads stdout in full
3. reads stderr in full
Unfortunately, writing to stdout/stderr can be a blocking operation for
the callee process in that situation. Double unfortunately, reading both
stdout and stderr in a way that avoids starvation requires sophisticated
Unix-fu. Fortunately, callers of this utility only ever need to read
*one* of stdout or stderr.
Fix the starvation by:
1. reading *one* channel only (either stdout or stderr)
2. doing the reading *before* `wait`ing on the process to finish
3. redirecting the other channel to the console
Reviewed By: skcho, ngorogiannis
Differential Revision: D20737388
fbshipit-source-id: 2988ac865
Summary:
Knowing the number associated with each issue is useful to pass to
`infer explore --select XXX`.
Reviewed By: skcho
Differential Revision: D20696724
fbshipit-source-id: f6f368aa1
Summary:
Used `2to3` but had to (poorly, sorry!) fix byte -> string output of processes.
update-submodule: facebook-clang-plugins
Reviewed By: ngorogiannis
Differential Revision: D20672767
fbshipit-source-id: 852c7e973
Summary:
infer/lib/python/'s not pinin'! It's passed on! This library is no more!
It has ceased to be! It's expired and gone to meet its maker! It's a
stiff! Bereft of life, it rests in peace! If you hadn't nailed it to the
perch it'd be pushing up the daisies! 'ts metabolic processes are now
'istory! It's off the twig! It's kicked the bucket, it's shuffled off
its mortal coil, run down the curtain and joined the bleedin' choir
invisible!! THIS IS AN EX-PYTHON!!
Reviewed By: ngorogiannis
Differential Revision: D20672771
fbshipit-source-id: 7808c0ece
Summary:
Re-implement the generation of an HTML report (with bug traces) in
OCaml.
Kills the --only-show as a side-effect, it is of dubious use since there
is already infer-out/report.txt to get the report list as text. A
follow-up diff adds numbers to the list in infer-out/report.txt for easy
cross-referencing with `infer explore --select 123`.
Reviewed By: skcho
Differential Revision: D20672769
fbshipit-source-id: 39b3a299d
Summary:
When executing unit tests, don't parse the arguments as they will be
parsed by OUnit.
Reviewed By: skcho
Differential Revision: D20669675
fbshipit-source-id: 897ec10ee
Summary:
The text is ambiguous because it sounds as if it recommends annotating the current class as `ThreadSafe`, not the interface invoked.
Also, remove the not useful part "or using an interface known to be thread-safe" because developers don't know in general what interfaces Infer thinks are thread-safe.
Reviewed By: skcho
Differential Revision: D20675729
fbshipit-source-id: 9da438621
Summary:
Morally, INTERFACE_NOT_THREAD_SAFE is issued when an interface method is invoked from `ThreadSafe`-annotated code on an interface that is not known to be thread-safe or annotated so.
However, the ultimate purpose is to prevent races. Thus it should never be issued on an owned object or on objects we would not report races on for any reason (local variables, non-source variables, etc).
This diff equips interface call records with the abstract address they are invoked on, and uses the same rules for maintaining those records or not.
Reviewed By: skcho
Differential Revision: D20669259
fbshipit-source-id: 6c7841e6a
Summary:
For historical reasons, the record of an access is a three-level record:
1. `AccessSnapshot`, a record with info such as ownership and lock status, including
2. `TraceElem`, a record with a trace and an element which is
3. Access, the abstract addressed accessed and the type of access.
This stack flips the order to 2, 1, 3, leading up to the possibility of merging 1 and 3.
This diff improves the domain interface and consolidates all the various validity invariant checking for accesses inside their constructors.
Reviewed By: skcho
Differential Revision: D20668611
fbshipit-source-id: 45806d40d
Summary:
For historical reasons, the record of an access is a three-level record:
1. `AccessSnapshot`, a record with info such as ownership and lock status, including
2. `TraceElem`, a record with a trace and an element which is
3. Access, the abstract addressed accessed and the type of access.
This stack flips the order to 2, 1, 3, leading up to the possibility of merging 1 and 3.
This diff inverts 2 and 1.
Reviewed By: skcho
Differential Revision: D20644100
fbshipit-source-id: 89d810b68
Summary:
For historical reasons, the record of an access is a three-level record:
1. `AccessSnapshot`, a record with info such as ownership and lock status, including
2. `TraceElem`, a record with a trace and an element which is
3. `Access`, the abstract addressed accessed and the type of access.
This stack flips the order to 2, 1, 3, leading up to the possibility of merging 1 and 3.
This diff introduces functions in (1) that mask calls to (2), making the flip easier.
Reviewed By: skcho
Differential Revision: D20619614
fbshipit-source-id: 19fda0916
Summary: In an intra-procedural analysis we assume that parameters passed by reference to a function will be initialized inside that function. We use the type information of an actual parameter to initialize the fields of the struct. This does not work if a function has a parameter of type void* as the actual parameters also has type void*. To solve this issue, we use type information from local variables.
Reviewed By: jvillard
Differential Revision: D20670253
fbshipit-source-id: dc9f051ef
Summary:
This diff adds a procedure name to the head of the trace in order to distinguish issues in the same line.
"Updated Cost is ..." is changed to "Updated Cost of <proc name> is ..."
Reviewed By: ezgicicek
Differential Revision: D20672214
fbshipit-source-id: 303b4492f
Summary:
- Model `System.exit()` as early_exit and add a test
- Tweak message of methods that are impure due to having no pulse summary (and add a test)
Reviewed By: skcho
Differential Revision: D20668979
fbshipit-source-id: 6b5589aae
Summary:
Introducing a generalization of map_changed that can now
use a context on each instruction. The context is computed with
the previous instructions in the collection.
Reviewed By: skcho, jvillard
Differential Revision: D20669993
fbshipit-source-id: 58fdee1d9
Summary: This diff avoids that an invalid interval value, e.g. [0, -1], is genrated by interval pruning.
Reviewed By: ezgicicek
Differential Revision: D20645488
fbshipit-source-id: 6516c75d1
Summary:
Hopefully no one uses this. This is in Python and we'd like to get rid
of it. Easy enough to either re-implement if needed or to be
re-implemented by a third party.
Reviewed By: ngorogiannis
Differential Revision: D20626344
fbshipit-source-id: 484022482
Summary:
Seems like a more sensible name. Most tooling should read report.json so
won't notice.
Still output a bugs.txt file with a message to point to report.txt while
people migrate.
Reviewed By: mityal, artempyanykh
Differential Revision: D20626111
fbshipit-source-id: efb84d098
Summary:
The documentation of `--quiet` dates back from when it applied only to
`InferPrint.ml`. Make it more general and more in line with
expectations one might have about a `--quiet` option:
- change the doc
- make it disable the progress bar
Reviewed By: ngorogiannis
Differential Revision: D20626110
fbshipit-source-id: db096fd31
Summary:
This is a fairly popular class that have bunch of nullable methods.
Providing an alternative will make an error message actionable.
Note that this involves some duplication, and the whole API could be
improved. But let's leave it for future improvements.
Reviewed By: jvillard
Differential Revision: D20649099
fbshipit-source-id: bfcc7fd95
Summary: The current message is recommending to change `View.findViewById()` to `View.requireViewById()`, but the latter method is not supported in all API, so might lead to a crash in runtime.
Differential Revision: D20619361
fbshipit-source-id: 542746c79
Summary: Use the an LRUCache in Ondemand.LocalCache to avoid clearing it after every toplevel analysis.
Reviewed By: ngorogiannis
Differential Revision: D20281932
fbshipit-source-id: 752c8e1ea
Summary:
- the order of call state was wrong when printing contradiction for CItv
- add a test for impurity
Reviewed By: jvillard
Differential Revision: D20646181
fbshipit-source-id: 1c86fd0a4
Summary: There are no plans currently to track which lock protects each access, so reduce to the functional equivalent of having a singleton lock domain.
Reviewed By: skcho
Differential Revision: D20595013
fbshipit-source-id: d5100ac49
Summary:
As exemplified by added tests, pulse computes an empty summary (with 0 disjuncts) whenever it discovers a contradiction which might be caused by:
- discovering aliasing in memory
- widening limited number of times in loops and concluding that loop exit conditions are never taken
However, AFAIU, it is not possible to have a function with 0 disjunct apart from such anomalities. Even a function which does nothing like `void foo(){}` has 1 disjuncts:
```
Pulse: 1 pre/post(s)
#0: PRE:
{ roots={ };
mem ={ };
attrs={ };}
POST:
{ roots={ };
mem ={ };
attrs={ };}
SKIPPED_CALLS: { }
```
The aim of this diff is to consider functions with 0 disjuncts as **impure** because most often such cases are impure, rather than actually pure.
Reviewed By: skcho
Differential Revision: D20619504
fbshipit-source-id: 3a8502c90
Summary:
Although try-with-resource is supported by nullsafe this code pattern
throws it off and make nullsafe report on a virtual **b**yte-**c**ode
variable.
Check out debug output from `TryWithResource` (or attached
visualisation of CFG):
0. node14: $bcvar2=null (on entry to try-with-resource).
1. node16: n$14=$bcvar2, but **also** PRUNE(!(n$14 == null), true). Then we go to
2. node18: do something here and in case of exception go to
3. node25->node23->node19->node20: and here we do
$bcvar2->addSuppressed(...).
Because on step 1 we refined nullability of n$14, but didn't refine
nullability of $bcvar20, on step 3 we are sure that $bcvar is null and
therefore issue an error.
Reviewed By: mityal
Differential Revision: D20558343
fbshipit-source-id: 520505039
Summary:
This is likely not the final refinement, rather one step forward.
We classify all classes by 3 categories:
- Nullsafe and 0 issues
- can add Nullsafe and will be 0 issues
- the rest (class needs improvement)
Each class will fall into exactly one category.
Error messaging is WIP, they are not intended to be surfaced to the user
just yet.
Note how this diff uses the result of the previous refactoring.
Reviewed By: artempyanykh
Differential Revision: D20512999
fbshipit-source-id: 7f462d29d
Summary: Add a flag `is-inclusive-cost` (`true` by default) which computes inclusive cost for each function. Setting the flag to `false` computes exclusive cost of the function where the cost of the callees are assumed to be `0`.
Reviewed By: skcho
Differential Revision: D20558275
fbshipit-source-id: 6b5798916
Summary:
This function is used to adapt the callee summary at a call site. It did two things for every domain element in the callee summary:
- A linear search through the list of actuals.
- For each such actual, it would (repeatedly) compute its ownership (!).
For large summaries this can be substantial. The right way is to precompute the ownership for all actuals once and then simply retrieve it (via an array).
Reviewed By: jberdine
Differential Revision: D20564447
fbshipit-source-id: 1ca3121c2
Summary: The attribute types present are exclusive, so sets are not needed for the attribute map domain. This changes `Attribute` to a flat domain and removes the set on top of that.
Reviewed By: jberdine
Differential Revision: D20560240
fbshipit-source-id: 83e59d73e
Summary:
Both modules define properties the analysis maps to addresses, there is no reason to have two modules for this.
Also remove an instance of `Caml.Not_found` usage.
Reviewed By: jberdine
Differential Revision: D20558683
fbshipit-source-id: eacafd780
Summary:
# Problem
Consider
```
some_method(Object a) { a.deref(); }
```
What is nullability of `a` when we dereference it?
Logically, things like "LocallyCheckedNonnull" etc are not applicable
here.
This would be applicable if we called some_method() outside! But not
inside. Inside the function, it can freely treat params as non-null, as
long they are declared as non-nullable.
The best we can capture it is via StrictNonnull nullability.
Reviewed By: artempyanykh
Differential Revision: D20536586
fbshipit-source-id: 5c2ba7f0d
Summary:
# Problem
Yes, nullsafe is not null-safe, such an irony.
ErrorRenderingUtils overuses `option` and `let+` constructions. Most of
internal functions can return `None` when "something is wrong".
On top of this, "default" pattern match is overused either.
Because of this, `ErrorRenderingUtils.mk_nullsafe_special_issue` returns
optional type. In practice, this result can be None for many unclear
reasons, and it is super tricky to even understand them all.
This in turn forced AssignmentRule and DereferenceRule to process this
None is defensive way. The rules have some theory why None was returned,
and have assertions along the way.
Turns out those theories might be wrong. This diff will make triaging wrong assumptions easier.
Reviewed By: artempyanykh
Differential Revision: D20535720
fbshipit-source-id: 2b81e25b7
Summary: When we have clashing args to bug (for instance -j and -Xbuck --num-threads) CLI passed -Xbuck args should win.
Reviewed By: jvillard
Differential Revision: D20557060
fbshipit-source-id: 726fc501a
Summary:
`make test` failed in some test directories, because we were getting warnings
```
Foo.java uses unchecked or unsafe operations.
```
This diff fixes or suppresses these warnings.
Reviewed By: skcho
Differential Revision: D20557572
fbshipit-source-id: 63ecd3dfa
Summary:
First version of a new memory leak check based on Pulse. The idea is to examine unreachable cells in the heap and check that the "Allocated" attribute is available but the "Invalid CFree" isn't. This is done when we remove variables from the state.
Currently it only works for malloc, we can extend it to other allocation functions later.
Reviewed By: jvillard
Differential Revision: D20444097
fbshipit-source-id: 33b6b25a2
Summary:
- Add more naive pulse models for:
- `System.arraycopy`
- `StringBuilder.setLength`
- `StringBuilder.delete`
- Model the following as pure
- `SparseArrayCompat.valueAt`
- `File.get...`
- Add a nice test
Reviewed By: jvillard
Differential Revision: D20513397
fbshipit-source-id: 6d412d13a
Summary:
`to_reportable_violation` is responsible for identifying if the
violation is reportable in this mode or not.
This logic is higly coupled with other functions in
`ReportableViolation`, such as `get_description`: You can not have
sensible description on the violation that is NOT reportable in a given
mode.
So from logical perpsective, creation of `ReportableViolation.t` should
belong to this module itself, not to the parent `Rule` module.
This change will make design clearer.
Reviewed By: artempyanykh
Differential Revision: D20511756
fbshipit-source-id: ef27b5057
Summary:
This diff finishes work in D20491716.
We removed dependency on nullsafe mode for field initialization in
D20491716, so this diff just formalizes it.
Reviewed By: jvillard
Differential Revision: D20493164
fbshipit-source-id: 6ac612e78
Summary:
This diff continues work in D20491716.
This time for Inheritance Rule.
Reviewed By: jvillard
Differential Revision: D20492889
fbshipit-source-id: c4dfd95c3
Summary:
This diff continues work in D20491716.
This time for Dereference Rule.
Reviewed By: jvillard
Differential Revision: D20492296
fbshipit-source-id: ff7f824f9
Summary:
# Problem
In current design, Rules (assignment rule, dereference rule, inheritance
rule) decide, depending on the mode, wether the issue is legit or not.
If the issue is not actionable for the given mode, it won't be created
and registered.
For meta-issues, we want to be able to do smart things like:
- Identify if we can raise strictness of the mode without
introducing new issues
- Classify classes on "clean" vs "broken", taking into account issues
that are currently invisible.
# Solution
In the new design:
1. Rules are issuing violations independently of mode. This makes sense
semantically. Mode is "level of trust we have for suspicious things",
but the thing does not cease to be suspicious in any mode.
2. Each Rule decides if it is reportable or not in a given mode.
3. `nullsafe_mode` is passed to the function `register_error`, that 1)
adds error so it can be recorded in summary for file-level analysis
phase 2) reports some of them to the user.
# This diff
This diff converts only AssignmentRule, follow up will include
conversion of other rules, so no issue encapsutes the mode.
Reviewed By: jvillard
Differential Revision: D20491716
fbshipit-source-id: af17dd66d
Summary:
`make deadcode` is failing on master but our CI jobs didn't catch it :(
Let's fix existing deadcode for now.
Reviewed By: martintrojer
Differential Revision: D20510062
fbshipit-source-id: 4a5e5f849
Summary:
Previously, at each function call, we added a `WrittenTo` attribute for applying the address of the actuals. However, this results in mistakenly considering each function application that inspects its argument as impure. Instead, we should only propagate `WrittenTo` if the actuals have already `WrittenTo` attributes.
For instance, for the following functions
```
public static boolean is_null(Byte a) {
return a == null;
}
public static boolean call_is_null(Byte a) {
return is_null(a);
}
```
We used to get the following pulse summary for `call_is_null` (showing only one of the disjuncts):
```
#0: PRE:
{ roots={ &a=v1 };
mem ={ v1 -> { * -> v2 } };
attrs={ v1 -> { MustBeValid },
v2 -> { Arith =null, BoItv ([max(0, v2), min(0, v2)]) } };}
POST:
{ roots={ &a=v1, &return=v8 };
mem ={ v1 -> { * -> v2 }, v8 -> { * -> v4 } };
attrs={ v2 -> { Arith =null,
BoItv ([max(0, v2), min(0, v2)]),
WrittenTo-----------WRONG },
v4 -> { Arith =1,
BoItv (1),
Invalid ConstantDereference(is the constant 1),
WrittenTo-----------WRONG },
v8 -> { WrittenTo } };}
SKIPPED_CALLS: { }
```
where we mistakenly recorded a `WrittenTo` for `v2` (what `a` points to). As a result, we considered `call_is_null` as impure :( This diff fixes that since the callee `is_null` doesn't have any `WrittenTo` attributes for its parameter `a`. So, we don't propagate `WrittenTo` and get the following summary
```
#0: PRE:
{ roots={ &a=v1 };
mem ={ v1 -> { * -> v2 } };
attrs={ v1 -> { MustBeValid },
v2 -> { Arith =null, BoItv ([max(0, v2), min(0, v2)]) } };}
POST:
{ roots={ &a=v1, &return=v8 };
mem ={ v1 -> { * -> v2 }, v8 -> { * -> v4 } };
attrs={ v2 -> { Arith =null, BoItv ([max(0, v2), min(0, v2)]) },
v4 -> { Arith =1,
BoItv (1),
Invalid ConstantDereference(is the constant 1) },
v8 -> { WrittenTo } };}
SKIPPED_CALLS: { }
```
Reviewed By: skcho
Differential Revision: D20490102
fbshipit-source-id: 253d8ef64
Summary:
Make all arguments named and move function from `Procname.Java` to `Procname`, and making it return a `Procname.t` as opposed to `Procname.Java.t` (all callers want a `Procname` eventually).
Various other small fixes in the callers.
Reviewed By: skcho
Differential Revision: D20492305
fbshipit-source-id: e646cc799
Summary: These tests fail when seemingly unrelated changes are made to infer. In particular, it seems timeout limits have to be increased by 10x or more to make them succeed again. Disabling until we have a more stable replacement.
Reviewed By: ezgicicek
Differential Revision: D20489647
fbshipit-source-id: 9706b0807
Summary:
This diff naively models the following as `StdVector.push_back`:
- `StringBuilder.append`
- `String.replace`
- `Queue.poll`
It also adds a FN test for `Iterator.next`.
Reviewed By: skcho
Differential Revision: D20469786
fbshipit-source-id: 2d8e8d117
Summary:
This diff is doing three things:
1. Finishes work paved in D20115024, and applies it to nullsafe. In that diff, we hardened API for
file level analysis. Here we use this API in nullsafe, so now we can
analyze things on file-level, not only in proc-level like it was before!
2. Introduces a class-level analysis. For Nullsafe purposes, file is not
an interesting granularity, but we want to analyze a lot of things on
file level. Interesting part here is anonymous classes and how we link
them to their corresponding user-defined classes.
3. Introduces a first (yet to be improved) implementation of class-level
analysis. Namely it is "meta-issues" that tell what is going with class
on high level. For now these are two primitive issues, and we will
refine them in follow up diffs. They are disabled by default.
Follow ups include:
1. Refining semantics of meta-issues.
2. Adding other issues that we could not analyze before or analyzed not
user friendly. Most importantly, we will use it to improve reporting for
FIELD NOT INITIALIZED, which is not very user friendly exactly because
of lack of class-level aggregation.
Reviewed By: artempyanykh
Differential Revision: D20417841
fbshipit-source-id: 59ba7d2e3
Summary: The `FN_loop2` was not actually FN because infer analyzes its complexity as degree 1 correctly.
Reviewed By: dulmarod
Differential Revision: D20468367
fbshipit-source-id: 9e4c19415
Summary: The `iterate_over_mycollection_quad_FN` was not actually FN because infer analyzes its complexity as degree 2 correctly. So, this diff removed `_FN` from there.
Reviewed By: ezgicicek
Differential Revision: D20467398
fbshipit-source-id: b10340612
Summary: There has never been a sufficient formal basis for soundness nor completeness of reports on locals. This diff changes the domain to effectively concern only expressions rooted at formals or globals.
Reviewed By: ezgicicek
Differential Revision: D19769201
fbshipit-source-id: 36ae04d8c
Summary: `Object.clone` modeled as pure until the analysis can distinguish returning a fresh object vs. having no side-effects.
Reviewed By: skcho
Differential Revision: D20439998
fbshipit-source-id: 421054cfb
Summary:
As ngorogiannis pointed out, we never expect whitespaces in classname, so
stripping makes no sense here in best case, and hides a bug under rug in
worst case.
Reviewed By: jvillard
Differential Revision: D20417033
fbshipit-source-id: bc7449171
Summary: Let's also print skipped calls in `pp` to ease debugging both for summary and intermediate steps.
Reviewed By: jvillard
Differential Revision: D20417852
fbshipit-source-id: 7da03ae81
Summary:
There is a module and a module type in the file PulseAbductiveDomain.ml
with the same name. This is confusing and it's better to keep separate names.
Reviewed By: jvillard
Differential Revision: D20388769
fbshipit-source-id: bcfed436e
Summary:
Be a bit more careful about the difference between PrePost.t and
AbductiveDomain.t. It's needed in another diff where the types will be
different.
Reviewed By: ezgicicek
Differential Revision: D20393927
fbshipit-source-id: beaf80c90
Summary: In preparation for PulseArithmetic to be something else.
Reviewed By: ezgicicek
Differential Revision: D20393928
fbshipit-source-id: d93131e12
Summary:
`JavaSplitName` is used to represent Java types (in `Procname` in particular). The type itself is a pair of string (an optional package qualifier) and a "type name" (the quotes are there because it may contain array qualifiers).
For example `java.lang.Object[][]` should be represented as
```
{package=Some "java.lang"; typename="Object[][]"}
```
The constructor `make` was misused to construct instead types such as
```
{package=None; typename="java.lang.Object[][]"}`
```
This is evident when we print the return type of a `Procname` non-verbosely (the default), but we still see the package qualifier.
Obviously this is not just a pretty-printing bug, the values were themselves wrong.
The fix is to use the `of_string` constructor which will parse the package and separate it correctly. Another bug (in response to this one) had to be fixed in `Procname.is_vararg` to maintain behaviour in Nullsafe and Quandary.
Reviewed By: mityal
Differential Revision: D20394146
fbshipit-source-id: 4633902eb
Summary:
We will use it in follow up diffs.
From many perspectives, if the function belongs to an anonymous class,
it is useful to know the original user-defined class.
This function makes this distinction clear.
Thanks to ngorogiannis, whos work on refactoring `Typ.name` made this module
easy enough so we can introduce unit tests!
Reviewed By: ngorogiannis
Differential Revision: D20389311
fbshipit-source-id: 408d95660
Summary: `Procname.Java.get_return_typ` is buggy because whenever faced with an array of objects, it returns a type that implies the object is stored by value in the array (this is correct behaviour only when the element type is primitive, not when it's an object type).
Reviewed By: ezgicicek
Differential Revision: D20384403
fbshipit-source-id: d91322d3a
Summary:
We try to consolidate Java-specific stuff in JavaClassName.
Let's introduce the function in JavaClassName and make it clear that
its analog in Typ.Name.Java one throws if called on a wrong type.
Reviewed By: ngorogiannis
Differential Revision: D20386357
fbshipit-source-id: a1577ef8b
Summary:
Impurity domain was tracking all changes to variables (with a list of traces that containing all write/invalid accesses). This results in having long traces with multiple access events for the same variable. For instance,
```
void swap_impure(int[] array, int i, int j) {
int tmp = array[i];
array[i] = array[j]; \\ included in the trace
array[j] = tmp; \\ included in the trace
}
```
here we recorded both array accesses.
This diff changes the domain to include accesses so that we only keep track of a single trace per access. Array accesses are only recorded once.
Note that we want to record all unique accesses, not just the first one, because impurity will be used for hoisting/cost where we will invalidate impure arguments and consider all the rest as not changing.
Reviewed By: jvillard
Differential Revision: D20385745
fbshipit-source-id: d3647dad3
Summary:
D20362149 missed
- to pass the optional argument `include_value_history` to the recursive call in `PulseTrace.add_to_errlog`.
- to set `include_value_history=false` for skipped calls.
This diff fixes these issues.
Reviewed By: skcho
Differential Revision: D20385604
fbshipit-source-id: 176e4d010
Summary: No need to load the contents of the whole file(s) as a string first.
Reviewed By: ngorogiannis
Differential Revision: D20362602
fbshipit-source-id: 46fbc3693
Summary:
Next step in moving logic from make to dune. Since dune understands
build rules with multiple targets we don't need to introduce
artificial pipelining as in make. Rules are pretty straightforward,
albeit somewhat verbose.
The tricky part here was adjusting deadcode detection.
Reviewed By: jvillard
Differential Revision: D20322605
fbshipit-source-id: 688e5f96f
Summary:
Main changes are:
1. Dune can promote targets into the source tree as a part of build. This
allows us to **remove custom promotion/installation logic in src/Makefile**.
2. Dune promotion only works for path within workspace. This required
**moving dune-workspace one folder up**: from infer/infer/src to infer/infer.
But this is not bad, since it makes it possible to migrate tests under dune at some point.
3. `checkCopyright` now also promoted into `infer/infer/bin` instead of
`infer/scripts` partly for consistency and partly because of the
dune-workspace location.
4. `byte` mode was replaced with `byte_complete`. The latter takes
similar amount of time to build compared to `byte`, but produces
standalone binaries that don't require InferCStubs to be
installed. This allowed to remove `dune_exec_shim` and custom logic
around `dune build InferCStubs.install` when dealing with byte
targets.
All in all, `infer/src/Makefile` is not about 2/3 its previous size
with less custom logic in Makefiles/scripts and more encoded in dune
build files.
Reviewed By: jvillard
Differential Revision: D20303902
fbshipit-source-id: 9e4c65bd0
Summary:
With the introduction of environments and profiles we no longer need
to generate most dune files in libraries via make. Also, those dune
builds don't need to be in OCaml.
In addition to converting build files to plain sexp definitions, this
patch also:
- Adjusts copyrightCheck to work correctly with sexp-based dune files.
- Adds auto-formatting for sexp-based dune files.
Reviewed By: jvillard
Differential Revision: D20250208
fbshipit-source-id: 495aeaa99
Summary: With plain/sexp dune files we need to support lisp style comments in checkCopyright
Reviewed By: jvillard
Differential Revision: D20366314
fbshipit-source-id: 04db9e3c1
Summary:
With profiles and `(env ...)` stanza it's possible to consolidate
various ocamlc/ocamlopt/etc setups in a single place.
Where previously we needed to append `dune.common` to every dune file
and specify `flags` and `ocamlopt_flags` now the flags are specified
in `env` and applied accross the board.
This allows to
1. simplify build definitions,
2. avoid the need to generate dune files,
3. use plain sexps instead of OCaml and JBuilder plugin in build
files.
(I'll try to address 2 and 3 in the followup patches).
Existing `make` targets should continue working as before. Also, we
can use dune CLI like so:
```
infer/src$ dune printenv --profile opt # <- very useful for introspection
infer/src$ dune build check
infer/src$ dune build check --profile test
infer/src$ dune build infer.exe --profile dev
infer/src$ dune build infer.exe --profile opt
```
Also, with just 1 context something like `dune runtest` will run unit
tests only once instead of N times, where N is the number of contexts.
Now, there's one difference compared to the previous setup with
contexts:
- Previously, each context had its own build folder, and building infer
in opt context didn't invalidate any of the build artifacts in default
context. Therefore, alternating between `make` and `make opt` had low
overhead at the expense of having N copies of all build artifacts (1
for every context).
- Now, there's just 1 build folder and switching between profiles does
invalidate some artifacts (but not all) and rebuild takes a bit more
time.
So, if you're alternating like crazy between profiles your experience
may get worse (but not necessarily, more on that below). If you want
to trigger an opt build occasionally, you shouldn't notice much
difference.
For those who are concerned about slower build times when alternating
between different build profiles, there's a solution: [dune
cache](https://dune.readthedocs.io/en/stable/caching.html).
You can enable it by creating a file `~/.config/dune/config` with the
following contents:
```
(lang dune 2.0)
(cache enabled)
```
With cache enabled switching between different build profiles (but
also branches and commits) has ~0 overhead.
Dune cache works fine on Linux, but unfortunately there are [certain
problems with
MacOS](https://github.com/ocaml/dune/issues/3233) (hopefully, those
will be fixed soon and then there will be no downsides to using
profiles compared to contexts for our case).
Reviewed By: jvillard
Differential Revision: D20247864
fbshipit-source-id: 5f8afa0db
Summary:
What was happening in that case is that a .inferconfig file containing `{ "myflag":
false }` used to be translated by CommandLineOption as `--no-` (`--no-<long>`),
because it picked the *non-deprecated* form of the option (here `myflag` would
have to be a deprecated form of the option since its non-deprecated form is
empty `""`). Instead, pick a non-empty form of the option.
Reviewed By: jberdine
Differential Revision: D20368784
fbshipit-source-id: 8e761e684
Summary:
This was never quite finished and inferbo has a new way to do sort of
the same thing.
Reviewed By: skcho, ngorogiannis
Differential Revision: D20362619
fbshipit-source-id: 7c7935d47
Summary: Just for fun, and because killing InferPrint.ml is just so satisfying.
Reviewed By: ngorogiannis
Differential Revision: D20362643
fbshipit-source-id: 039cfec61
Summary:
Now that this module only prints report.json and costs_report.json, we
can dis-entangle the whole callback spaghetti.
Reviewed By: ngorogiannis
Differential Revision: D20362640
fbshipit-source-id: 56ffa4e08
Summary:
At this point in the stack, here's what's left in InferPrint.ml:
1. how to output report.json and costs_report.json
2. how to print summaries from the command line (`infer report`)
3. how to print --issues-tests stuff (`infer report --issues-tests`)
Keep only 1. in there. 2. goes to SpecsFiles.ml directly from infer.ml,
and 3. goes to its own module (also the fields to output in
--issues-tests get a non-poly variant).
1. does some extra stuff sometimes, eg in test-determinator mode. Keep
this for now.
Reviewed By: ngorogiannis
Differential Revision: D20362642
fbshipit-source-id: 0d9f0e8e2
Summary:
Make <infer-out>/report.json the default value for this option, as this
is what is used 99% of the time. Clean up test options using this.
Reviewed By: ngorogiannis
Differential Revision: D20362644
fbshipit-source-id: a1bb18757
Summary:
InferPrint hasn't been in charge of writing bugs.txt since forever.
This will be re-implemented as a post-processing of report.json instead
(like it is now, but in OCaml instead of python).
Reviewed By: ngorogiannis
Differential Revision: D20362641
fbshipit-source-id: 83d8cb53d
Summary:
I don't think anyone uses this. Meta-goal: cleaning up InferPrint.ml.
Measuring stats about summaries is good in principle, but we should do
it somewhere else instead of in the InferPrint callback hell. For
instance when we record each summary. Meanwhile, delete this.
Reviewed By: ngorogiannis
Differential Revision: D20362639
fbshipit-source-id: c73d431a5
Summary:
Adding a model for malloc: we add an attribute "Allocated". This can be used for implementing memory leaks: whenever the variables get out of scope, we can check that if the variable has an attribute Allocated, it also has an attribute Invalid CFree.
Possibly we will need more details in the Allocated attribute, to know if it's malloc, or other allocation function, but we can add that later when we know how it should look like.
Reviewed By: jvillard
Differential Revision: D20364541
fbshipit-source-id: 5e667a8c3
Summary:
This is not a full cleanup, but it is better than nothing.
At least `callback2` won't trigger me each time I see it anymore.
Reviewed By: jvillard
Differential Revision: D20364812
fbshipit-source-id: 8f25c24ad
Jules Villard
Mitya Lyubarskiy
Nikos Gorogiannis
Daiva Naudziuniene
David Pichardie
Sungkeun Cho
Dulma Churchill
Ezgi Çiçek
Fernando Gasperi Jabalera
Artem Pianykh
Martin Trojer