From babe25fd29d3d956b6f45847aa79d5d3cd0790f2 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Fri, 31 May 2019 14:19:23 -0700
Subject: [PATCH] [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 |  8 ++++----
 sledge/test/Makefile         |  2 +-
 sledge/test/exec/globals.c   | 22 ++++++++++++++++++++++
 3 files changed, 27 insertions(+), 5 deletions(-)
 create mode 100644 sledge/test/exec/globals.c

diff --git a/sledge/src/llair/frontend.ml b/sledge/src/llair/frontend.ml
index bd2e2a175..25968b7d4 100644
--- a/sledge/src/llair/frontend.ml
+++ b/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
-        | _, (External | External_weak) -> None
-        | GlobalVariable, _ ->
+        match (Llvm.classify_value llg, Llvm.global_initializer llg) with
+        | GlobalVariable, Some llinit ->
             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
diff --git a/sledge/test/Makefile b/sledge/test/Makefile
index ec9f69d42..5c55cafcc 100644
--- a/sledge/test/Makefile
+++ b/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
diff --git a/sledge/test/exec/globals.c b/sledge/test/exec/globals.c
new file mode 100644
index 000000000..800fb1eec
--- /dev/null
+++ b/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;
+}