Merge branch 'master' into issue-1373

src/analyses/apron/relationAnalysis.apron.ml

@@ -44,10 +44,10 @@ struct
     if ContextUtil.should_keep ~isAttr:GobContext ~keepOption:"ana.relation.context" ~removeAttr:"relation.no-context" ~keepAttr:"relation.context" fd then
       x
     else
-      D.bot () (* just like startstate, heterogeneous RD.bot () means top over empty set of variables *)
+      D.top ()
 
-  let exitstate  _ = { rel = RD.bot (); priv = Priv.startstate () }
-  let startstate _ = { rel = RD.bot (); priv = Priv.startstate () }
+  let exitstate  _ = { rel = RD.top (); priv = Priv.startstate () }
+  let startstate _ = { rel = RD.top (); priv = Priv.startstate () }
 
   (* Functions for manipulating globals as temporary locals. *)
 

src/analyses/apron/relationPriv.apron.ml

@@ -127,7 +127,7 @@ struct
     {st with rel = rel_local}
 
   let threadenter ask getg (st: relation_components_t): relation_components_t =
-    {rel = RD.bot (); priv = startstate ()}
+    {rel = RD.top (); priv = startstate ()}
 
   let iter_sys_vars getg vq vf = ()
   let invariant_vars ask getg st = []
@@ -489,7 +489,11 @@ struct
     in
     let get_mutex_inits = getg V.mutex_inits in
     let get_mutex_inits' = RD.keep_vars get_mutex_inits [g_var] in
