Summary:
Previously only the arguments of binary operations on integers were
clamped to the given bitwidth, but the results could overflow. This
was incorrect.
Also, use a clamped version of equality to simplify equality
expressions. This was previously overlooked.
Reviewed By: mbouaziz
Differential Revision: D12854502
fbshipit-source-id: 8786b4217
Summary:
Running `dune build check` while `dune build --watch` is running
intermittently produces strange errors due to race conditions between
the two.
Reviewed By: mbouaziz
Differential Revision: D12854510
fbshipit-source-id: 348a902bc
Summary:
Get rid of `USE_AFTER_LIFETIME`. This could be useful to deploy pulse
alongside the ownership checker too.
Reviewed By: da319
Differential Revision: D12857477
fbshipit-source-id: 8e2a2a37c
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:
Keep `USE_AFTER_LIFETIME` for unclassified errors (for now it contains
vector invalidation too because I can't think of a good name for
them, and maybe it makes sense to wait until we have more types of them
to decide on a name).
Reviewed By: da319
Differential Revision: D12825060
fbshipit-source-id: bd75ef698
Summary:
Getting this right will be long and complex so for now the easiest is to
underreport and only consider as invalid the addresses we know to be invalid on
both sides of a join. In fact the condition for an address to be invalid after
a join is more complex than this: it is invalid only if *all* the addresses in
its equivalence class as discovered by the join are invalid.
Reviewed By: skcho
Differential Revision: D12823925
fbshipit-source-id: 2ca109356
Summary: Similarly as for destructors, we provide an address of an object as a first parameter to constructors. When constructor is called we want to create a fresh location for a new object.
Reviewed By: jvillard
Differential Revision: D10868433
fbshipit-source-id: b60f32953
Summary:
There were several lists constructed unnecessarily -- replaced them with find_maps
and hopefully simplified the logic.
Reviewed By: mbouaziz, jvillard
Differential Revision: D12823559
fbshipit-source-id: 1f06b20f3
Summary:
Sometimes in debug mode, the condition set is too big to print in the
log file. This diff limits the maximum number of conditions to print
as 30.
Reviewed By: mbouaziz
Differential Revision: D12836661
fbshipit-source-id: 8ddfe64a7
Summary: We provide an address of an object as a parameter to destructor. When destructor is called the object itself is invalidated, but not the address.
Reviewed By: jvillard
Differential Revision: D12824032
fbshipit-source-id: 516eebcf8
Summary:
Seems useful to know when we're printing one instruction only, but not when we
print lots of them for readability.
Reviewed By: mbouaziz
Differential Revision: D12823481
fbshipit-source-id: 2beb339f2
Summary:
It terminates narrowing when new and old states are not comparable.
Since current narrowing does not use meet operations guaranteeing
termination of narrowing, it tries to terminate narrowing more
conservatively.
Reviewed By: mbouaziz
Differential Revision: D12815419
fbshipit-source-id: e8b45199e
Summary: It tries division on minmax value approximately, rather than just returning infinities. For example, `[0,2+min(6,s)] / 2` returns `[0,4]`.
Reviewed By: mbouaziz
Differential Revision: D10867091
fbshipit-source-id: d3f49987b
Summary:
This diff preserves values of offset and index separately, rather than
one value of their addition, because premature addition results in
imprecise FPs by the limited expressiveness of the domain.
Reviewed By: mbouaziz
Differential Revision: D10851393
fbshipit-source-id: 1685ead36
Summary:
The time has come to keep track of which tests pass and which are FP/FN
for pulse.
Reviewed By: mbouaziz
Differential Revision: D10854064
fbshipit-source-id: 60938e48f
Summary:
Turns out once a vector array became invalid it stayed that way, instead
of the vector getting a new valid internal array.
Reviewed By: skcho
Differential Revision: D10853532
fbshipit-source-id: f6f22407f
Summary:
Now the domain can reason about `&` and `*` too. When recording `&`
between two locations also record a back-edge `*`, and vice-versa.
Reviewed By: mbouaziz
Differential Revision: D10509335
fbshipit-source-id: 8091b6ec0
Summary: This is more flexible and allows us to give more details when reporting.
Reviewed By: mbouaziz
Differential Revision: D10509336
fbshipit-source-id: 79c3ac1c8
Summary: Just to organise PulseDomain a bit more since it's quite big.
Reviewed By: mbouaziz
Differential Revision: D10509334
fbshipit-source-id: a81b36aa6
Summary: This should stop the bleeding until we get a better solution like shared memory + single writer process.
Reviewed By: mbouaziz
Differential Revision: D10868360
fbshipit-source-id: a4d0b064e
Summary: To avoid reporting on private methods, ignore those starting with underscore. Other cleanups.
Reviewed By: jvillard
Differential Revision: D10558970
fbshipit-source-id: 0572f1e70
Josh Berdine
Jules Villard
Daiva Naudziuniene
Mehdi Bouaziz
Sungkeun Cho
Nikos Gorogiannis
Dino Distefano
Jeremy Dubreil