Merge remote-tracking branch 'upstream/master' into relationalArray

Author: FungOliver

.gitmodules

@@ -4,6 +4,3 @@
 [submodule "g2html"]
 	path = g2html
 	url = https://github.com/goblint/g2html.git
-[submodule "gobview"]
-	path = gobview
-	url = https://github.com/goblint/gobview.git

src/analyses/apron/relationAnalysis.apron.ml

@@ -196,7 +196,7 @@ struct
   let assert_type_bounds ask rel x =
     assert (RD.Tracked.varinfo_tracked x);
     match Cilfacade.get_ikind x.vtype with
-    | ik  -> (* don't add type bounds for signed when assume_none *)
+    | ik ->
       let (type_min, type_max) = IntDomain.Size.range ik in
       (* TODO: don't go through CIL exp? *)
       let e1 = BinOp (Le, Lval (Cil.var x), (Cil.kintegerCilint ik type_max), intType) in
@@ -293,10 +293,10 @@ struct
         let castedPointer =  PointerMap.to_varinfo v in 
         Lval (Var castedPointer, offset)
       | BinOp (binop, e1, e2, typ) when binop = PlusPI || binop = IndexPI ->  (*pointer is always on the most left*)
-        let e2WithMult = BinOp (Mult, integer sizeOfTyp , CastE (!upointType ,e2), !upointType) in
+        let e2WithMult = BinOp (Mult, integer sizeOfTyp , CastE (!ptrdiffType ,e2), !ptrdiffType) in
         BinOp (PlusA, replacePointer e1 , e2WithMult, typ) 
       | BinOp (MinusPI, e1, e2, typ) -> 
-        let e2WithMult = BinOp (Mult, integer sizeOfTyp, CastE (!upointType ,e2), !upointType) in
+        let e2WithMult = BinOp (Mult, integer sizeOfTyp, CastE (!ptrdiffType ,e2), !ptrdiffType) in
         BinOp (MinusA, replacePointer e1 , e2WithMult, typ) 
       | e -> e
     in
@@ -393,9 +393,9 @@ struct
     if var_option != None &&  PointerMap.mem_varinfo (Option.get var_option) then 
       false 
     else 
-      let vname = RD.Var.to_string var in
+      let vname = Apron.Var.to_string var in
       let locals = fundec.sformals @ fundec.slocals in
-      match List.find_opt (fun v -> VM.var_name (Local v) = vname) locals with 
+      match List.find_opt (fun v -> VM.var_name (Local v) = vname) locals with (* TODO: optimize *)
       | None -> true
       | Some v -> any_local_reachable
 
@@ -420,24 +420,27 @@ struct
   let make_callee_rel ~thread ctx f args =
     let fundec = Node.find_fundec ctx.node in
     let st = ctx.local in
-    let argPointerMapping (x,y) = (*maps expression assigned to pointer args *)
-      if GobConfig.get_bool "ana.apron.pointer_tracking" && isPointerType x.vtype then 
+    let argPointerMapping (x,e) = (*maps expression assigned to pointer args *)
+      if GobConfig.get_bool "ana.apron.pointer_tracking" then 
         begin match sizeOfTyp (Lval (Var x, NoOffset)) with
           | Some typSize -> 
-            (PointerMap.to_varinfo x, replacePointerWithMapping y typSize) 
-          | _ -> (x,y)
+            let x = PointerMap.to_varinfo x in (*map pointer to helper variable*)
+            let y = replacePointerWithMapping e typSize in (*replace right side of assignment with pointer mapping*)
+            Some (RV.local x, y) (* assignment only works with local for some reason *)
+          | _ -> None
         end
-      else (x,y)
+      else None
     in
     let arg_assigns =
       GobList.combine_short f.sformals args (* TODO: is it right to ignore missing formals/args? *)
-      |> List.filter (fun (x, _) -> RD.Tracked.varinfo_tracked x || isPointerType x.vtype)
-      |> List.map argPointerMapping
-      |> List.map (Tuple2.map1 (fun x -> 
-          if PointerMap.mem_varinfo x then 
-            RV.local x (* assignment only works with local for some reason *)
+      |> List.filter_map (fun (x, e) -> 
+          if RD.Tracked.varinfo_tracked x then 
+            Some (RV.arg x, e) 
+          else if  isPointerType x.vtype then 
+            argPointerMapping (x,e) 
           else 
-            RV.arg x))
+            None
+        )
     in
     let reachableAllocSizeVars = (* get a list of all possible addresses arg may point to *)
       GobList.combine_short f.sformals args |> List.filter (fun (x, _) -> isPointerType x.vtype) |> List.map ((fun (_,x) -> mayPointToList ctx x)) |> List.flatten
@@ -461,10 +464,9 @@ struct
     let any_local_reachable = any_local_reachable fundec reachable_from_args in
     RD.remove_filter_with new_rel (fun var ->
         match RV.find_metadata var with
-        | Some (Local _) when not (pass_to_callee fundec any_local_reachable var) && not (List.mem_cmp RD.Var.compare var arg_vars) -> if M.tracing then M.trace "re" "remove Local: %a\n" (docOpt (CilType.Varinfo.pretty())) (RV.to_cil_varinfo var);true (* remove caller locals provided they are unreachable *)
-        | Some (Arg _) when not (List.mem_cmp RD.Var.compare var arg_vars) -> if M.tracing then M.trace "re" "remove Arg: %a\n" (docOpt (CilType.Varinfo.pretty())) (RV.to_cil_varinfo var);true (* remove caller args, but keep just added args *)
-        | _ -> 
-          match RV.to_cil_varinfo var with
+        | Some (Local _) when not (pass_to_callee fundec any_local_reachable var) && not (List.mem_cmp Apron.Var.compare var arg_vars) -> true (* remove caller locals provided they are unreachable *)
+        | Some (Arg _) when not (List.mem_cmp Apron.Var.compare var arg_vars) -> true (* remove caller args, but keep just added args *)
+        | _ -> match RV.to_cil_varinfo var with
           | None -> false
           | Some var -> filterAllocVar var reachableAllocSizeVars (* check if the allocMapping var is reachable from the new function *)
           (* keep everything else (just added args, globals, global privs) *)
@@ -889,15 +891,15 @@ struct
         if M.tracing then M.trace "OOB" "st: %a\n" RD.pretty st.rel;
         begin match sizeOfTyp e1 with 
           | Some typSize -> 
-            let e2Mult = BinOp (Mult, e2, integer typSize, TInt ( Cilfacade.ptrdiff_ikind (), []) )in
+            let e2Mult = BinOp (Mult, e2, integer typSize, TInt (IInt, []) )in
             let isAfterZero = 
               begin match IntDomain.IntDomTuple.minimal i with  
                 | None  -> VDQ.ID.top ()
                 | Some min -> 
                   begin 
                     try 
                       let min = Z.to_int min in 
-                      let aZExp = BinOp (binop, integer min, e2Mult, TInt (Cilfacade.ptrdiff_ikind (),[])) in
+                      let aZExp = BinOp (binop, integer min, e2Mult, TInt (IInt, [])) in
                       let afterZero = Cilfacade.makeBinOp Le  Cil.zero aZExp in
                       eval_int afterZero (no_overflow ask afterZero)
                     with 
@@ -911,7 +913,7 @@ struct
                 | Some i -> 
                   begin try
                       let i = Z.to_int i + structOffset in
-                      let relExp =  BinOp (binop, integer i, e2Mult, TInt (Cilfacade.ptrdiff_ikind () ,[])) in
+                      let relExp =  BinOp (binop, integer i, e2Mult, TInt (IInt, [])) in
                       inBoundsForAllAddresses relExp
                     with
                     | Z.Overflow -> VDQ.ID.top ()

src/analyses/base.ml

@@ -1289,7 +1289,7 @@ struct
             (match r with
              | Array a ->
                (* unroll into array for Calloc calls *)
-               (match ValueDomain.CArrays.get (Queries.to_value_domain_ask (Analyses.ask_of_ctx ctx)) a (None, (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.zero)) with
+               (match ValueDomain.CArrays.get (Queries.to_value_domain_ask (Analyses.ask_of_ctx ctx)) a (None, (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.zero)) None with
                 | Blob (_,s,_) -> `Lifted s
                 | _ -> Queries.Result.top q
                )

src/analyses/memOutOfBounds.ml

@@ -69,17 +69,17 @@ struct
     in
     host_contains_a_ptr host || offset_contains_a_ptr offset
 
-  let points_to_heap_only ctx ptr =
+  let points_to_alloc_only ctx ptr =
     match ctx.ask (Queries.MayPointTo ptr) with
     | a when not (Queries.AD.is_top a)->
       Queries.AD.for_all (function
-          | Addr (v, o) -> ctx.ask (Queries.IsHeapVar v)
+          | Addr (v, o) -> ctx.ask (Queries.IsAllocVar v)
           | _ -> false
         ) a
     | _ -> false
 
   let get_size_of_ptr_target ctx ptr =
-    if points_to_heap_only ctx ptr then
+    if points_to_alloc_only ctx ptr then
       (* Ask for BlobSize from the base address (the second component being set to true) in order to avoid BlobSize giving us bot *)
       ctx.ask (Queries.BlobSize {exp = ptr; base_address = true})
     else

src/cdomain/value/cdomains/arrayDomain.ml

@@ -45,9 +45,6 @@ sig
   type idx
   type value
 
-  val domain_of_t: t -> domain
-
-  val get: ?checkBounds:bool -> VDQ.t -> t -> Basetype.CilExp.t option * idx -> (lval option * int) option -> value
   val set: VDQ.t -> t -> Basetype.CilExp.t option * idx -> value -> t
   val make: ?varAttr:attributes -> ?typAttr:attributes -> idx -> value -> t
   val length: t -> idx option
@@ -70,7 +67,7 @@ sig
   include S0
 
   val domain_of_t: t -> domain
-  val get: ?checkBounds:bool -> VDQ.t -> t -> Basetype.CilExp.t option * idx -> value
+  val get: ?checkBounds:bool -> VDQ.t -> t -> Basetype.CilExp.t option * idx -> (lval option * int) option -> value
 end
 
 module type Str =
@@ -209,7 +206,7 @@ struct
   let extract x default = match x with
     | Some c -> c
     | None -> default
-  let get ?(checkBounds=true)  (ask: VDQ.t) (xl, xr) (_,i) arr =
+  let get ?(checkBounds=true)  (ask: VDQ.t) (xl, xr) (_,i) _ =
     let search_unrolled_values min_i max_i =
       let rec subjoin l i = match l with
         | [] -> Val.bot ()
@@ -403,7 +400,7 @@ struct
                ("m", Val.to_yojson xm);
                ("r", Val.to_yojson xr) ]
 
-  let get ?(checkBounds=true) (ask:VDQ.t) (x:t) (i,_) _ =
+  let get ?(checkBounds=true) (ask:VDQ.t) (x:t) (i,_) _=
     match x, i with
     | Joint v, _ -> v
     | Partitioned (e, (xl, xm, xr)), Some i' ->
@@ -1127,7 +1124,7 @@ struct
     in
 
     (* warn if index is (potentially) out of bounds *)
-    array_oob_check (module Idx) (Nulls.get_set Possibly, size) (e, i);
+    array_oob_check (module Idx) (Nulls.get_set Possibly, size) (e, i) None ask;
     let nulls = match max_i with
       (* if no maximum number in index interval *)
       | None ->
@@ -1822,8 +1819,8 @@ struct
 
   let domain_of_t (t_f, _) = A.domain_of_t t_f
 
-  let get ?(checkBounds=true) (ask: VDQ.t) (t_f, t_n) i =
-    let f_get = A.get ~checkBounds ask t_f i in
+  let get ?(checkBounds=true) (ask: VDQ.t) (t_f, t_n) i arrExpDim=
+    let f_get = A.get ~checkBounds ask t_f i arrExpDim in
     if get_bool "ana.base.arrays.nullbytes" then
       let n_get = N.get ask t_n i in
       match Val.get_ikind f_get, n_get with

src/cdomain/value/cdomains/arrayDomain.mli

@@ -21,12 +21,6 @@ sig
   type value
   (** The abstract domain of values stored in the array. *)
 
-  val domain_of_t: t -> domain
-  (* Returns the domain used for the array*)
-
-  val get: ?checkBounds:bool -> VDQ.t -> t -> Basetype.CilExp.t option * idx -> (lval option * int) option -> value
-  (** Returns the element residing at the given index. *)
-
   val set: VDQ.t -> t -> Basetype.CilExp.t option * idx -> value -> t
   (** Returns a new abstract value, where the given index is replaced with the
     * given element. *)
@@ -68,7 +62,7 @@ sig
   val domain_of_t: t -> domain
   (* Returns the domain used for the array*)
 
-  val get: ?checkBounds:bool -> VDQ.t -> t -> Basetype.CilExp.t option * idx -> value
+  val get: ?checkBounds:bool -> VDQ.t -> t -> Basetype.CilExp.t option * idx -> (lval option * int) option -> value
   (** Returns the element residing at the given index. *)
 end
 

src/cdomain/value/cdomains/valueDomain.ml

@@ -930,7 +930,7 @@ struct
     in
     do_eval_offset ask f x offs exp l o v t 0
 
-  let update_offset (ask: VDQ.t) (x:t) (offs:offs) (value:t) (exp:exp option) (v:lval) (t:typ): t =
+  let update_offset ?(blob_destructive=false) (ask: VDQ.t) (x:t) (offs:offs) (value:t) (exp:exp option) (v:lval) (t:typ): t =
     let rec do_update_offset (ask:VDQ.t) (x:t) (offs:offs) (value:t) (exp:exp option) (l:lval option) (o:offset option) (v:lval) (t:typ) (depth:int):t =
       if M.tracing then M.traceli "update_offset" "do_update_offset %a %a (%a) %a\n" pretty x Offs.pretty offs (Pretty.docOpt (CilType.Exp.pretty ())) exp pretty value;
       let mu = function Blob (Blob (y, s', orig), s, orig2) -> Blob (y, ID.join s s',orig) | x -> x in

src/domains/queries.ml

@@ -332,11 +332,14 @@ struct
     | Any (EvalMutexAttr _ ) -> 50
     | Any ThreadCreateIndexedNode -> 51
     | Any ThreadsJoinedCleanly -> 52
-    | Any (TmpSpecial _) -> 53
-    | Any (IsAllocVar _) -> 54
-    | Any (MayBeOutOfBounds _) -> 55
-    | Any (MayOverflow _) -> 56
-    | Any (AllocMayBeOutOfBounds _) -> 56
+    | Any (MustTermLoop _) -> 53
+    | Any MustTermAllLoops -> 54
+    | Any IsEverMultiThreaded -> 55
+    | Any (TmpSpecial _) -> 56
+    | Any (IsAllocVar _) -> 57
+    | Any (MayBeOutOfBounds _) -> 58
+    | Any (MayOverflow _) -> 59
+    | Any (AllocMayBeOutOfBounds _) -> 60
 
   let rec compare a b =
     let r = Stdlib.compare (order a) (order b) in