-    RD.join get_mutex_global_g get_mutex_inits'
+    if not (RD.mem_var get_mutex_inits' g_var) then (* TODO: is this just a workaround for an escape bug? https://github.com/goblint/analyzer/pull/1354/files#r1498882657 *)
+      (* This is an escaped variable whose value was never side-effected to get_mutex_inits' *)
+      get_mutex_global_g
+    else
+      RD.join get_mutex_global_g get_mutex_inits'
 
   let get_mutex_global_g_with_mutex_inits_atomic ask getg =
     (* Unprotected invariant is one big relation. *)
@@ -527,12 +531,15 @@ struct
     else
       rel_local (* Keep write local as if it were protected by the atomic section. *)
 
-  let write_global ?(invariant=false) (ask: Q.ask) getg sideg (st: relation_components_t) g x: relation_components_t =
+  (** Like write global but has option to skip meet with current value, as the value will not have been side-effected to a useful location thus far *)
+  let write_global_internal ?(skip_meet=false)  ?(invariant=false) (ask: Q.ask) getg sideg (st: relation_components_t) g x: relation_components_t =
     let atomic = Param.handle_atomic && ask.f MustBeAtomic in
     let rel = st.rel in
     (* lock *)
     let rel =
-      if atomic && RD.mem_var rel (AV.global g) then
+      if skip_meet then
+        rel
+      else if atomic && RD.mem_var rel (AV.global g) then
         rel (* Read previous unpublished unprotected write in current atomic section. *)
       else if atomic then
         RD.meet rel (get_mutex_global_g_with_mutex_inits_atomic ask getg) (* Read unprotected invariant as full relation. *)
@@ -564,6 +571,9 @@ struct
       {st with rel = rel_local} (* Keep write local as if it were protected by the atomic section. *)
 
 
+  let write_global = write_global_internal ~skip_meet:false
+  let write_escape = write_global_internal ~skip_meet:true
+
   let lock ask getg (st: relation_components_t) m =
     let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in
     (* TODO: somehow actually unneeded here? *)
@@ -626,13 +636,17 @@ struct
         st
       else
         let rel = st.rel in
-        let rel_side = RD.keep_filter rel (fun var ->
+        (* Replace with remove_filter once issues are fixed *)
+        let g_vars = List.filter (fun var ->
             match AV.find_metadata var with
             | Some (Global _) -> true
             | _ -> false
-          )
+          ) (RD.vars rel)
         in
-        sideg V.mutex_inits rel_side;
+        let rel_side = RD.keep_vars rel g_vars in
+        (* If no globals are contained here, none need to be published *)
+        (* https://github.com/goblint/analyzer/pull/1354 *)
+        if g_vars <> [] then sideg V.mutex_inits rel_side;
         let rel_local = RD.remove_filter rel (fun var ->
             match AV.find_metadata var with
             | Some (Global g) -> is_unprotected ask g
@@ -662,11 +676,11 @@ struct
   let escape node ask getg sideg (st:relation_components_t) escaped : relation_components_t =
     let esc_vars = EscapeDomain.EscapedVars.elements escaped in
     let esc_vars = List.filter (fun v -> not v.vglob && RD.Tracked.varinfo_tracked v && RD.mem_var st.rel (AV.local v)) esc_vars in
-    let escape_one (x:varinfo) st = write_global ask getg sideg st x x in
+    let escape_one (x:varinfo) st = write_escape ask getg sideg st x x in
     List.fold_left (fun st v -> escape_one v st) st esc_vars
 
   let threadenter ask getg (st: relation_components_t): relation_components_t =
-    {rel = RD.bot (); priv = startstate ()}
+    {rel = RD.top (); priv = startstate ()}
 
   let init () = ()
   let finalize () = ()
@@ -799,7 +813,7 @@ struct
   let lock_get_m oct local_m get_m =
     let joined = LRD.join local_m get_m in
     if M.tracing then M.traceli "relationpriv" "lock_get_m:\n  get=%a\n  joined=%a\n" LRD.pretty get_m LRD.pretty joined;
-    let r = LRD.fold (fun _ -> RD.meet) joined (RD.bot ()) in (* bot is top with empty env *)
+    let r = LRD.fold (fun _ -> RD.meet) joined (RD.top ()) in
     if M.tracing then M.trace "relationpriv" "meet=%a\n" RD.pretty r;
     let r = RD.meet oct r in
     if M.tracing then M.traceu "relationpriv" "-> %a\n" RD.pretty r;
@@ -1220,7 +1234,7 @@ struct
 
   let threadenter ask getg (st: relation_components_t): relation_components_t =
     let _,lmust,l = st.priv in
-    {rel = RD.bot (); priv = (W.bot (),lmust,l)}
+    {rel = RD.top (); priv = (W.bot (),lmust,l)}
 
   let iter_sys_vars getg vq vf =
     match vq with

src/analyses/wrapperFunctionAnalysis.ml

@@ -141,9 +141,9 @@ module MallocWrapper : MCPSpec = struct
         if not (GobConfig.get_bool "dbg.full-output") && ThreadLifted.is_top t then
           Format.dprintf ""
         else
-          Format.dprintf "@tid:%s%t" (ThreadLifted.show t) uniq_count
+          Format.dprintf "@tid:%s" (ThreadLifted.show t)
       in
-      Format.asprintf "(alloc@sid:%s%t)" (Node.show_id node) tid
+      Format.asprintf "(alloc@sid:%s%t%t)" (Node.show_id node) tid uniq_count
   end
 
   module NodeVarinfoMap = RichVarinfo.BiVarinfoMap.Make(ThreadNode)

src/build-info/dune

@@ -27,6 +27,12 @@
   (mode (promote (until-clean) (only configOcaml.ml))) ; replace existing file in source tree, even if releasing (only overrides)
   (action (write-file %{target} "(* Automatically regenerated, changes do not persist! *)\nlet flambda = \"%{ocaml-config:flambda}\"")))
 
+(rule
+  (target configDatetime.ml)
+  (mode (promote (until-clean) (only configDatetime.ml))) ; replace existing file in source tree, even if releasing (only overrides)
+  (deps (universe)) ; do not cache, always regenerate
+  (action (pipe-stdout (bash "date +\"%Y-%m-%dT%H:%M:%S\" || echo \"n/a\"") (with-stdout-to %{target} (bash "xargs printf '(* Automatically regenerated, changes do not persist! *)\nlet datetime = \"%s\"'")))))
+
 (env
   (_
     (flags (:standard -w -no-cmx-file)))) ; suppress warning from flambda compiler bug: https://github.com/ocaml/dune/issues/3277

src/build-info/goblint_build_info.ml

@@ -32,3 +32,6 @@ let version =
 
 (** Statically linked libraries with versions. *)
 let statically_linked_libraries = Dune_build_info.statically_linked_libraries
+
+(** Build date and time. *)
+let datetime = ConfigDatetime.datetime

src/cdomain/value/cdomains/floatDomain.ml

@@ -5,6 +5,23 @@ open FloatOps
 
 exception ArithmeticOnFloatBot of string
 
+(** Define records that hold mutable variables representing different Configuration values.
+  * These values are used to keep track of whether or not the corresponding Config values are en-/disabled  *)
+type ana_float_config_values = {
+  mutable evaluate_math_functions : bool option;
+}
+
+let ana_float_config: ana_float_config_values = {
+  evaluate_math_functions = None;
+}
+
+let get_evaluate_math_functions () =
+  if ana_float_config.evaluate_math_functions = None then
+    ana_float_config.evaluate_math_functions <- Some (GobConfig.get_bool "ana.float.evaluate_math_functions");
+  Option.get ana_float_config.evaluate_math_functions
+
+let reset_lazy () = ana_float_config.evaluate_math_functions <- None
+
 module type FloatArith = sig
   type t
 
@@ -273,12 +290,12 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct
     | _ -> Bot
 
   (** [widen x y] assumes [leq x y]. Solvers guarantee this by calling [widen old (join old new)]. *)
-  let widen v1 v2 = (**TODO: support 'threshold_widening' option *)
+  let widen v1 v2 = (* TODO: support 'threshold_widening' option *)
     match v1, v2 with
     | Top, _ | _, Top -> Top
     | Bot, v | v, Bot -> v
     | Interval (l1, h1), Interval (l2, h2) ->
-      (**If we widen and we know that neither interval contains +-inf or nan, it is ok to widen only to +-max_float,
+      (* If we widen and we know that neither interval contains +-inf or nan, it is ok to widen only to +-max_float,
          because a widening with +-inf/nan will always result in the case above -> Top *)
       let low = if l1 <= l2 then l1 else Float_t.lower_bound in
       let high = if h1 >= h2 then h1 else Float_t.upper_bound in
@@ -289,7 +306,7 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct
     | _ -> Top
 
   let narrow v1 v2 =
-    match v1, v2 with (**we cannot distinguish between the lower bound beeing -inf or the upper bound beeing inf. Also there is nan *)
+    match v1, v2 with (* we cannot distinguish between the lower bound beeing -inf or the upper bound beeing inf. Also there is nan *)
     | Bot, _ | _, Bot -> Bot
     | Top, _ -> v2
     | Interval (l1, h1), Interval (l2, h2) ->
@@ -623,15 +640,79 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct
       else
         unknown_IInt ()
 
-  (**it seems strange not to return an explicit 1 for negative numbers, but in c99 signbit is defined as: *)
-  (**<<The signbit macro returns a nonzero value if and only if the sign of its argument value is negative.>> *)
+  (**it seems strange not to return an explicit 1 for negative numbers, but in c99 signbit is defined as:
+   **<<The signbit macro returns a nonzero value if and only if the sign of its argument value is negative.>> *)
   let eval_signbit = function
     | (_, h) when h < Float_t.zero -> true_nonZero_IInt ()
     | (l, _) when l > Float_t.zero -> false_zero_IInt ()
-    | _ -> unknown_IInt () (**any interval containing zero has to fall in this case, because we do not distinguish between 0. and -0. *)
-
-  (**This Constant overapproximates pi to use as bounds for the return values of trigonometric functions *)
-  let overapprox_pi = 3.1416
+    | _ -> unknown_IInt () (* any interval containing zero has to fall in this case, because we do not distinguish between 0. and -0. *)
+
+  (** returns the max of the given mfun once computed with rounding mode Up and once with rounding mode down*)
+  let safe_mathfun_up mfun f = max (mfun Down f) (mfun Up f)
+  (** returns the min of the given mfun once computed with rounding mode Up and once with rounding mode down*)
+  let safe_mathfun_down mfun f = min (mfun Down f) (mfun Up f)
+
+  (** This function does two things: 
+   ** 1. projects l and h onto the interval [0, k*pi] (for k = 2 this is the phase length of sin/cos, for k = 1 it is the phase length of tan)
+   ** 2. compresses/transforms the interval [0, k*pi] to the interval [0, 1] to ease further computations
+   ** i.e. the function computes dist = distance, l'' = (l/(k*pi)) - floor(l/(k*pi)), h'' = (h/(k*pi)) - floor(h/(k*pi))*)
+  let project_and_compress l h k =
+    let ft_over_kpi = (Float_t.mul Up (Float_t.of_float Up k) Float_t.pi) in
+    let ft_under_kpi = (Float_t.mul Down (Float_t.of_float Down k) Float_t.pi) in
+    let l' =
+      if l >= Float_t.zero then (Float_t.div Down l ft_over_kpi)
+      else (Float_t.div Down l ft_under_kpi)
+    in
+    let h' =
+      if h >= Float_t.zero then (Float_t.div Up h ft_under_kpi)
+      else (Float_t.div Up h ft_over_kpi)
+    in
+    let dist = (Float_t.sub Up h' l') in
+    let l'' =
+      if l' >= Float_t.zero then
+        Float_t.sub Down l' (Float_t.of_float Up (Z.to_float (Float_t.to_big_int l')))
+      else
+        Float_t.sub Down l' (Float_t.of_float Up (Z.to_float (Z.pred (Float_t.to_big_int l'))))
+    in
+    let h'' =
+      if h' >= Float_t.zero then
+        Float_t.sub Up h' (Float_t.of_float Down (Z.to_float (Float_t.to_big_int h')))
+      else
+        Float_t.sub Up h' (Float_t.of_float Down (Z.to_float (Z.pred (Float_t.to_big_int h'))))
+    in
+    (dist, l'', h'')
+
+  let eval_cos_cfun l h =
+    let (dist, l'', h'') = project_and_compress l h 2. in
+    if Messages.tracing then Messages.trace "CstubsTrig" "cos: dist %s; l'' %s; h'' %s\n" (Float_t.to_string dist) (Float_t.to_string l'') (Float_t.to_string h'');
+    if (dist <= Float_t.of_float Down 0.5) && (h'' <= Float_t.of_float Down 0.5) && (l'' <= h'') then
+      (* case: monotonic decreasing interval*)
+      Interval (safe_mathfun_down Float_t.cos h, safe_mathfun_up Float_t.cos l)
+    else if (dist <= Float_t.of_float Down 0.5) && (l'' >= Float_t.of_float Up 0.5) && (l'' <= h'') then
+      (* case: monotonic increasing interval*)
+      Interval (safe_mathfun_down Float_t.cos l, safe_mathfun_up Float_t.cos h)
+    else if (dist <= Float_t.of_float Down 1.) && (l'' <= h'') then
+      (* case: contains at most one minimum*)
+      Interval (Float_t.of_float Down (-.1.), max (safe_mathfun_up Float_t.cos l) (safe_mathfun_up Float_t.cos h))
+    else if (dist <= Float_t.of_float Down 1.) && (l'' >= Float_t.of_float Up 0.5) && (h'' <= Float_t.of_float Down 0.5) then
+      (* case: contains at most one maximum*)
+      Interval (min (safe_mathfun_down Float_t.cos l) (safe_mathfun_down Float_t.cos h), Float_t.of_float Up 1.)
+    else
+      of_interval (-. 1., 1.)
+
+  let eval_sin_cfun l h =
+    let lcos = Float_t.sub Down l (Float_t.div Up Float_t.pi (Float_t.of_float Down 2.0)) in
+    let hcos = Float_t.sub Up h (Float_t.div Down Float_t.pi (Float_t.of_float Up 2.0)) in
+    eval_cos_cfun lcos hcos
+
+  let eval_tan_cfun l h =
+    let (dist, l'', h'') = project_and_compress l h 1. in
+    if Messages.tracing then Messages.trace "CstubsTrig" "tan: dist %s; l'' %s; h'' %s\n" (Float_t.to_string dist) (Float_t.to_string l'') (Float_t.to_string h'');
+    if (dist <= Float_t.of_float Down 1.) && (Bool.not ((l'' <= Float_t.of_float Up 0.5) && (h'' >= Float_t.of_float Up 0.5))) then
+      (* case: monotonic increasing interval*)
+      Interval (safe_mathfun_down Float_t.tan l, safe_mathfun_up Float_t.tan h)
+    else
+      top ()
 
   let eval_fabs = function
     | (l, h) when l > Float_t.zero -> Interval (l, h)
