Merge branch 'master' into rm-libmaincil

Author: sim642

docs/requirements.txt

@@ -1,5 +1,3 @@
 # Python requirements for MkDocs and Read the Docs
 
-mkdocs==1.2.4
-
-jinja2==3.1.3
+mkdocs==1.5.3

g2html

@@ -61,6 +61,72 @@ def serve():
     panel = browser.find_element(By.CLASS_NAME, "panel")
     print("found DOM elements main, sidebar-left, sidebar-right, content and panel")
 
+    # test syntactic search
+    leftS.find_element(By.LINK_TEXT,  "Search").click()
+    leftS.find_element(By.CLASS_NAME, "switch-to-json").click()
+    textfield = leftS.find_element(By.CLASS_NAME, "form-control")
+    textfield.clear()
+    textfield.send_keys('{"kind":["var"],"target":["name","fail"],"find":["uses"],"mode":["Must"]}')
+    leftS.find_element(By.CLASS_NAME, "exec-button").click()
+    results = leftS.find_elements(By.CLASS_NAME, "list-group-item")
+    locations = []
+    for r in results:
+        for tr in r.find_elements(By.TAG_NAME, "tr"):
+            if tr.find_element(By.TAG_NAME, "th").text == "Location":
+                locations.insert(0,tr.find_element(By.TAG_NAME, "td").find_element(By.TAG_NAME, "a").text)
+
+    print("syntactic search for variable use of 'fail' found", len(results), "results")
+    for l in locations:
+        print(l)
+    assert(len(results) == 2)
+    assert("tests/regression/00-sanity/01-assert.c:7" in locations)
+    assert("tests/regression/00-sanity/01-assert.c:12" in locations)
+
+    # clear results
+    leftS.find_element(By.CLASS_NAME, "clear-btn").click()
+
+    # test semantic search 1
+    textfield = leftS.find_element(By.CLASS_NAME, "form-control")
+    textfield.clear()
+    textfield.send_keys('{"kind":["var"],"target":["name","success"],"find":["uses"],"expression":"success == 1","mode":["Must"]}')
+    leftS.find_element(By.CLASS_NAME, "exec-button").click()
+    results = leftS.find_elements(By.CLASS_NAME, "list-group-item")
+    locations = []
+    for r in results:
+        for tr in r.find_elements(By.TAG_NAME, "tr"):
+            if tr.find_element(By.TAG_NAME, "th").text == "Location":
+                locations.insert(0,tr.find_element(By.TAG_NAME, "td").find_element(By.TAG_NAME, "a").text)
+
+    print("semantic search for variable use of 'success' where it must be 1 found", len(results), "results")
+    for l in locations:
+        print(l)
+    assert(len(results) == 2)
+    assert("tests/regression/00-sanity/01-assert.c:10" in locations)
+    assert("tests/regression/00-sanity/01-assert.c:5" in locations)
+
+    # clear results
+    leftS.find_element(By.CLASS_NAME, "clear-btn").click()
+
+    # test semantic search 2
+    textfield = leftS.find_element(By.CLASS_NAME, "form-control")
+    textfield.clear()
+    textfield.send_keys('{"kind":["var"],"target":["name","success"],"find":["uses"],"expression":"success == 0","mode":["Must"]}')
+    leftS.find_element(By.CLASS_NAME, "exec-button").click()
+    results = leftS.find_elements(By.CLASS_NAME, "list-group-item")
+    locations = []
+    for r in results:
+        for tr in r.find_elements(By.TAG_NAME, "tr"):
+            if tr.find_element(By.TAG_NAME, "th").text == "Location":
+                locations.insert(0,tr.find_element(By.TAG_NAME, "td").find_element(By.TAG_NAME, "a").text)
+
+    print("semantic search for variable use of 'success' where it must be 0 found", len(results), "results")
+    for l in locations:
+        print(l)
+    assert(len(results) == 0)
+
+    # close "No results found" alert
+    leftS.find_element(By.CLASS_NAME, "btn-close").click()
+
     cleanup(browser, thread)
 
 except Exception as e:

gobview

