From f56f18350d3e526af5a0c4e3b1b117817900e032 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 18 Mar 2021 09:13:02 -0700 Subject: [PATCH] [pulse] bump base_fuel to 10 to avoid under-normalising formulas Summary: 10 seems better at no visible CPU cost. Not very scientific as this is only one data point, but neither was choosing 5 in the first place. Measurements on OpenSSL using Pulse.ISL: ``` $ time infer --pulse-only --scheduler callgraph -j 2 --pulse-report-latent-issues --pulse-isl | fuel | user time (s) | under-normalisation | latent issues | |------+---------------+---------------------+---------------| | 5 | 163 | 3074 | 160 | | 10 | 158 | 85 | 160 | | 15 | 174 | 32 | 160 | | 20 | 186 | 20 | 160 | ``` Reviewed By: skcho Differential Revision: D27156497 fbshipit-source-id: 1114b8677 --- infer/src/pulse/PulseFormula.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml index 2797538d7..ccaeb39e3 100644 --- a/infer/src/pulse/PulseFormula.ml +++ b/infer/src/pulse/PulseFormula.ml @@ -1204,7 +1204,7 @@ module Formula = struct (** an arbitrary value *) - let base_fuel = 5 + let base_fuel = 10 let solve_lin_eq new_eqs t1 t2 phi = solve_normalized_lin_eq ~fuel:base_fuel new_eqs (apply phi t1) (apply phi t2) phi