[sledge] Fix translation of global initializers

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

sledge/src/llair/frontend.ml

@@ -578,11 +578,11 @@ and xlate_global : x -> Llvm.llvalue -> Global.t =
          its own initializer *)
       Hashtbl.set memo_global ~key:llg ~data:(Global.mk g typ loc) ;
       let init =
-        match (Llvm.classify_value llg, Llvm.linkage llg) with
+        match (Llvm.classify_value llg, Llvm.global_initializer llg) with
-        | _, (External | External_weak) -> None
+        | GlobalVariable, Some llinit ->
-        | GlobalVariable, _ ->
             let siz = size_of x (Llvm.element_type llt) in
-            Some (xlate_value x (Llvm.global_initializer llg), siz)
+            let init = xlate_value x llinit in
+            Some (init, siz)
         | _ -> None
       in
       Global.mk ?init g typ loc

sledge/test/Makefile

@@ -42,7 +42,7 @@ $(MODEL_DIR)/cxxabi.bc : $(MODEL_DIR)/cxxabi.cpp
 	@(cd $(dir $@) && clang $(CLANG_ARGS) -I../llvm/projects/libcxxabi/include -I../llvm/projects/libcxxabi/src -c -emit-llvm cxxabi.cpp)
 
 # compile c to llvm bitcode
-%.bc : %.c $(MODEL_DIR)/cxxabi.bc
+%.bc : %.c
 	@(cd $(dir $*) && clang $(CLANG_ARGS) -c -emit-llvm $(notdir $*).c -o - | opt $(OPT_ARGS) -o $(notdir $*).bc)
 
 #  $(MODEL_DIR)/cxxabi.bc

sledge/test/exec/globals.c

@@ -0,0 +1,22 @@
+/*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+char* mutable_string = "a string";
+const char* immutable_string = "a string";
+
+int mutable_int = 0;
+const int immutable_int = 0;
+
+int main() {
+  int mi = mutable_int;
+  int imi = immutable_int;
+  char* c = mutable_string;
+  char a_char = *mutable_string;
+  char b_char = *immutable_string;
+
+  return 0;
+}