Summary:
Change command line interface to include buck and llvm integration as
separate subcommands.
Reviewed By: kren1
Differential Revision: D15614567
fbshipit-source-id: b7618571b
Summary:
Use the new LLVM bindings to handle internalization.
We would like to use global dead code elimination (gdce) to remove all the code not reachable from an entry point. However in normal compilation most functions aren't globally dead (they can be linked to). At the point of running sledge we won't be linking anymore, therefore we can internalize (make invisible outside of the compilation unit) all the symbols. In that case the whole program is dead with respect to gdce, therefore we need to preserve the entry point as external.
Previously we could only preserve `main` as the entry point (through a boolean flag). This patch uses a newer API that lets us preserve functions that satisfy a given predicate function. This enables us to have arbitrary entry points (not just main). Currently only the 3 entry points from `src/control.ml` are used, but this patch makes it easy to change.
Reviewed By: ngorogiannis
Differential Revision: D15561461
fbshipit-source-id: 88e054411
Summary:
LLVM.global_initializer casues a cast assertion failure if the value
passed to it is not a GlobalVariable. So we first check if it is a
GlobalVariable and only then ask for an initiliazer.
This is hidden if LLVM is built without assertions.
Reviewed By: jberdine
Differential Revision: D15601632
fbshipit-source-id: e9db23a12
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:
This diff changes the translation of global variables to translate the
initializer whenever it exists in LLVM, rather than relying on
linkage. Previously code such as
```
char *mutable_string = "hahaha";
```
would lead to LLVM code
```
nutritious_string = global i8* getelementptr inbounds ([7 x i8], [7 x i8]* @.str, i32 0, i32 0), align 8, !dbg !0 ; [#uses=2 type=i8**]
```
in which `mutable_string` had `External` linkage according to
`Llvm.linkage` even though it has an initializer. This could cause
sledge to drop the initializer.
Reviewed By: kren1
Differential Revision: D15577755
fbshipit-source-id: 50aa06c5e
Summary:
Global variables have pointer type. The size needed by the backend is
of the element type, not of the pointer itself. This diff corrects
this.
Reviewed By: kren1
Differential Revision: D15577756
fbshipit-source-id: 948ecf3cd
Summary:
It is unsafe to call protocol methods defined optional. Before calling them we should check it
the implementation exists by calling
`if ([object respondsToSelector:selector(...)]) ...`
Without the above check we get run time crashes.
Reviewed By: jvillard
Differential Revision: D15554951
fbshipit-source-id: f0560971b
Summary: In its new form it actually tests that infer takes the correct branch.
Reviewed By: mbouaziz
Differential Revision: D15494297
fbshipit-source-id: 7b9bb8f75
Summary:
- take advantage more structured attributes in the exported AST
- circumvent new format of `if` and `switch`
- a few new features/nodes but nothing major there
update-submodule: facebook-clang-plugins
Reviewed By: mbouaziz, martintrojer
Differential Revision: D15453572
fbshipit-source-id: c0c24345f
Summary:
Somehow clang now chooses slightly different arguments to pass to `ld`
in the invocation that `ndk-build` makes to link:
```
--- clang7 2019-05-28 07:47:19.214949009 -0700
+++ clang8 2019-05-28 07:46:55.095924374 -0700
@@ -1,6 +1,15 @@
"/opt/android_ndk/r15c/toolchains/aarch64-linux-android-4.9/prebuilt/linux-x86_64/lib/gcc/aarch64-linux-android/4.9.x/../../../../aarch64-linux-android/bin/ld"
"--sysroot=/opt/android_ndk/r15c/platforms/android-21/arch-arm64"
+"-EL"
"--fix-cortex-a53-843419"
+"-z"
+"now"
+"-z"
+"relro"
+"-z"
+"max-page-size=4096"
+"--hash-style=gnu"
+"--hash-style=both"
"--no-add-needed"
"--enable-new-dtags"
"--eh-frame-hdr"
@@ -32,7 +41,7 @@
"--fatal-warnings"
"-lc"
"-lm"
-"-lstdc++"
+"-lc++"
"-lm"
"-lgcc"
"-ldl"
```
In particular:
- `lc++` results in `libc++.so` not found from the toolchain
- the forced relocation `-z relro` fails with "/..//bin/ld: ./obj/local/arm64-v8a/objs/hello/__/hello.o: Relocations in generic ELF (EM: 183)" and other weirder errors
Somehow pretending the C++ compiler is `clang` instead of `clang++` stops the insanity.
Also add an Application.mk file to specify some sane defaults.
Also add `V=1` to the `ndk-build` invocation in our tests so that when it fails we have a bit more to work with.
Reviewed By: mbouaziz, martintrojer
Differential Revision: D15518447
fbshipit-source-id: 40203814b
Summary:
- Rename `invariantModels` to `purityModels`
- Track which arguments are modified in purity models. Before we were invalidating all arguments of impure modeled functions. Instead, now we only invalidate modified args given in the model. This should ideally result in more precision in the analysis.
- Add some more purity models for :`cast`, `new`, `new_array` and `Math.random`
Reviewed By: mbouaziz
Differential Revision: D15535332
fbshipit-source-id: 5395800d9
Summary:
The root cause is not clear, but it seems that not calling
Llvm.dispose_context avoids segfaults in the GC.
Reviewed By: kren1
Differential Revision: D15535434
fbshipit-source-id: 280e44d0b
Summary:
The name and loc tables are added-to almost exactly in sync, so
combine them to amortize the overhead.
Reviewed By: kren1
Differential Revision: D15535435
fbshipit-source-id: 801da75bb
Summary:
Format is slow. Especially Format.sprintf, which has to allocate and
initialize a buffer every time.
Reviewed By: kren1
Differential Revision: D15535437
fbshipit-source-id: ea43f44e1
Summary:
This isn't free and is expected to hold of bitcode produced by
clang/llvm. There are tests that fail verification, so keep it in
debug mode.
Reviewed By: kren1
Differential Revision: D15535438
fbshipit-source-id: 9390a8363
Summary:
If the input file has a .bc or .ll suffix, treat it as a pre-linked
bitcode file. Otherwise, treat it as before, as a file containing a
list of bitcode files to be linked. Also, perform global dead-code
elimination only when linking multiple files.
Reviewed By: kren1
Differential Revision: D15513345
fbshipit-source-id: 4c80ff9c3
Summary:
That test wasn't hooked up to `make test` and so regressed at some
unknown time in the past. Just recording the new state of things for
now.
Reviewed By: ngorogiannis
Differential Revision: D15495234
fbshipit-source-id: 14fb112de
Summary:
Change the sledge input format from a bitcode file to a newline
separated list of paths to LLVM bitcode files.
Reviewed By: jberdine
Differential Revision: D15470082
fbshipit-source-id: 8860f947c
Summary:
Llvm.string_of_llvalue, which just calls llvm::Value::print, is
extremely slow when called on instructions or functions. In these
cases, it initializes metadata slots for everything in the *parent
module* of the instruction or function being printed, on every
call. This is ridiculously slow, don't do it.
Reviewed By: kren1
Differential Revision: D15511376
fbshipit-source-id: 658eeccab
Summary:
Add shortcut code paths to return early in some cases guaranteed to be
the identity function.
Reviewed By: ngorogiannis
Differential Revision: D15468704
fbshipit-source-id: f137049c6
Summary:
Infer was complaining about a parameter not null checked, which was failing the
model compilation since no errors are allowed on models.
Reviewed By: ezgicicek
Differential Revision: D15453573
fbshipit-source-id: 3bd0df715
Josh Berdine
Ezgi Çiçek
Timotej Kapus
Martin Trojer
Dino Distefano
Nikos Gorogiannis
Peter O'Hearn
Jules Villard
Radu Grigore