Summary: Just changing ClangTrace to actually look at the different sanitizer kinds.
Reviewed By: jeremydubreil
Differential Revision: D6325086
fbshipit-source-id: 5da236d
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:
In a summary, you never want to see a trace where non-footprint sources flow to a sink.
Such a trace is useless because nothing the caller does can make more data flow into that sink.
Reviewed By: jeremydubreil
Differential Revision: D5779983
fbshipit-source-id: d06778a
Summary: A stepping stone to have descriptive issue types for each kind of flow rather that lumping everything into `QUANDARY_TAINT_ERROR`.
Reviewed By: mbouaziz
Differential Revision: D6126690
fbshipit-source-id: a7230c0
Summary: Previously, this would incorrectly classify types like `map<std::string, int>` as a buffer
Reviewed By: mbouaziz
Differential Revision: D6125530
fbshipit-source-id: c8564de
Summary:
Looked at some problematic summaries and am noticing some common patterns.
Adding some dynamic checks to be run in debug mode in order to make sure my fixes for these patterns are real.
Reviewed By: jeremydubreil
Differential Revision: D5779593
fbshipit-source-id: 9de6497
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:
`pp_instr_list` was not tailrec causing a stack overflow on big code.
Also simplified a few things
Reviewed By: jvillard
Differential Revision: D5995451
fbshipit-source-id: 40a4911
Summary:
Expanding traces currently works in the following way:
Given a `TraceElem.Kind` `k` we want to report in `foo`, we look for a callee `C` of `foo` that has a `TraceElem.Kind` equal to `k` in its summary, grab the summary for `C`, then repeat until we bottom out.
This isn't very flexible: it insists on equality between `TraceElem.Kind`'s as the criteria for expanding a trace.
This diff introduces a new `matches` function for deciding when to expand a trace from a caller into a callee.
Clients that don't want strict equality can implement a fuzzier kind of equality inside this function.
I've gone ahead and done this for the trace elemes of thread-safety.
In the near future, equivalent access paths won't always compare equal from caller to callee, so we want to match their suffixes instead.
Reviewed By: jvillard
Differential Revision: D5914118
fbshipit-source-id: 233c603
Summary:
We supported globals as sources before, but we did so by allowing ClangTrace etc. to match against any access path in the footprint of the trace.
This is very powerful/flexible, but it's ultimately not a good idea because it leads to traces that are hard to read.
This is because a footprint source doesn't have any information about its provenance: we might know that the value came from a global, but we don't know where the read occurred.
The mechanism for handling procedure calls as sources already knows how to solve this problem.
This diff implements globals as sources as a special case of procedure call sources instead.
This will give us much nicer traces with full provenance of the read from the global.
Reviewed By: mbouaziz
Differential Revision: D5772299
fbshipit-source-id: 491ae81
Summary: Add procedure where error is triggered (if available) + bad data to messages.
Reviewed By: jvillard
Differential Revision: D5756398
fbshipit-source-id: a16f7cf
Summary:
- failwith police: no more `failwith`. Instead, use `Logging.die`.
- Introduce the `SimpleLogging` module for dying from modules where `Logging`
cannot be used (usually because that would create a cyclic dependency).
- always log backtraces, and show backtraces on the console except for usage errors
- Also point out in the log file where the toplevel executions of infer happen
Reviewed By: jeremydubreil
Differential Revision: D5726362
fbshipit-source-id: d7a01fc
Summary:
A function can both be a sink and propagate source info, but we currently ignore the summary for any function that is also a sink.
This will cause us to under-report for (e.g.) `src1 = source(); src2 = strcpy(dest, src1); exec(src2)`.
This is both a potential buffer overflow and a potential shell injection, but we won't report the second issue.
Reviewed By: jberdine
Differential Revision: D5676167
fbshipit-source-id: 232ab2f
Summary:
We now represent the footprint with an access trie, so this code is no longer required.
This lets us simplify things a bit
Reviewed By: jberdine
Differential Revision: D5664484
fbshipit-source-id: c35edf2
Summary:
In looking at summaries that Quandary took a long time to compute, one thing I notice frequently is redundancy in the footprint sources (e.g., I might see `Footprint(x), Footprint(x.f), Footprint(x*)`).
`sudo perf top` indicates that joining big sets of sources is a major performance bottleneck, and a large number of footprint sources is surely a big part of this (since we expect the number of non-footprint sources to be small).
This diff addresses the redundancy issue by using a more complex representation for a set of sources. The "known" sources are still in a set, but the footprint sources are now represented as a set of access paths (via an access trie).
The access path trie is a minimal representation of a set of access paths, so it would represent the example above as a simple `x*`.
This should make join/widen/<= faster and improve performance
Reviewed By: jberdine
Differential Revision: D5663980
fbshipit-source-id: 9fb66f8
Summary:
Instead of a whitelist and blacklist and default issue types and default
blacklist and filtering, consider a simpler semantics where
1. checkers can be individually turned on or off on the command line
2. most checkers are on by default
3. `--no-filtering` turns all issue types on, but they can then be turned off again by further arguments
This provides a more flexible CLI and is similar to other options in the infer
CLI, where "global" behaviour is generally avoided.
Dynamically created checkers (eg, AL linters) cause some complications in the
implementation but I think the semantics is still clear.
Also change the name of the option to mention "issue types" instead of
"checks", since the latter can be confused with "checkers".
Reviewed By: jberdine
Differential Revision: D5583238
fbshipit-source-id: 21de476
Summary: Useful for identifying user-controlled array accesses that could lead to buffer overflows
Reviewed By: mbouaziz
Differential Revision: D5520985
fbshipit-source-id: 92984f6
Summary:
When a sink name is specified in `.inferconfig` or in OCaml, it might conflict with a function of the same name that has a different number of args.
We shouldn't try to create a sink in this case, and we definitely shouldn't crash.
Reviewed By: jeremydubreil
Differential Revision: D5561216
fbshipit-source-id: fa1859b
Summary: A temporary workaround until we can understand why this happens and fix it.
Reviewed By: jeremydubreil
Differential Revision: D5559838
fbshipit-source-id: dc86eb9
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:
It's nice to have "raw" as the default kind of access path, since it's used much more often than the abstraction.
This is also a prereq for supporting index expressions in access paths, since we'll need mutual recursion between accesses and access paths.
Reviewed By: jeremydubreil
Differential Revision: D5529807
fbshipit-source-id: cb3f521
Summary: This gives us more expressive power when defining sources--we can use heuristics like "`foo(o)` only returns a source when `o` is not a constant".
Reviewed By: jvillard
Differential Revision: D5467935
fbshipit-source-id: f3d581d
Sam Blackshear
Josh Berdine
Mehdi Bouaziz
Jules Villard