Merge pull request #749 from goblint/remove-inthack

Remove `inthack` and fix i-lock star display

Author: sim642

src/analyses/symbLocks.ml

@@ -1,8 +1,11 @@
-(** Symbolic lock-sets for use in per-element patterns. *)
+(** Symbolic lock-sets for use in per-element patterns.
+
+    See Section 5 and 6 in https://dl.acm.org/doi/10.1145/2970276.2970337 for more details. *)
 
 module LF = LibraryFunctions
 module LP = SymbLocksDomain.LockingPattern
 module Exp = SymbLocksDomain.Exp
+module ILock = SymbLocksDomain.ILock
 module VarEq = VarEq.Spec
 
 module PS = SetDomain.ToppedSet (LP) (struct let topname = "All" end)
@@ -106,22 +109,14 @@ struct
       ctx.local
 
 
-  let rec conv_const_offset x =
-    match x with
-    | NoOffset    -> `NoOffset
-
-    | Index (Const  (CInt (i,ikind,s)),o) -> `Index (IntDomain.of_const (i,ikind,s), conv_const_offset o)
-    | Index (_,o) -> `Index (ValueDomain.IndexDomain.top (), conv_const_offset o)
-    | Field (f,o) -> `Field (f, conv_const_offset o)
-
   module A =
   struct
     module E = struct
-      include Printable.Either (CilType.Offset) (ValueDomain.Addr)
+      include Printable.Either (CilType.Offset) (ILock)
 
       let pretty () = function
         | `Left o -> Pretty.dprintf "p-lock:%a" (d_offset (text "*")) o
-        | `Right addr -> Pretty.dprintf "i-lock:%a" ValueDomain.Addr.pretty addr
+        | `Right addr -> Pretty.dprintf "i-lock:%a" ILock.pretty addr
 
       include Printable.SimplePretty (
         struct
@@ -164,7 +159,7 @@ struct
     let one_lockstep (_,a,m) xs =
       match m with
       | AddrOf (Var v,o) ->
-        let lock = ValueDomain.Addr.from_var_offset (v, conv_const_offset o) in
+        let lock = ILock.from_var_offset (v, o) in
         A.add (`Right lock) xs
       | _ ->
         Messages.warn "Internal error: found a strange lockstep pattern.";

src/cdomains/intDomain.ml

@@ -930,7 +930,7 @@ struct
   let bot () = raise Error
   let top_of ik = top ()
   let bot_of ik = bot ()
-  let show (x: Ints_t.t) = if (Ints_t.to_int64 x) = GU.inthack then "*" else Ints_t.to_string x
+  let show (x: Ints_t.t) = Ints_t.to_string x
 
   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)
   (* is_top and is_bot are never called, but if they were, the Std impl would raise their exception, so we overwrite them: *)

src/cdomains/lval.ml

@@ -10,7 +10,15 @@ type ('a, 'b) offs = [
 ] [@@deriving eq, ord, hash]
 
 
