From 007c044d92917afc86cfbf54d521bf45b88cd182 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 26 Jun 2019 10:27:46 -0700 Subject: [PATCH] [HIL] add warning about HIL unsoundness Summary: In light of Pulse's misadventures with HIL, leave a warning for future checkers writers. Comment mostly taken from summary of D15824961. Reviewed By: ngorogiannis Differential Revision: D16005392 fbshipit-source-id: 805f17584 --- infer/src/absint/LowerHil.mli | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/infer/src/absint/LowerHil.mli b/infer/src/absint/LowerHil.mli index 8bbfa5e58..e234bc657 100644 --- a/infer/src/absint/LowerHil.mli +++ b/infer/src/absint/LowerHil.mli @@ -44,7 +44,25 @@ module type S = sig (** compute and return the postcondition for the given procedure starting from [initial]. *) end -(** Wrapper around Interpreter to prevent clients from having to deal with IdAccessPathMapDomain *) +(** Wrapper around Interpreter to prevent clients from having to deal with IdAccessPathMapDomain. + + CAVEAT: the translation does not attempt to preserve the semantics in the case where side-effects + happen between an assignment to a logical variable and the assignement of that logical variable + to a program variable. For instance the following SIL program + + n$0 = *&x.f + _ = delete(&x) + *&y = n$0 + + becomes + + _ = delete(&x) + *&y = *&x.f + + The latter is a use-after-delete of &x whereas the original SIL program is well behaved. + + Only use HIL if that is not something your checker needs to care about. + *) module MakeAbstractInterpreterWithConfig (MakeAbstractInterpreter : AbstractInterpreter.Make) (HilConfig : HilConfig)