@@ -9,16 +9,10 @@ include RelationAnalysis
 let spec_module: (module MCPSpec) Lazy.t =
   lazy (
     let module AD = AffineEqualityDomain.D2 (VectorMatrix.ArrayVector) (VectorMatrix.ArrayMatrix) in
-    let module RD: RelationDomain.RD =
-    struct
-      module V = AffineEqualityDomain.V
-      include AD
-    end
-    in
     let module Priv = (val RelationPriv.get_priv ()) in
     let module Spec =
     struct
-      include SpecFunctor (Priv) (RD) (RelationPrecCompareUtil.DummyUtil)
+      include SpecFunctor (Priv) (AD) (RelationPrecCompareUtil.DummyUtil)
       let name () = "affeq"
     end
     in

scripts/test-gobview.py

@@ -9,18 +9,11 @@ let spec_module: (module MCPSpec) Lazy.t =
     let module Man = (val ApronDomain.get_manager ()) in
     let module AD = ApronDomain.D2 (Man) in
     let diff_box = GobConfig.get_bool "ana.apron.invariant.diff-box" in
-    let module AD = (val if diff_box then (module ApronDomain.BoxProd (AD): ApronDomain.S3) else (module AD)) in
-    let module RD: RelationDomain.RD =
-    struct
-      module V = ApronDomain.V
-      include AD
-      type var = Apron.Var.t
-    end
-    in
+    let module AD = (val if diff_box then (module ApronDomain.BoxProd (AD): RelationDomain.RD) else (module AD)) in
     let module Priv = (val RelationPriv.get_priv ()) in
     let module Spec =
     struct
-      include SpecFunctor (Priv) (RD) (ApronPrecCompareUtil.Util)
+      include SpecFunctor (Priv) (AD) (ApronPrecCompareUtil.Util)
       let name () = "apron"
     end
     in

src/analyses/apron/affineEqualityAnalysis.apron.ml

@@ -177,14 +177,15 @@ struct
     | LNot -> ID.c_lognot
 
   let unop_FD = function
-    | Neg  -> FD.neg
-    (* other unary operators are not implemented on float values *)
-    | _ -> (fun c -> FD.top_of (FD.get_fkind c))
+    | Neg  -> (fun v -> (Float (FD.neg v):value))
+    | LNot -> (fun c -> Int (FD.eq c (FD.of_const (FD.get_fkind c) 0.)))
+    | BNot -> failwith "BNot on a value of type float!"
+
 
   (* Evaluating Cil's unary operators. *)
   let evalunop op typ: value -> value = function
     | Int v1 -> Int (ID.cast_to (Cilfacade.get_ikind typ) (unop_ID op v1))
-    | Float v -> Float (unop_FD op v)
+    | Float v -> unop_FD op v
     | Address a when op = LNot ->
       if AD.is_null a then
         Int (ID.of_bool (Cilfacade.get_ikind typ) true)
@@ -877,9 +878,9 @@ struct
       | CastE (t, Const (CStr (x,e))) -> (* VD.top () *) eval_rv ~ctx st (Const (CStr (x,e))) (* TODO safe? *)
       | CastE  (t, exp) ->
         (let v = eval_rv ~ctx st exp in
-         try 
+         try
            VD.cast ~torg:(Cilfacade.typeOf exp) t v
-         with Cilfacade.TypeOfError _  -> 
+         with Cilfacade.TypeOfError _  ->
            VD.cast t v)
       | SizeOf _
       | Real _
@@ -1644,6 +1645,9 @@ struct
     module V = V
     module G = G
 
+    let unop_ID = unop_ID
+    let unop_FD = unop_FD
+
     let eval_rv = eval_rv
     let eval_rv_address = eval_rv_address
     let eval_lv = eval_lv
@@ -2841,6 +2845,9 @@ struct
 
           let ost = octx.local
 
+          let unop_ID = unop_ID
+          let unop_FD = unop_FD
+
           (* all evals happen in octx with non-top values *)
           let eval_rv ~ctx st e = eval_rv ~ctx:octx ost e
           let eval_rv_address ~ctx st e = eval_rv_address ~ctx:octx ost e

src/analyses/apron/apronAnalysis.apron.ml

@@ -14,6 +14,9 @@ sig
   module V: Analyses.SpecSysVar
   module G: Lattice.S
 
+  val unop_ID: Cil.unop -> ID.t -> ID.t
+  val unop_FD: Cil.unop -> FD.t -> VD.t
+
   val eval_rv: ctx:(D.t, G.t, _, V.t) Analyses.ctx -> D.t -> exp -> VD.t
   val eval_rv_address: ctx:(D.t, G.t, _, V.t) Analyses.ctx -> D.t -> exp -> VD.t
   val eval_lv: ctx:(D.t, G.t, _, V.t) Analyses.ctx -> D.t -> lval -> AD.t
@@ -41,16 +44,6 @@ module Make (Eval: Eval) =
 struct
   open Eval
 
-  let unop_ID = function
-    | Neg  -> ID.neg
-    | BNot -> ID.lognot
-    | LNot -> ID.c_lognot
-
-  let unop_FD = function
-    | Neg  -> FD.neg
-    (* other unary operators are not implemented on float values *)
-    | _ -> (fun c -> FD.top_of (FD.get_fkind c))
-
   let is_some_bot (x:VD.t) =
     match x with
     | Bot -> false (* HACK: bot is here due to typing conflict (we do not cast appropriately) *)
@@ -565,18 +558,31 @@ struct
       else
         match exp, c_typed with
         | UnOp (LNot, e, _), Int c ->
-          let ikind = Cilfacade.get_ikind_exp e in
-          let c' =
-            match ID.to_bool (unop_ID LNot c) with
-            | Some true ->
-              (* i.e. e should evaluate to [1,1] *)
-              (* LNot x is 0 for any x != 0 *)
-              ID.of_excl_list ikind [Z.zero]
-            | Some false -> ID.of_bool ikind false
-            | _ -> ID.top_of ikind
-          in
-          inv_exp (Int c') e st
-        | UnOp (Neg, e, _), Float c -> inv_exp (Float (unop_FD Neg c)) e st
+          (match Cilfacade.typeOf e with
+           | TInt  _ | TPtr _ ->
+             let ikind = Cilfacade.get_ikind_exp e in
+             let c' =
+               match ID.to_bool (unop_ID LNot c) with
+               | Some true ->
+                 (* i.e. e should evaluate to [1,1] *)
+                 (* LNot x is 0 for any x != 0 *)
+                 ID.of_excl_list ikind [Z.zero]
+               | Some false -> ID.of_bool ikind false
+               | _ -> ID.top_of ikind
+             in
+             inv_exp (Int c') e st
+           | TFloat(fkind, _) when ID.to_bool (unop_ID LNot c) = Some false ->
+             (* C99 §6.5.3.3/5 *)
+             (* The result of the logical negation operator ! is 0 if the value of its operand compares *)
+             (* unequal to 0, 1 if the value of its operand compares equal to 0. The result has type int. *)
+             (* The expression !E is equivalent to (0==E). *)
+             (* NaN compares unequal to 0 so no problems *)
+             (* We do not have exclusions for floats, so we do not bother here with the other case *)
+             let zero_float = FD.of_const fkind 0. in
+             inv_exp (Float zero_float) e st
+           | _ -> st
+          )
+        | UnOp (Neg, e, _), Float c -> inv_exp (unop_FD Neg c) e st
         | UnOp ((BNot|Neg) as op, e, _), Int c -> inv_exp (Int (unop_ID op c)) e st
         (* no equivalent for Float, as VD.is_safe_cast fails for all float types anyways *)
         | BinOp((Eq | Ne) as op, CastE (t1, e1), CastE (t2, e2), t), Int c when typeSig (Cilfacade.typeOf e1) = typeSig (Cilfacade.typeOf e2) && VD.is_safe_cast t1 (Cilfacade.typeOf e1) && VD.is_safe_cast t2 (Cilfacade.typeOf e2) ->

src/analyses/base.ml

@@ -26,8 +26,6 @@ module Mpqf = struct
   let hash x = 31 * (Z.hash (get_den x)) + Z.hash (get_num x)
 end
 
-module V = RelationDomain.V
-
 (** It defines the type t of the affine equality domain (a struct that contains an optional matrix and an apron environment) and provides the functions needed for handling variables (which are defined by RelationDomain.D2) such as add_vars remove_vars.
     Furthermore, it provides the function get_coeff_vec that parses an apron expression into a vector of coefficients if the apron expression has an affine form. *)
 module VarManagement (Vec: AbstractVector) (Mx: AbstractMatrix)=
@@ -240,7 +238,7 @@ struct
   include VarManagement (Vc) (Mx)
 
   module Bounds = ExpressionBounds (Vc) (Mx)
-
+  module V = RelationDomain.V
   module Convert = SharedFunctions.Convert (V) (Bounds) (struct let allow_global = true end) (SharedFunctions.Tracked)
 
   type var = V.t
@@ -703,9 +701,9 @@ struct
   let unmarshal t = t
 end
 
-module D2(Vc: AbstractVector) (Mx: AbstractMatrix): RelationDomain.S3 with type var = Var.t =
+module D2(Vc: AbstractVector) (Mx: AbstractMatrix): RelationDomain.RD with type var = Var.t =
 struct
   module D =  D (Vc) (Mx)
-  include SharedFunctions.AssertionModule (V) (D)
+  include SharedFunctions.AssertionModule (D.V) (D)
   include D
 end

src/analyses/baseInvariant.ml

@@ -779,6 +779,7 @@ module type S2 =
 (* TODO: ExS3 or better extend RelationDomain.S3 directly?*)
 sig
   module Man: Manager
+  module V: RV
   include module type of AOps (Tracked) (Man)
   include SLattice with type t = Man.mt A.t
 
@@ -803,6 +804,7 @@ sig
   include SLattice
   include AOps with type t := t
 
+  module V: RV
   module Tracked: RelationDomain.Tracked
 
   val assert_inv : t -> exp -> bool -> bool Lazy.t -> t
@@ -813,6 +815,7 @@ end
 module D2 (Man: Manager) : S2 with module Man = Man  =
 struct
   include D (Man)
+  module V = RelationDomain.V
 
   type marshal = OctagonD.marshal
 
@@ -926,8 +929,10 @@ struct
     |> Lincons1Set.elements
 end
 
-module BoxProd (D: S3): S3 =
+module BoxProd (D: S3): RD =
 struct
+  module V = D.V
+  type var = V.t
   module BP0 = BoxProd0 (D)
   module Tracked = SharedFunctions.Tracked
   include BP0

src/cdomains/apron/affineEqualityDomain.apron.ml

@@ -128,7 +128,6 @@ end
 module type S3 =
 sig
   include S2
-
   val cil_exp_of_lincons1: Lincons1.t -> exp option
   val invariant: t -> Lincons1.t list
 end

src/cdomains/apron/apronDomain.apron.ml

@@ -122,7 +122,6 @@ let rec pretty_edges () = function
   | [_,x] -> Edge.pretty_plain () x
   | (_,x)::xs -> Pretty.dprintf "%a; %a" Edge.pretty_plain x pretty_edges xs
 
-
 let node_scc_global = NH.create 113
 
 exception Not_connect of fundec

src/cdomains/apron/relationDomain.apron.ml

@@ -8,11 +8,9 @@ include Cilfacade0
 
 (** Command for assigning an id to a varinfo. All varinfos directly created by Goblint should be modified by this method *)
 let create_var (var: varinfo) =
-  (* TODO Hack: this offset should preempt conflicts with ids generated by CIL *)
-  let start_id = 10_000_000_000 in
+  (* Hack: using negative integers should preempt conflicts with ids generated by CIL *)
   let hash = Hashtbl.hash { var with vid = 0 } in
-  let hash = if hash < start_id then hash + start_id else hash in
-  { var with vid = hash }
+  { var with vid = - hash } (* Hashtbl.hash returns non-negative integer *)
 
 
 (** Is character type (N1570 6.2.5.15)? *)
@@ -531,9 +529,7 @@ let stmt_fundecs: fundec StmtH.t ResettableLazy.t =
 
 
 let get_pseudo_return_id fd =
-  let start_id = 10_000_000_000 in (* TODO get max_sid? *)
-  let sid = Hashtbl.hash fd.svar.vid in (* Need pure sid instead of Cil.new_sid for incremental, similar to vid in Cilfacade.create_var. We only add one return stmt per loop, so the hash from the functions vid should be unique. *)
-  if sid < start_id then sid + start_id else sid
+  - fd.svar.vid (* Need pure sid instead of Cil.new_sid for incremental, similar to vid in Cilfacade.create_var. We only add one return stmt per loop, so the hash from the functions vid should be unique. *)
 
 let pseudo_return_to_fun = StmtH.create 113
 

src/common/framework/cfgTools.ml

@@ -52,7 +52,7 @@ struct
       (* Not using Node.location here to have updated locations in incremental analysis.
          See: https://github.com/goblint/analyzer/issues/290#issuecomment-881258091. *)
       let loc = UpdateCil.getLoc n in
-      BatPrintf.fprintf f "<call id=\"%s\" file=\"%s\" line=\"%d\" order=\"%d\" column=\"%d\">\n" (Node.show_id n) loc.file loc.line loc.byte loc.column;
+      BatPrintf.fprintf f "<call id=\"%s\" file=\"%s\" line=\"%d\" order=\"%d\" column=\"%d\" endLine=\"%d\" endColumn=\"%d\" synthetic=\"%B\">\n" (Node.show_id n) loc.file loc.line loc.byte loc.column loc.endLine loc.endColumn loc.synthetic;
       BatPrintf.fprintf f "%a</call>\n" Range.printXml v
     in
     iter print_one xs