[sledge] Drop globals with appending linkage and size 0

Summary:
Some globals have 'appending' linkage, where linking modules results
in appending the arrays from each module. These can appear even when
empty, leading to useless and somewhat troublesome 0-length arrays. So
drop them.

Reviewed By: ngorogiannis

Differential Revision: D17801927

fbshipit-source-id: d2dc180d7

sledge/src/llair/frontend.ml

@@ -1423,7 +1423,12 @@ let translate ~models ~fuzzer ~internalize : string list -> Llair.t =
   let x = {llcontext; llmodule; lldatalayout} in
   let globals =
     Llvm.fold_left_globals
-      (fun globals llg -> xlate_global x llg :: globals)
+      (fun globals llg ->
+        if
+          Poly.equal (Llvm.linkage llg) Appending
+          && Llvm.(array_length (element_type (type_of llg))) = 0
+        then globals
+        else xlate_global x llg :: globals )
       [] llmodule
   in
   let functions =