From 7f423f7fa10eb609b4e7a212461b92253fcccc05 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 17 Jul 2019 15:14:17 -0700 Subject: [PATCH] [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 | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml index c4f522a93..a7d16cf78 100644 --- a/sledge/src/symbheap/exec.ml +++ b/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