Summary:
When comparing stacks as part of a control-flow edge, treat each as a
code location in a hypothetical expansion of the program where all
non-recursive functions have been completely inlined. In particular,
this means to compare stacks as if all Locals frames or Return frames
for recursive calls had been removed. Additionally, the from_call info
in Return frames is ignored.
Reviewed By: jvillard
Differential Revision: D14657601
fbshipit-source-id: b8a42d3fa
Summary:
- Ensure that popping Throw or Return does not leave stale Throw or
Return frames
- Add a module for Control.stack
- Add invariant to enforce that a Throw frame can appear only
immediately above a Return frame
Reviewed By: jvillard
Differential Revision: D14547263
fbshipit-source-id: deb31b8af
Summary:
This diff adds support in symbolic execution for calls to intrinsic
functions, to be used in lieu of adding a separate Llair instruction
for each intrinsic. This involves:
- adding skeleton support in Exec for symbolically execution an
intrinsic function call;
- exposing this in Domain;
- allowing symbolic execution of block terminators (e.g. function
call) to possibly fail; and
- generalizing Report for failing terminators.
Reviewed By: ngorogiannis
Differential Revision: D14403652
fbshipit-source-id: d86d9d1b8
Summary:
Also for debugging support, note that analysis can be stopped after
reporting an attempt to call an unknown function with `sledge
-tReport.unknown_call` and likewise for invalid memory accesses with
`sledge -tReport.invalid_access`.
Reviewed By: mbouaziz
Differential Revision: D10389474
fbshipit-source-id: b006480d3
Josh Berdine