-module Offset (Idx: IntDomain.Z) =
+(** Subinterface of IntDomain.Z which is sufficient for Printable (but not Lattice) Offset. *)
+module type IdxDomain =
+sig
+  include Printable.S
+  val equal_to: IntOps.BigIntOps.t -> t -> [`Eq | `Neq | `Top]
+  val is_int: t -> bool
+end
+
+module OffsetPrintable (Idx: IdxDomain) =
 struct
   type t = (fieldinfo, Idx.t) offs
   include Printable.Std
@@ -90,6 +98,17 @@ struct
     | `Field _, `Index _ -> -1
     | `Index _, `Field _ ->  1
 
+  let rec to_cil_offset (x:t) =
+    match x with
+    | `NoOffset -> NoOffset
+    | `Field(f,o) -> Field(f, to_cil_offset o)
+    | `Index(i,o) -> NoOffset (* array domain can not deal with this -> leads to being handeled as access to unknown part *)
+end
+
+module Offset (Idx: IntDomain.Z) =
+struct
+  include OffsetPrintable (Idx)
+
   let rec leq x y =
     match x, y with
     | `NoOffset, `NoOffset -> true
@@ -112,12 +131,6 @@ struct
     | `Index (x1,y1), `Index (x2,y2) -> `Index (op x1 x2, merge cop y1 y2)
     | _ -> raise Lattice.Uncomparable
 
-  let rec to_cil_offset (x:t) =
-    match x with
-    | `NoOffset -> NoOffset
-    | `Field(f,o) -> Field(f, to_cil_offset o)
-    | `Index(i,o) -> NoOffset (* array domain can not deal with this -> leads to being handeled as access to unknown part *)
-
   let join x y = merge `Join x y
   let meet x y = merge `Meet x y
   let widen x y = merge `Widen x y
@@ -160,11 +173,11 @@ sig
   (** Finds the type of the address location. *)
 end
 
-module Normal (Idx: IntDomain.Z) =
+module Normal (Idx: IdxDomain) =
 struct
   type field = fieldinfo
   type idx = Idx.t
-  module Offs = Offset (Idx)
+  module Offs = OffsetPrintable (Idx)
   type t =
     | Addr of CilType.Varinfo.t * Offs.t (** Pointer to offset of a variable. *)
     | NullPtr (** NULL pointer. *)
@@ -287,6 +300,7 @@ end
 module NormalLat (Idx: IntDomain.Z) =
 struct
   include Normal (Idx)
+  module Offs = Offset (Idx)
 
   let is_definite = function
     | NullPtr | StrPtr _ -> true

src/cdomains/symbLocksDomain.ml

@@ -111,6 +111,8 @@ struct
     | Index (i,o) -> isConstant i && conc o
     | Field (_,o) -> conc o
 
+  let star = Lval (Cil.var (Goblintutil.create_var (makeGlobalVar "*" intType)))
+
   let rec one_unknown_array_index exp =
     let rec separate_fields_index o =
       match o with
@@ -121,7 +123,6 @@ struct
         | Some (osf, ie,o) -> Some ((fun o -> Field (f,o)), ie, o)
         | x -> x
     in
-    let star = kinteger64 IInt Goblintutil.inthack in
     match exp with
     | Lval (Mem (Lval (Var v, io)),o) when conc o ->
       begin match separate_fields_index io with
@@ -272,3 +273,44 @@ struct
     with Invalid_argument _ -> None
   let printXml f (x,y,z) = BatPrintf.fprintf f "<value>\n<map>\n<key>1</key>\n%a<key>2</key>\n%a<key>3</key>\n%a</map>\n</value>\n" Exp.printXml x Exp.printXml y Exp.printXml z
 end
+
+(** Index-based symbolic lock *)
+module ILock =
+struct
+
+  (** Index in index-based symbolic lock *)
+  module Idx =
+  struct
+    include Printable.Std
+    type t =
+      | Unknown (** Unknown index. Mutex index not synchronized with access index. *)
+      | Star (** Star index. Mutex index synchronized with access index. Corresponds to star_0 in ASE16 paper, multiple star indices not supported in this implementation. *)
+    [@@deriving eq, ord, hash]
+    let name () = "i-lock index"
+
+    let show = function
+      | Unknown -> "?"
+      | Star -> "*"
+
+    include Printable.SimpleShow (
+      struct
+        type nonrec t = t
+        let show = show
+      end
+      )
+
+    let equal_to _ _ = `Top
+    let is_int _ = false
+  end
+
+  include Lval.Normal (Idx)
+
+  let rec conv_const_offset x =
+    match x with
+    | NoOffset    -> `NoOffset
+    | Index (i,o) when Exp.(equal i star) -> `Index (Idx.Star, conv_const_offset o)
+    | Index (_,o) -> `Index (Idx.Unknown, conv_const_offset o)
+    | Field (f,o) -> `Field (f, conv_const_offset o)
+
+  let from_var_offset (v, o) = from_var_offset (v, conv_const_offset o)
+end

src/util/goblintutil.ml

@@ -14,9 +14,6 @@ let should_warn = ref false
 (** Whether signed overflow or underflow happened *)
 let svcomp_may_overflow = ref false
 
-(** hack to use a special integer to denote synchronized array-based locking *)
-let inthack = Int64.of_int (-19012009) (* TODO do we still need this? *)
-
 (** The file where everything is output *)
 let out = ref stdout