@@ -656,39 +737,51 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct
 
   let eval_acos = function
     | (l, h) when l = h && l = Float_t.of_float Nearest 1. -> of_const 0. (*acos(1) = 0*)
-    | (l, h) ->
-      if l < (Float_t.of_float Down (-.1.)) || h > (Float_t.of_float Up 1.) then
-        Messages.warn ~category:Messages.Category.Float "Domain error might occur: acos argument might be outside of [-1., 1.]";
-      of_interval (0., (overapprox_pi)) (**could be more exact *)
+    | (l, h) when l < (Float_t.of_float Down (-.1.)) || h > (Float_t.of_float Up 1.) ->
+      Messages.warn ~category:Messages.Category.Float "Domain error might occur: acos argument might be outside of [-1., 1.]";
+      Interval (Float_t.of_float Down 0., Float_t.pi)
+    | (l, h) when get_evaluate_math_functions () ->
+      norm @@ Interval (safe_mathfun_down Float_t.acos h, safe_mathfun_up Float_t.acos l) (* acos is monotonic decreasing in [-1, 1]*)
+    | _ -> Interval (Float_t.of_float Down 0., Float_t.pi)
 
   let eval_asin = function
     | (l, h) when l = h && l = Float_t.zero -> of_const 0. (*asin(0) = 0*)
