Summary:
this makes frontends no longer depend on SymExec.ml. `ModelBuiltins` was split into two modules:
- `BuiltinDecl` with procnames for builtins (used to determine whether some function is a builtin)
- `BuiltinDefn` with implementations used by `SymExec`
- they both have similar type defined in `BUILTINS.S` which makes sure that new builtin gets added into both modules.
During the refactor I ran some scripts:
`BuiltinDecl.ml`:
let X = create_procname "X"
cat BuiltinDecl.ml | grep "create_procname" | tail -70 | awk ' { print $1,$2,$3,$4,"\42"$2"\42"} '
then manually confirm string match. Exceptions:
"__exit" -> "_exit"
"objc_cpp_throw" -> "__infer_objc_cpp_throw"
__objc_dictionary_literal
nsArray_arrayWithObjects
nsArray_arrayWithObjectsCount
`BuiltinDefn.ml`:
let X = Builtin.register BuiltinDecl.X execute_X
cat BuiltinDecl.ml | grep "create_procname" | tail -70 | awk ' { print $1,$2,$3,"Builtin.register BuiltinDecl."$2,"execute_"$2} '
then, fix all compilation problems
Reviewed By: jberdine
Differential Revision: D3951035
fbshipit-source-id: f059602
Summary:
Change command line options for dynamic dispatch to capture that the
alternatives are mutually exclusive.
Reviewed By: jeremydubreil
Differential Revision: D4074540
fbshipit-source-id: c329717
Summary: The lazy dynamic dispatch algorithm works by re-analyzing the generic methods with the more specialized types encountered during the symbolic execution. In order to do that, the analysis must access the procedure description of the method to reanalyze in order to run the analysis of the specialized procedure description on demand. This diff adds the procedure description on the summary as the summary are stored in the Buck cache and can easily be retrieved by procname.
Reviewed By: sblackshear
Differential Revision: D4077415
fbshipit-source-id: c2f1cc8
Summary:
This diff removes the unused support for reporting props, which enables
refactoring so that the 'base' directory has no dependencies, and the
'IR' directory depends only on 'base'.
Reviewed By: jvillard
Differential Revision: D3981352
fbshipit-source-id: 3700a23
Summary:
Change Sil.Call instruction to have only a single optional return
identifier, insted of a list. Essentially none of the code handled
multiple return identifiers. Also, add the type of the return
identitifier to Call instructions.
Reviewed By: sblackshear
Differential Revision: D3919358
fbshipit-source-id: d2d4f72
Summary:
It is no longer necessary to keep the name of a struct within the
struct, as the name will just have been used to look it up.
Reviewed By: cristianoc
Differential Revision: D3919355
fbshipit-source-id: ab65168
Summary:
This diff removes the redundancy in the representation of types where
struct types could be represented either directly using Tstruct or
indirectly using Tvar to refer to the type environment. A consequence
is that it is much harder to construct large type values.
Reviewed By: sblackshear, cristianoc
Differential Revision: D3839753
fbshipit-source-id: cf04ea5
Summary:
Rename Typ.mk_struct to internal_mk_struct, and add Tenv.mk_struct that
ensures types are added to the environment under the right name.
Reviewed By: cristianoc
Differential Revision: D3791865
fbshipit-source-id: fd4b667
Summary:
The Typ.struct_typ.csu field is now redundant with the Csu.t in the
name: Typename.t field.
Reviewed By: cristianoc
Differential Revision: D3791861
fbshipit-source-id: 5370885
Summary: Replace the struct_name: Mangled.t option field of Typ.struct_typ with name: Typename.t
Reviewed By: sblackshear
Differential Revision: D3791860
fbshipit-source-id: 3ee1d00
Summary:
This helps avoid some unintended reports where the actual is known to point to
a specific object before a call to a skipped function. This requires a change
in the plugin to export more info about const types.
Reviewed By: dulmarod
Differential Revision: D3711901
fbshipit-source-id: f5c903e
Summary:
Clean up the API to access component of propositions.
Use uniform naming for getting and setting components.
Reviewed By: jberdine
Differential Revision: D3696180
fbshipit-source-id: a8aedb0
Summary:
This diff lifts the Prop.Attribute module out of Prop. This required
moving several Prop functions that depend on Attribute
(find_arithmetic_problem, deallocate_stack_vars, find_equal_formal_path)
and adding numerous calls to Prop.normalize to fix normal/exposed
mismatches. Also note that the type of Prop.normalize is generalized to
allow calling it on normalized props.
Reviewed By: cristianoc
Differential Revision: D3684523
fbshipit-source-id: f37af8b
Summary:
Move the Sil.attribute type and associated types and operations to a new
PredSymb module.
Reviewed By: cristianoc
Differential Revision: D3683834
fbshipit-source-id: d3606a8
Summary:
Change the Aobjc_null attribute from a family of unary predicates, one
for each Pvar.t * Ident.fieldname list, to a single binary predicate.
This diff should not change behavior except for printing of Aobjc_null
attributes. Also, operations such as free variables, etc. should now
behave correctly with respect to variables occurring in the arguments of
Aobjc_null.
Reviewed By: cristianoc
Differential Revision: D3669392
fbshipit-source-id: fe4434a
Summary:
Add support for nary predicates, not just unary ones. Many operations
don't make much sense for nullary predicates, and are generally treated
as no-ops. The first argument is treated specially, as the "anchor" of
the predicate application. For example, adding or removing an attribute
uses the anchor to identify the atom to operate on. Also, abstraction
and normalization operations treat the anchor specially.
Reviewed By: cristianoc
Differential Revision: D3669391
fbshipit-source-id: 3d142ea
Summary:
Simplify the (implementation and) interface of Prop by using the atom
type directly instead of a tuple type that duplicates the fields.
This change does not weaken the type guarantees, while reducing
redundancy between types thereby making future changes easier.
Reviewed By: cristianoc
Differential Revision: D3669388
fbshipit-source-id: 65f7493
Summary:
Treat attributes as unary predicates in classical first-order logic.
This diff extends predicates with a polarity and uses classical 2-valued
semantics. This potentially changes the behavior of negating
attributes, which was not previously relied on.
Reviewed By: sblackshear
Differential Revision: D3669365
fbshipit-source-id: 2f26776
Summary:
Replace disequalities to Attribute expressions with predicate symbol
application pure atomic formulas.
This diff should preserve existing behavior, up to the comparison order
of attribute disequalities versus predicate applications.
Reviewed By: sblackshear
Differential Revision: D3647049
fbshipit-source-id: c39a901
Summary:
Cosmetic changes to comments to improve the results of the Reason
comment attachment logic.
These were found using `git grep -nH -e 'in[ ]*(\*'` although the
attachment logic seems ok if the associated `let` is on the same line.
Some others were found with `git grep -nH -e ')[ ]*(\*'` although the
attachment logic seems ok if the associated `(` is on the same line.
Reviewed By: jvillard
Differential Revision: D3654027
fbshipit-source-id: 122aa3b
Summary:
Move Sil.call_flags type and operations into separate CallFlags
module.
Reviewed By: dulmarod
Differential Revision: D3548086
fbshipit-source-id: 6d264e9
Summary: Move Sil.binop type and operations into separate Binop module.
Reviewed By: dulmarod
Differential Revision: D3548082
fbshipit-source-id: 356bee3
Summary: Move Sil.unop type and operations into separate Unop module.
Reviewed By: dulmarod
Differential Revision: D3548077
fbshipit-source-id: 49d3d83
Summary: Move Sil.const type and operations into separate Const module.
Reviewed By: dulmarod
Differential Revision: D3548073
fbshipit-source-id: 388d03e
Summary:
Move attribute values from const to exp. They are not constants, and
this reduces interdependence between Sil types.
Reviewed By: cristianoc
Differential Revision: D3548055
fbshipit-source-id: 31a9121
Summary:
The Aobjc_null attribute does not need a fully general exp. This diff
refines this to a possibly-empty path of fields starting from a pvar,
which reduces interdependence between Sil types.
Reviewed By: dulmarod
Differential Revision: D3548043
fbshipit-source-id: 49d16ab
Summary:
Move closure values from const to exp. They are not constants, and
this reduces interdependence between Sil types.
Reviewed By: sblackshear
Differential Revision: D3541364
fbshipit-source-id: 1a2f998
Summary:
Move exception values from const to exp. They are not constants, and
this reduces interdependence between Sil types.
Reviewed By: sblackshear
Differential Revision: D3541355
fbshipit-source-id: f22e0ba
Summary:
Now that array types record only static - and therefore constant -
lengths, Sil typ and exp no longer need to be mutually recursive.
This diff:
- splits the recursion in the type definitions of typ and exp,
- splits the recursion in the comparison and pretty-printing
functions,
- and then refactors typ into a separate module.
Reviewed By: cristianoc
Differential Revision: D3423575
fbshipit-source-id: 6130630
Summary:
This diff refactors Sil.Int, which represents integer literals, into a
separate module IntLit. There are no dependencies forcing Sil.Int to
be a submodule of Sil, and it is also no simpler as a submodule.
Reviewed By: cristianoc
Differential Revision: D3422910
fbshipit-source-id: 63013f2
Andrzej Kotulski
Josh Berdine
Jeremy Dubreil
Cristiano Calcagno
Dulma Churchill
Sam Blackshear
Jules Villard
Martino Luca