Skip to content

Commit

Permalink
Merge branch 'master' into issue_1211
Browse files Browse the repository at this point in the history
  • Loading branch information
@michael-schwarz
michael-schwarz committed Feb 4, 2024
2 parents 0cc39e2 + e8da916 commit 1eee742
Show file tree
Hide file tree
Showing 37 changed files with 805 additions and 641 deletions.
8 changes: 1 addition & 7 deletions src/analyses/apron/affineEqualityAnalysis.apron.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
11 changes: 2 additions & 9 deletions src/analyses/apron/apronAnalysis.apron.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
20 changes: 16 additions & 4 deletions src/analyses/apron/relationAnalysis.apron.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -218,10 +218,22 @@ struct
| Lval (Mem e, NoOffset) ->
begin match ask (Queries.MayPointTo e) with
| ad when not (Queries.AD.is_top ad) && (Queries.AD.cardinal ad) = 1 ->
begin match Queries.AD.Addr.to_mval (Queries.AD.choose ad) with
| Some mval -> ValueDomain.Addr.Mval.to_cil_exp mval
| None -> Lval (Mem e, NoOffset)
end
let replace mval =
try
let pointee = ValueDomain.Addr.Mval.to_cil_exp mval in
let pointee_typ = Cil.typeSig @@ Cilfacade.typeOf pointee in
let lval_typ = Cil.typeSig @@ Cilfacade.typeOfLval (Mem e, NoOffset) in
if pointee_typ = lval_typ then
Some pointee
else
(* there is a type-mismatch between pointee and pointer-type *)
(* to avoid mismatch errors, we bail on this expression *)
None
with Cilfacade.TypeOfError _ ->
None
in
let r = Option.bind (Queries.AD.Addr.to_mval (Queries.AD.choose ad)) replace in
Option.default (Lval (Mem e, NoOffset)) r
(* It would be possible to do better here, exploiting e.g. that the things pointed to are known to be equal *)
(* see: https://github.com/goblint/analyzer/pull/742#discussion_r879099745 *)
| _ -> Lval (Mem e, NoOffset)
Expand Down
54 changes: 28 additions & 26 deletions src/analyses/base.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,6 @@ module Addr = ValueDomain.Addr
module Offs = ValueDomain.Offs
module LF = LibraryFunctions
module CArrays = ValueDomain.CArrays
module BI = IntOps.BigIntOps
module PU = PrecisionUtil

module VD = BaseDomain.VD
Expand Down Expand Up @@ -174,8 +173,8 @@ struct

let unop_ID = function
| Neg -> ID.neg
| BNot -> ID.bitnot
| LNot -> ID.lognot
| BNot -> ID.lognot
| LNot -> ID.c_lognot

let unop_FD = function
| Neg -> (fun v -> (Float (FD.neg v):value))
Expand Down Expand Up @@ -214,13 +213,13 @@ struct
evalint: base eval_rv 1 -> (1,[1,1])
evalint: base query_evalint m == 1 -> (0,[1,1]) *)
| Ne -> ID.ne
| BAnd -> ID.bitand
| BOr -> ID.bitor
| BXor -> ID.bitxor
| BAnd -> ID.logand
| BOr -> ID.logor
| BXor -> ID.logxor
| Shiftlt -> ID.shift_left
| Shiftrt -> ID.shift_right
| LAnd -> ID.logand
| LOr -> ID.logor
| LAnd -> ID.c_logand
| LOr -> ID.c_logor
| b -> (fun x y -> (ID.top_of result_ik))