-    | (l, h) ->
-      if l < (Float_t.of_float Down (-.1.)) || h > (Float_t.of_float Up 1.) then
-        Messages.warn ~category:Messages.Category.Float "Domain error might occur: asin argument might be outside of [-1., 1.]";
-      div (of_interval ((-. overapprox_pi), overapprox_pi)) (of_const 2.) (**could be more exact *)
+    | (l, h) when l < (Float_t.of_float Down (-.1.)) || h > (Float_t.of_float Up 1.) ->
+      Messages.warn ~category:Messages.Category.Float "Domain error might occur: asin argument might be outside of [-1., 1.]";
+      div (Interval (Float_t.neg Float_t.pi, Float_t.pi)) (of_const 2.)
+    | (l, h) when get_evaluate_math_functions () ->
+      norm @@ Interval (safe_mathfun_down Float_t.asin l, safe_mathfun_up Float_t.asin h) (* asin is monotonic increasing in [-1, 1]*)
+    | _ -> div (Interval (Float_t.neg Float_t.pi, Float_t.pi)) (of_const 2.)
 
   let eval_atan = function
     | (l, h) when l = h && l = Float_t.zero -> of_const 0. (*atan(0) = 0*)
-    | _ -> div (of_interval ((-. overapprox_pi), overapprox_pi)) (of_const 2.) (**could be more exact *)
+    | (l, h) when get_evaluate_math_functions () ->
+      norm @@ Interval (safe_mathfun_down Float_t.atan l, safe_mathfun_up Float_t.atan h) (* atan is monotonic increasing*)
+    | _ -> div (Interval (Float_t.neg Float_t.pi, Float_t.pi)) (of_const 2.)
 
   let eval_cos = function
     | (l, h) when l = h && l = Float_t.zero -> of_const 1. (*cos(0) = 1*)
