[sledge] Model `folly::usingJEMalloc()`

Summary:
The actual implementation of folly::usingJEMalloc() tests if malloc is
jemalloc using internal knowledge of the jemalloc implemenation of
malloc. This internal behavior is not reflected in the analyzer's
spec, so the detection fails.

Additionally, folly::usingJEMalloc is implemented using mallctl to
query internal state of jemalloc. Depending on the key string passed
to mallctl, it might return a pointer to jemalloc internal state, or a
scalar, which means that the spec needs to essentially allocate that
state in those cases.

Since the jemalloc detection fails, and the analyzer is not always
able to reason precisely about string equality, this diff models
folly::usingJEMalloc directly (as nondet).

Reviewed By: kren1

Differential Revision: D16059776

fbshipit-source-id: 7e7156d7d

sledge/src/symbheap/exec.ml

@@ -706,4 +706,9 @@ let intrinsic ~skip_throw :
    *)
   | Some _, "__cxa_allocate_exception", [_] when skip_throw ->
       skip (Sh.false_ pre.us)
+  (*
+   * folly
+   *)
+  (* bool folly::usingJEMalloc() *)
+  | Some _, "_ZN5folly13usingJEMallocEv", [] -> skip pre
   | _ -> None