let binop_FD (result_fk: Cil.fkind) = function
Expand Down Expand Up @@ -248,7 +247,7 @@ struct
if M.tracing then M.tracel "eval" "evalbinop %a %a %a\n" d_binop op VD.pretty a1 VD.pretty a2;
(* We define a conversion function for the easy cases when we can just use
* the integer domain operations. *)
let bool_top ik = ID.(join (of_int ik BI.zero) (of_int ik BI.one)) in
let bool_top ik = ID.(join (of_int ik Z.zero) (of_int ik Z.one)) in
(* An auxiliary function for ptr arithmetic on array values. *)
let addToAddr n (addr:Addr.t) =
let typeOffsetOpt o t =
Expand All @@ -271,7 +270,7 @@ struct
begin match t with
| Some t ->
let (f_offset_bits, _) = bitsOffset t (Field (f, NoOffset)) in
let f_offset = IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) (BI.of_int (f_offset_bits / 8)) in
let f_offset = IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int (f_offset_bits / 8)) in
begin match IdxDom.(to_bool (eq f_offset (neg n_offset))) with
| Some true -> `NoOffset
| _ -> `Field (f, `Index (n_offset, `NoOffset))
Expand All @@ -287,7 +286,7 @@ struct
| `NoOffset -> `Index(iDtoIdx n, `NoOffset)
in
let default = function
| Addr.NullPtr when GobOption.exists (BI.equal BI.zero) (ID.to_int n) -> Addr.NullPtr
| Addr.NullPtr when GobOption.exists (Z.equal Z.zero) (ID.to_int n) -> Addr.NullPtr
| _ -> Addr.UnknownPtr
in
match Addr.to_mval addr with
Expand Down Expand Up @@ -389,9 +388,9 @@ struct
Int (ID.top_of ik)
end
| Eq ->
Int (if AD.is_bot (AD.meet p1 p2) then ID.of_int ik BI.zero else match eq p1 p2 with Some x when x -> ID.of_int ik BI.one | _ -> bool_top ik)
Int (if AD.is_bot (AD.meet p1 p2) then ID.of_int ik Z.zero else match eq p1 p2 with Some x when x -> ID.of_int ik Z.one | _ -> bool_top ik)
| Ne ->
Int (if AD.is_bot (AD.meet p1 p2) then ID.of_int ik BI.one else match eq p1 p2 with Some x when x -> ID.of_int ik BI.zero | _ -> bool_top ik)
Int (if AD.is_bot (AD.meet p1 p2) then ID.of_int ik Z.one else match eq p1 p2 with Some x when x -> ID.of_int ik Z.zero | _ -> bool_top ik)
| IndexPI when AD.to_string p2 = ["all_index"] ->
addToAddrOp p1 (ID.top_of (Cilfacade.ptrdiff_ikind ()))
| IndexPI | PlusPI ->
Expand Down Expand Up @@ -873,13 +872,16 @@ struct
(* CIL's very nice implicit conversion of an array name [a] to a pointer
* to its first element [&a[0]]. *)
| StartOf lval ->
let array_ofs = `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.zero, `NoOffset) in
let array_ofs = `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero, `NoOffset) in
let array_start = add_offset_varinfo array_ofs in
Address (AD.map array_start (eval_lv ~ctx st lval))
| 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
VD.cast ~torg:(Cilfacade.typeOf exp) t v
(let v = eval_rv ~ctx st exp in
try
VD.cast ~torg:(Cilfacade.typeOf exp) t v
with Cilfacade.TypeOfError _ ->
VD.cast t v)
| SizeOf _
| Real _
| Imag _
Expand Down Expand Up @@ -976,11 +978,11 @@ struct
match op with
| MinusA when must_be_equal () ->
let ik = Cilfacade.get_ikind t in
Int (ID.of_int ik BI.zero)
Int (ID.of_int ik Z.zero)
| MinusPI (* TODO: untested *)
| MinusPP when must_be_equal () ->
let ik = Cilfacade.ptrdiff_ikind () in
Int (ID.of_int ik BI.zero)
Int (ID.of_int ik Z.zero)
(* Eq case is unnecessary: Q.must_be_equal reconstructs BinOp (Eq, _, _, _) and repeats EvalInt query for that, yielding a top from query cycle and never being must equal *)
| Le
| Ge when must_be_equal () ->
Expand Down Expand Up @@ -1273,7 +1275,7 @@ struct
| _ -> None
in
let alen = Seq.filter_map (fun v -> lenOf v.vtype) (List.to_seq (AD.to_var_may a)) in
let d = Seq.fold_left ID.join (ID.bot_of (Cilfacade.ptrdiff_ikind ())) (Seq.map (ID.of_int (Cilfacade.ptrdiff_ikind ()) %BI.of_int) (Seq.append slen alen)) in
let d = Seq.fold_left ID.join (ID.bot_of (Cilfacade.ptrdiff_ikind ())) (Seq.map (ID.of_int (Cilfacade.ptrdiff_ikind ()) %Z.of_int) (Seq.append slen alen)) in
(* ignore @@ printf "EvalLength %a = %a\n" d_exp e ID.pretty d; *)
`Lifted d
| Bot -> Queries.Result.bot q (* TODO: remove *)
Expand Down Expand Up @@ -1306,7 +1308,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 ()) Z.zero)) with
| Blob (_,s,_) -> `Lifted s
| _ -> Queries.Result.top q
)
Expand Down Expand Up @@ -2456,7 +2458,7 @@ struct
| Isgreaterequal (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.ge x y))
| Isless (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.lt x y))
| Islessequal (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.le x y))
| Islessgreater (x,y) -> Int(ID.logor (ID.cast_to IInt (apply_binary FDouble FD.lt x y)) (ID.cast_to IInt (apply_binary FDouble FD.gt x y)))
| Islessgreater (x,y) -> Int(ID.c_logor (ID.cast_to IInt (apply_binary FDouble FD.lt x y)) (ID.cast_to IInt (apply_binary FDouble FD.gt x y)))
| Isunordered (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.unordered x y))
| Fmax (fd, x ,y) -> Float (apply_binary fd FD.fmax x y)
| Fmin (fd, x ,y) -> Float (apply_binary fd FD.fmin x y)
Expand All @@ -2476,7 +2478,7 @@ struct
let st' =
(* TODO: should invalidate shallowly? https://github.com/goblint/analyzer/pull/1224#discussion_r1405826773 *)
match eval_rv ~ctx st ret_var with
| Int n when GobOption.exists (BI.equal BI.zero) (ID.to_int n) -> st
| Int n when GobOption.exists (Z.equal Z.zero) (ID.to_int n) -> st
| Address ret_a ->
begin match eval_rv ~ctx st id with
| Thread a when ValueDomain.Threads.is_top a -> invalidate ~ctx st [ret_var]
Expand Down Expand Up @@ -2536,8 +2538,8 @@ struct
let blobsize = ID.mul (ID.cast_to ik @@ sizeval) (ID.cast_to ik @@ countval) in
(* the memory that was allocated by calloc is set to bottom, but we keep track that it originated from calloc, so when bottom is read from memory allocated by calloc it is turned to zero *)
set_many ~ctx st [
(add_null (AD.of_var heap_var), TVoid [], Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.one) (Blob (VD.bot (), blobsize, false))));
(eval_lv ~ctx st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_mval (heap_var, `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.zero, `NoOffset)))))
(add_null (AD.of_var heap_var), TVoid [], Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.one) (Blob (VD.bot (), blobsize, false))));
(eval_lv ~ctx st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_mval (heap_var, `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero, `NoOffset)))))
]
)
| _ -> st
Expand All @@ -2552,7 +2554,7 @@ struct
match p_rv with
| Address a -> a
(* TODO: don't we already have logic for this? *)
| Int i when ID.to_int i = Some BI.zero -> AD.null_ptr
| Int i when ID.to_int i = Some Z.zero -> AD.null_ptr
| Int i -> AD.top_ptr
| _ -> AD.top_ptr (* TODO: why does this ever happen? *)
in
Expand Down Expand Up @@ -2591,7 +2593,7 @@ struct
in
begin match lv with
| Some lv ->
set ~ctx st' (eval_lv ~ctx st lv) (Cilfacade.typeOfLval lv) (Int (ID.of_int IInt BI.zero))
set ~ctx st' (eval_lv ~ctx st lv) (Cilfacade.typeOfLval lv) (Int (ID.of_int IInt Z.zero))
| None -> st'
end
| Longjmp {env; value}, _ ->
Expand Down
Loading

0 comments on commit 1eee742

Please sign in to comment.