-    | _ -> of_interval (-. 1., 1.) (**could be exact for intervals where l=h, or even for Interval intervals *)
+    | (l, h) when get_evaluate_math_functions () ->
+      norm @@ eval_cos_cfun l h
+    | _ -> of_interval (-. 1., 1.)
 
   let eval_sin = function
     | (l, h) when l = h && l = Float_t.zero -> of_const 0. (*sin(0) = 0*)
-    | _ -> of_interval (-. 1., 1.) (**could be exact for intervals where l=h, or even for some intervals *)
+    | (l, h) when get_evaluate_math_functions () ->
+      norm @@ eval_sin_cfun l h
+    | _ -> of_interval (-. 1., 1.)
 
   let eval_tan = function
     | (l, h) when l = h && l = Float_t.zero -> of_const 0. (*tan(0) = 0*)
-    | _ -> top () (**could be exact for intervals where l=h, or even for some intervals *)
+    | (l, h) when get_evaluate_math_functions () ->
+      norm @@ eval_tan_cfun l h
+    | _ -> top ()
 
   let eval_sqrt = function
     | (l, h) when l = Float_t.zero && h = Float_t.zero -> of_const 0.
-    | (l, h) when l >= Float_t.zero ->
-      let low = Float_t.sqrt Down l in
-      let high = Float_t.sqrt Up h in
+    | (l, h) when l >= Float_t.zero && get_evaluate_math_functions () ->
+      let low = safe_mathfun_down Float_t.sqrt l in
+      let high = safe_mathfun_up Float_t.sqrt h in
       Interval (low, high)
     | _ -> top ()
 

src/cdomain/value/cdomains/floatDomain.mli

@@ -4,6 +4,8 @@ open GoblintCil
 
 exception ArithmeticOnFloatBot of string
 
+val reset_lazy: unit -> unit
+
 module type FloatArith = sig
   type t
 

src/cdomains/apron/affineEqualityDomain.apron.ml

@@ -305,9 +305,9 @@ struct
 
   let is_bot_env t = t.d = None
 
-  let top () = failwith "D.top ()"
+  let top () = {d = Some (Matrix.empty ()); env = Environment.make [||] [||]}
 
-  let is_top _ = false
+  let is_top t = Environment.equal empty_env t.env && GobOption.exists Matrix.is_empty t.d
 
   let is_top_env t = (not @@ Environment.equal empty_env t.env) && GobOption.exists Matrix.is_empty t.d
 

src/cdomains/apron/apronDomain.apron.ml

@@ -666,14 +666,15 @@ struct
 
   let empty_env = Environment.make [||] [||]
 
+  (* top and bottom over the empty environment are different, pending  https://github.com/goblint/analyzer/issues/1380 *)
   let bot () =
-    top_env empty_env
+    bot_env empty_env
 
   let top () =
-    failwith "D2.top"
+    top_env empty_env
 
-  let is_bot = equal (bot ())
-  let is_top _ = false
+  let is_bot x = equal (bot ()) x
+  let is_top x = equal (top ()) x
 
   let strengthening_enabled = GobConfig.get_bool "ana.apron.strengthening"