New Analysis combining Linear Two-Variable Equalities with other domains

src/analyses/apron/linearTwoVarEqualityAnalysisPentagon.apron.ml

@@ -0,0 +1,40 @@
+(** {{!RelationAnalysis} Relational integer value analysis} using an OCaml implementation of the linear two-variable equalities domain ([lin2vareq]).
+
+    @see <http://doi.acm.org/10.1145/2049706.2049710> A. Flexeder, M. Petter, and H. Seidl Fast Interprocedural Linear Two-Variable Equalities. *)
+
+open Analyses
+include RelationAnalysis
+
+module NoIneq = LinearTwoVarEqualityDomainPentagon.D2(RepresentantDomains.NoInequalties)
+module PentagonIneq = LinearTwoVarEqualityDomainPentagon.D2(RepresentantDomains.InequalityFunctor(RepresentantDomains.PentagonCoeffs))
+module PentagonOffsetIneq = LinearTwoVarEqualityDomainPentagon.D2(RepresentantDomains.InequalityFunctor(RepresentantDomains.PentagonOffsetCoeffs))
+module FullIneq = LinearTwoVarEqualityDomainPentagon.D2(RepresentantDomains.InequalityFunctor(RepresentantDomains.TwoVarInequalitySet))
+
+let spec_module: (module MCPSpec) Lazy.t =
+  lazy (
+    let (module AD) = match GobConfig.get_string "ana.lin2vareq_p.inequalities" with 
+      | "none" -> (module NoIneq : RelationDomain.RD)
+      | "pentagon" -> (module PentagonIneq : RelationDomain.RD)
+      | "pentagon_offset" -> (module PentagonOffsetIneq : RelationDomain.RD)
+      | _ ->  (module FullIneq : RelationDomain.RD) (*Other options differ only in the limit function*)
+    in
+    let module Priv = (val RelationPriv.get_priv ()) in
+    let module Spec =
+    struct
+      include SpecFunctor (Priv) (AD) (RelationPrecCompareUtil.DummyUtil)
+      let name () = "lin2vareq_p"
+    end
+    in
+    (module Spec)
+  )
+
+let get_spec (): (module MCPSpec) =
+  Lazy.force spec_module
+
+let after_config () =
+  let module Spec = (val get_spec ()) in
+  MCP.register_analysis (module Spec : MCPSpec);
+  GobConfig.set_string "ana.path_sens[+]"  (Spec.name ())
+
+let _ =
+  AfterConfig.register after_config

src/analyses/apron/linearTwoVarEqualityAnalysisPentagon.no-apron.ml

@@ -0,0 +1,3 @@
+(* This analysis is empty on purpose. It serves only as an alternative dependency
+   in cases where the actual domain can't be used because of a missing library.
+   It was added because we don't want to fully depend on Apron. *)

src/analyses/apron/relationAnalysis.apron.ml

@@ -559,8 +559,8 @@ struct
       Priv.thread_join ~force:true ask man.global id st
     | Rand, _ ->
       Option.map_default (fun lv ->
-         let st = invalidate_one ask man st lv in
-         assert_fn {man with local = st} (BinOp (Ge, Lval lv, zero, intType)) true
+          let st = invalidate_one ask man st lv in
+          assert_fn {man with local = st} (BinOp (Ge, Lval lv, zero, intType)) true
         ) st r
     | _, _ ->
       let st' = special_unknown_invalidate man f args in

src/analyses/base.ml

@@ -202,21 +202,23 @@ struct
     | Mult -> ID.mul
     | Div ->
       fun x y ->
-        (match ID.equal_to Z.zero y with
-         | `Eq ->
-           M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of division is zero"
-         | `Top ->
-           M.warn ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of division might be zero"
-         | `Neq -> ());
+        if not !AnalysisState.executing_speculative_computations then 
+          (match ID.equal_to Z.zero y with
+           | `Eq ->
+             M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of division is zero"
+           | `Top ->
+             M.warn ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of division might be zero"
+           | `Neq -> ());
         ID.div x y
     | Mod ->
       fun x y ->
-        (match ID.equal_to Z.zero y with
-         | `Eq ->
-           M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of modulo is zero"
-         | `Top ->
-           M.warn ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of modulo might be zero"
-         | `Neq -> ());
+        if not !AnalysisState.executing_speculative_computations then 
+          (match ID.equal_to Z.zero y with
+           | `Eq ->
+             M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of modulo is zero"
+           | `Top ->
+             M.warn ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of modulo might be zero"
+           | `Neq -> ());
         ID.rem x y
     | Lt -> ID.lt
     | Gt -> ID.gt

src/analyses/baseInvariant.ml

@@ -286,7 +286,7 @@ struct
     let inv_bin_int (a, b) ikind c op =
       let warn_and_top_on_zero x =
         if GobOption.exists (Z.equal Z.zero) (ID.to_int x) then
-          (M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Must Undefined Behavior: Second argument of div or mod is 0, continuing with top";
+          (if not !AnalysisState.executing_speculative_computations then  M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Must Undefined Behavior: Second argument of div or mod is 0, continuing with top";
            ID.top_of ikind)
         else
           x

src/autoTune.ml

@@ -248,12 +248,12 @@ let focusOnMemSafetySpecification () =
 let focusOnTermination (spec: Svcomp.Specification.t) =
   match spec with
   | Termination ->
-    let terminationAnas = ["threadflag"; "apron"] in
+    let terminationAnas = ["threadflag"; get_string "ana.autotune.extraTerminationDomain"] in
     enableAnalyses "Specification: Termination" "termination analyses" terminationAnas;
     set_string "sem.int.signed_overflow" "assume_none";
     set_bool "ana.int.interval" true;
-    set_string "ana.apron.domain" "polyhedra"; (* TODO: Needed? *)
-    ()
+    if get_string "ana.autotune.extraTerminationDomain" = "apron" then 
+      set_string "ana.apron.domain" "polyhedra"; (* TODO: Needed? *)
   | _ -> ()
 
 let focusOnTermination () =

src/cdomain/value/cdomains/int/congruenceDomain.ml

@@ -1,8 +1,11 @@
 open IntDomain0
 open GoblintCil
 
+module type Norm = sig
+  val normalize : ikind -> (Z.t * Z.t) option -> (Z.t * Z.t) option
+end
 
-module Congruence : S with type int_t = Z.t and type t = (Z.t * Z.t) option =
+module CongruenceFunctor (Norm : Norm): S with type int_t = Z.t and type t = (Z.t * Z.t) option =
 struct
   let name () = "congruences"
   type int_t = Z.t
@@ -24,22 +27,7 @@ struct
   let ( |: ) a b =
     if a =: Z.zero then false else (b %: a) =: Z.zero
 
-  let normalize ik x =
-    match x with
-    | None -> None
-    | Some (c, m) ->
-      if m =: Z.zero then
-        if should_wrap ik then
-          Some (Size.cast ik c, m)
-        else
-          Some (c, m)
-      else
-        let m' = Z.abs m in
-        let c' = c %: m' in
-        if c' <: Z.zero then
-          Some (c' +: m', m')
-        else
-          Some (c' %: m', m')
+  let normalize = Norm.normalize
 
   let range ik = Size.range ik
 
@@ -540,3 +528,52 @@ struct
 
   let project ik p t = t
 end
+
+module Wrapping : Norm = struct
+
+  let (%:) = Z.rem
+  let (=:) = Z.equal
+  let (+:) = Z.add
+  let (<:) x y = Z.compare x y < 0
+
+  let normalize ik x =
+    match x with
+    | None -> None
+    | Some (c, m) ->
+      if m =: Z.zero then
+        if should_wrap ik then
+          Some (Size.cast ik c, m)
+        else
+          Some (c, m)
+      else
+        let m' = Z.abs m in
+        let c' = c %: m' in
+        if c' <: Z.zero then
+          Some (c' +: m', m')
+        else
+          Some (c' %: m', m')
+end
+
+module NoWrapping : Norm = struct
+
+  let (%:) = Z.rem
+  let (=:) = Z.equal
+  let (+:) = Z.add
+  let (<:) x y = Z.compare x y < 0
+
+  let normalize ik x =
+    match x with
+    | None -> None
+    | Some (c, m) ->
+      if m =: Z.zero then
+        Some (c, m)
+      else
+        let m' = Z.abs m in
+        let c' = c %: m' in
+        if c' <: Z.zero then
+          Some (c' +: m', m')
+        else
+          Some (c' %: m', m')
+end
+
+module Congruence = CongruenceFunctor(Wrapping)

src/cdomain/value/cdomains/int/intDomTuple.ml

@@ -124,6 +124,7 @@ module IntDomTupleImpl = struct
   let ending ?(suppress_ovwarn=false) ik = create2_ovc ik { fi2_ovc = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.ending ~suppress_ovwarn ik }
   let of_interval ?(suppress_ovwarn=false) ik = create2_ovc ik { fi2_ovc = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_interval ~suppress_ovwarn ik }
   let of_congruence ik = create2 { fi2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_congruence ik }
+  let to_congruence (_,_,_,c,_,_) = match c with Some c -> c | None -> I4.top_of IChar (*ikind is ignored, so choose an arbitrary one *) 
   let of_bitfield ik = create2 { fi2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_bitfield ik }
 
   let refine_with_congruence ik ((a, b, c, d, e, f) : t) (cong : (int_t * int_t) option) : t=
@@ -556,6 +557,8 @@ struct
   let no_intervalSet (x: I.t) = {x with v = IntDomTupleImpl.no_intervalSet x.v}
 
   let no_bitfield (x: I.t) = {x with v = IntDomTupleImpl.no_bitfield x.v}
+
+  let to_congruence (x: I.t) = IntDomTupleImpl.to_congruence x.v
 end
 
 let of_const (i, ik, str) = IntDomTuple.of_int ik i

src/cdomain/value/cdomains/int/intervalDomain.ml

@@ -1,28 +1,30 @@
 open IntDomain0
 
-module IntervalFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) option =
-struct
-  let name () = "intervals"
-  type int_t = Ints_t.t
-  type t = (Ints_t.t * Ints_t.t) option [@@deriving eq, ord, hash]
-  module IArith = IntervalArith (Ints_t)
+(**TODO Better Naming!*)
+module type BoundedIntOps = sig
+  include IntOps.IntOps
+
+  type t_interval = (t * t) option
 
+  val range : GoblintCil.ikind -> t * t
+  val top_of : GoblintCil.ikind -> t_interval
+  val bot_of : GoblintCil.ikind -> t_interval
+
+
+  val norm : ?suppress_ovwarn:bool -> ?cast:bool -> GoblintCil.ikind -> t_interval -> t_interval * overflow_info
+end
+
+module Bounded (Ints_t : IntOps.IntOps): BoundedIntOps with type t = Ints_t.t and type t_interval = (Ints_t.t * Ints_t.t) option = struct
+  include Ints_t
+  type t_interval = (Ints_t.t * Ints_t.t) option
   let range ik = BatTuple.Tuple2.mapn Ints_t.of_bigint (Size.range ik)
 
   let top_of ik = Some (range ik)
-  let bot () = None
-  let bot_of ik = bot () (* TODO: improve *)
+  let bot_of ik = None (* TODO: improve *)
 
-  let show = function None -> "bottom" | Some (x,y) -> "["^Ints_t.to_string x^","^Ints_t.to_string y^"]"
 
-  include Std (struct type nonrec t = t let name = name let top_of = top_of let bot_of = bot_of let show = show let equal = equal end)
 
-  let equal_to i = function
-    | None -> failwith "unsupported: equal_to with bottom"
-    | Some (a, b) ->
-      if a = b && b = i then `Eq else if Ints_t.compare a i <= 0 && Ints_t.compare i b <=0 then `Top else `Neq
-
-  let norm ?(suppress_ovwarn=false) ?(cast=false) ik : (t -> t * overflow_info) = function None -> (None, {underflow=false; overflow=false}) | Some (x,y) ->
+  let norm ?(suppress_ovwarn=false) ?(cast=false) ik : (t_interval -> t_interval * overflow_info) = function None -> (None, {underflow=false; overflow=false}) | Some (x,y) ->
     if Ints_t.compare x y > 0 then
       (None,{underflow=false; overflow=false})
     else (
@@ -58,6 +60,31 @@ struct
       (v, ov_info)
     )
 
+end
+
+module BoundedIntervalFunctor (Ints_t : BoundedIntOps): SOverflow with type int_t = Ints_t.t and type t = Ints_t.t_interval =
+struct
+  let name () = "intervals bounds injected"
+  type int_t = Ints_t.t
+  type t = (Ints_t.t * Ints_t.t) option [@@deriving eq, ord, hash]
+  module IArith = IntervalArith (Ints_t)
+
+  let range = Ints_t.range
+  let top_of = Ints_t.top_of
+  let norm = Ints_t.norm
+  let bot_of = Ints_t.bot_of
+
+  let bot () = None
+
+  let show = function None -> "bottom" | Some (x,y) -> "["^Ints_t.to_string x^","^Ints_t.to_string y^"]"
+
+  include Std (struct type nonrec t = t let name = name let top_of = top_of let bot_of = bot_of let show = show let equal = equal end)
+
+  let equal_to i = function
+    | None -> failwith "unsupported: equal_to with bottom"
+    | Some (a, b) ->
+      if a = b && b = i then `Eq else if Ints_t.compare a i <= 0 && Ints_t.compare i b <=0 then `Top else `Neq
+
   let leq (x:t) (y:t) =
     match x, y with
     | None, _ -> true
@@ -444,5 +471,7 @@ struct
   let project ik p t = t
 end
 
+module IntervalFunctor (Ints_t : IntOps.IntOps) = BoundedIntervalFunctor (Bounded(Ints_t))
+
 module Interval = IntervalFunctor (IntOps.BigIntOps)
 module Interval32 = IntDomWithDefaultIkind (IntDomLifter (SOverflowUnlifter (IntervalFunctor (IntOps.Int64Ops)))) (IntIkind)

src/cdomain/value/cdomains/intDomain_intf.ml

@@ -381,6 +381,7 @@ sig
     val no_intervalSet: t -> t
     val no_bitfield: t -> t
     val ikind: t -> ikind
+    val to_congruence : t -> (Z.t * Z.t) option
   end
 
   val of_const: Z.t * Cil.ikind * string option -> IntDomTuple.t

src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml

@@ -97,8 +97,9 @@ module EqualitiesConjunction = struct
   (** add/remove new variables to domain with particular indices; translates old indices to keep consistency
       add if op = (+), remove if op = (-)
       the semantics of indexes can be retrieved from apron: https://antoinemine.github.io/Apron/doc/api/ocaml/Dim.html *)
-  let modify_variables_in_domain (dim,map) indexes op =
-    if Array.length indexes = 0 then (dim,map) else
+
+  let modify_variables_in_domain_general map map_value indexes op =
+    if Array.length indexes = 0 then map else
       let offsetlist = Array.to_list indexes in
       let rec bumpvar delta i = function (* bump the variable i by delta; find delta by counting indices in offsetlist until we reach a larger index then our current parameter *)
         | head::rest when i>=head -> bumpvar (delta+1) i rest (* rec call even when =, in order to correctly interpret double bumps *)
@@ -115,13 +116,18 @@ module EqualitiesConjunction = struct
                IntHashtbl.add h x r;
                r)
       in
-      let rec bumpentry k (refvar,offset,divi) = function (* directly bumps lhs-variable during a run through indexes, bumping refvar explicitly with a new lookup in indexes *)
+      let rec bumpentry k value = function (* directly bumps lhs-variable during a run through indexes, bumping refvar explicitly with a new lookup in indexes *)
 
-        | (tbl,delta,head::rest) when k>=head            -> bumpentry k (refvar,offset,divi) (tbl,delta+1,rest) (* rec call even when =, in order to correctly interpret double bumps *)
-        | (tbl,delta,lyst) (* k<head or lyst=[] *) -> (IntMap.add (op k delta) (BatOption.map (fun (c,v) -> (c,memobumpvar v)) refvar,offset,divi) tbl, delta, lyst)
+        | (tbl,delta,head::rest) when k>=head            -> bumpentry k value (tbl,delta+1,rest) (* rec call even when =, in order to correctly interpret double bumps *)
+        | (tbl,delta,lyst) (* k<head or lyst=[] *) -> (IntMap.add (op k delta) (map_value memobumpvar value) tbl, delta, lyst)
       in
       let (a,_,_) = IntMap.fold bumpentry map (IntMap.empty,0,offsetlist) in (* Build new map during fold with bumped key/vals *)
-      (op dim (Array.length indexes), a)
+      a
+
+  let modify_variables_in_domain (dim,map) indexes op =
+    let map_value bumpvar (refvar,offset,divi) = (BatOption.map (fun (c,v) -> (c,bumpvar v)) refvar,offset,divi) in
+    (op dim (Array.length indexes), modify_variables_in_domain_general map map_value indexes op)
+
 
   let modify_variables_in_domain m cols op = let res = modify_variables_in_domain m cols op in if M.tracing then
       M.tracel "modify_dims" "dimarray bumping with (fun x -> x + %d) at positions [%s] in { %s } -> { %s }"