Summary:
The entry block contains all locals of the entire function, as
required by the backend. This makes the manipulation of the locals of
each block redundant.
This diff moves the locals from the entry block to the function
itself, removes the Locals frames of the Control.Stack, and adds a
locals field to Return frames.
This is part cleanup and part preparation for removing the
Control.Stack.
Reviewed By: ngorogiannis
Differential Revision: D15963503
fbshipit-source-id: 523ebc260
Summary:
The current handling of the formal return variable scope is not
correct. Since it is passed as an actual argument to the return
continuation, it is manipulated as if it was a local variable of the
caller. However, its scope is not ended with the caller's locals,
leading to clashes.
This diff reworks the passing of return values to avoid this problem,
mainly by introducing a notion of temporary variables during parameter
passing. This essentially has the effect of taking a function spec
{ P } f(x) { λv. Q }
and generating a "temporary" variable v, applying the post λv. Q to it
to obtain the pre-state for the call to the return continuation
k(v). Being a temporary variable just means that it goes out of scope
just after parameter passing. This amounts to a long-winded way of
applying the post-state to the formal parameter of the return
continuation without violating scopes or SSA.
This diff also separates the manipulation of the symbolic states as they
proceed from:
1. the pre-state before the return instruction;
2. the exit-state after the return instruction (including the binding
of the returned value to the return formal variable);
3. the post-state, where the locals are existentially quantified; and
4. the return-state, which is expressed in terms of actual args
instead of formal parameters.
Also in support of summarization, formal return and throw parameters
are no longer tracked on the analyzer's stack.
Note that these changes involve changing the locals of blocks and
functions to no longer include the formal parameters.
Reviewed By: kren1
Differential Revision: D15912148
fbshipit-source-id: e41dd6e42
Summary:
Print pre- and post- conditions (aka, summaries) when analyzer hits a
function return
- plumbing the precondition through the analyzer
so that it is available when return is hit
Reviewed By: jberdine
Differential Revision: D15713725
fbshipit-source-id: b10b6206f
Summary:
This diff adds a formal parameter to each non-void-returning function
to name the return value, and similarly a formal parameter for the
thrown exception value. These are interpreted as call-by-reference
parameters, so that they can be constrained in formulas to e.g. be
equal to the return value, and are still in scope when the function
returns, and so can be passed to the return block. Prior to
summarizing functions, this means that these formals need to be
tracked on the analyzer's control stack.
This will be needed to express function specs/summaries in terms of
formals, and fixes a bug where in some cases return values were not
tracked correctly.
Reviewed By: kren1
Differential Revision: D15738026
fbshipit-source-id: fff2d107c
Summary:
Disable exceptional control flow
- treat throw as unreachable
- confidence in the correctness of the frontend's treatment of
exception handling is very low, and making summaries that are
expressive enough to talk about exceptions is a complication
that isn't needed for the first iteration
To facilitate, start on a struct that holds all the CL options.
Reviewed By: jberdine, jvillard
Differential Revision: D15713601
fbshipit-source-id: ee92dfbd8
Summary:
The entry point functions are used in a couple of places, this
puts them in a single source of truth in the config file.
Reviewed By: jvillard
Differential Revision: D15651976
fbshipit-source-id: a572e8d4d
Summary:
Sledge does not terminate on programs with recursion, because
functions get "infinitely inlined" and therefore recursion is not
treated as retreating edge.
This patch bounds the number of times the same function can "inlined"
to respect the bound (`-b` option). On each call we check the number of
occurances of the called function in the call stack. If that is higher
than the bound, we skip it.
Reviewed By: jvillard
Differential Revision: D15577134
fbshipit-source-id: 4cd3b62c6
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
Timotej Kapus