Skip to content

Commit

Permalink
Rebase master onto relationalArray
Browse files Browse the repository at this point in the history
  • Loading branch information
@FungOliver
FungOliver committed Jan 24, 2024
1 parent 5ba88f9 commit 599e67e
Show file tree
Hide file tree
Showing 7 changed files with 100 additions and 90 deletions.
51 changes: 27 additions & 24 deletions src/analyses/apron/relationAnalysis.apron.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -183,7 +183,7 @@ struct
true
else
let t = ask.f (MayOverflow exp) in
if M.tracing then M.trace "overflow" "no_o exp: %a %a -> %b \n" d_exp exp d_ikind ik t;
if M.tracing then M.trace "error" "no_o exp: %a %a -> %b \n" d_exp exp d_ikind ik t;
t

let no_overflow ctx exp = lazy (
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -393,7 +393,7 @@ 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
| None -> true
Expand All @@ -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

Check warning

Code scanning / Semgrep OSS

Semgrep Finding: semgrep.list-map-flatten Warning

use List.concat_map instead
Expand All @@ -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) *)
Expand Down Expand Up @@ -853,8 +855,9 @@ struct
let newVar = ArrayMap.to_varinfo (v, t) in
let comp = Cilfacade.makeBinOp Lt exp (Lval (Var newVar,NoOffset)) in
let i = eval_int comp (no_overflow ask comp ) in
if M.tracing then M.trace "relationalArray" "comp: %a\n result=%a" d_exp comp ID.pretty i;
i
| AllocMayBeOutOfBounds (e, i, o) ->
| AllocMayBeOutOfBounds (e, i, o, _) ->
let inBoundsForAllAddresses indexExp = begin match ctx.ask (Queries.MayPointTo e) with
| a when not (Queries.AD.is_top a) ->
Queries.AD.fold ( fun (addr : AD.elt) (st ) ->
Expand Down Expand Up @@ -889,15 +892,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
Expand All @@ -911,7 +914,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 ()
Expand Down
2 changes: 1 addition & 1 deletion src/analyses/base.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
)
Expand Down
53 changes: 30 additions & 23 deletions src/analyses/memOutOfBounds.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -283,14 +283,20 @@ struct
| _ -> failwith "unexpected expression in calculateOffs!\n"
in
let addr_offs_casted = ID.cast_to (Cilfacade.ptrdiff_ikind ()) addr_offs in (*pointer offset + struct offset*)
let structOffset = begin match o with
| None -> ID.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero
let structOffset, currentSizeTyp = begin match o with
| None -> ID.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero, t
| Some o ->
let offsetTyp = begin match o with
| Field (f, o) ->
if M.tracing then M.trace "OOB" "Typ of Offset=%a\n" d_type f.ftype;
f.ftype
| _ -> t
end in
let offs_intdom = cil_offs_to_idx ctx t o in (*struct offset*)
ID.cast_to (Cilfacade.ptrdiff_ikind ()) offs_intdom
ID.cast_to (Cilfacade.ptrdiff_ikind ()) offs_intdom, offsetTyp
end
in
let isAfterZero, isBeforeEnd = (ctx.ask (Queries.AllocMayBeOutOfBounds (e, addr_offs_casted, structOffset))) in
let isAfterZero, isBeforeEnd = (ctx.ask (Queries.AllocMayBeOutOfBounds (e, addr_offs_casted, structOffset, currentSizeTyp))) in
let isAfterZeroBool, isBeforeEndBool = (VDQ.ID.to_bool isAfterZero, VDQ.ID.to_bool isBeforeEnd) in
begin match isAfterZeroBool with
| None ->
Expand Down Expand Up @@ -434,33 +440,36 @@ struct

let query ctx (type a) (q: a Queries.t): a Queries.result =
match q with
| Queries.AllocMayBeOutOfBounds (e, i, o) ->
| Queries.AllocMayBeOutOfBounds (e, i, o, t) ->
begin match i with
| i when not @@ ID.is_bot i ->
begin match typeOf e with
| TPtr (ty, _) ->
if M.tracing then M.trace "OOB" "e=%a i=%a o=%a\n" d_exp e ID.pretty i ID.pretty o;
let expOffset = match e with
| Lval (Var v, _) -> i
| BinOp (binop, e1, e2, t) when binop = PlusPI || binop = IndexPI || binop = MinusPI ->
let e2Offset = eval_ptr_offset_in_binop ctx e2 ty in (*add offset of e2*)
begin match e2Offset with
| `Lifted e2Offset ->
begin
try if binop = MinusPI then
ID.sub i e2Offset
else
ID.add i e2Offset
with IntDomain.ArithmeticOnIntegerBot _ -> ID.top_of (Cilfacade.ptrdiff_ikind ())
let ptr_deref_type = get_ptr_deref_type @@ typeOf e1 in
begin match ptr_deref_type with
| Some typ->
let e2Offset = eval_ptr_offset_in_binop ctx e2 typ in (*add offset of e2*)
begin match e2Offset with
| `Lifted e2Offset ->
begin
try if binop = MinusPI then
ID.sub i e2Offset
else
ID.add i e2Offset
with IntDomain.ArithmeticOnIntegerBot _ -> ID.top_of (Cilfacade.ptrdiff_ikind ())
end
| `Top | `Bot -> ID.top_of (Cilfacade.ptrdiff_ikind ())
end
| `Top | `Bot -> ID.top_of (Cilfacade.ptrdiff_ikind ())
| _ -> ID.top_of (Cilfacade.ptrdiff_ikind ())
end
| _ ->failwith "unexpected expression in query AllocMayBeOutOfBounds \n"
in
if M.tracing then M.trace "OOB" "e=%a expOffset %a \n" d_exp e ID.pretty expOffset;
let isBeforeZero = ID.le (ID.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero) expOffset in (*check for negative Indices*)

let current_index_size = size_of_type_in_bytes ty in
let current_index_size = size_of_type_in_bytes t in
let casted_current_index_size = ID.cast_to (Cilfacade.ptrdiff_ikind ()) current_index_size in (*add size of type*)
let expOffset_plus_current_index_size =
begin try ID.add expOffset casted_current_index_size
Expand All @@ -485,8 +494,6 @@ struct
(`Lifted isBeforeZero,`Lifted isBeforeEnd)
| _ -> (ValueDomainQueries.ID.top (), ValueDomainQueries.ID.top())
end
| _ -> (ValueDomainQueries.ID.top (), ValueDomainQueries.ID.top())
end
(* Queries.Result.top q *)
| _ -> Queries.Result.top q

Expand Down
20 changes: 9 additions & 11 deletions src/cdomain/value/cdomains/arrayDomain.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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 =
Expand Down Expand Up @@ -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 ()
Expand Down Expand Up @@ -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' ->
Expand Down Expand Up @@ -839,8 +836,9 @@ let array_oob_check ( type a ) (module Idx: IntDomain.Z with type t = a) (x, l)
if GobConfig.get_bool "ana.arrayoob" then (* The purpose of the following 2 lines is to give the user extra info about the array oob *)
let idx_before_end = Idx.to_bool (Idx.lt v l) (* check whether index is before the end of the array *)
and idx_after_start = Idx.to_bool (Idx.ge v (Idx.of_int Cil.ILong BI.zero)) in (* check whether the index is non-negative *)
if M.tracing then M.trace "malloc" "STart\n";
if M.tracing then M.trace "relationalArray" "STart before_end=%a after_start=%a\n" Idx.pretty (Idx.lt v l) Idx.pretty (Idx.ge v (Idx.of_int Cil.ILong BI.zero));

if M.tracing then M.trace "relationalArray" "arrExpDim , e=%a\n" (docOpt (d_exp())) e;
let idx_before_end =
match idx_before_end with
| None ->
Expand Down Expand Up @@ -1125,9 +1123,9 @@ struct
let nulls = Nulls.add_interval ~maxfull:(Idx.maximal size) Possibly (min_i, max_i) nulls in
Nulls.remove_interval Possibly (min_i, max_i) min_size nulls
in

if M.tracing then M.trace "setter" "Setting\n";
(* 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 ->
Expand Down Expand Up @@ -1822,8 +1820,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
Expand Down
8 changes: 1 addition & 7 deletions src/cdomain/value/cdomains/arrayDomain.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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. *)
Expand Down Expand Up @@ -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

Expand Down
Loading

0 comments on commit 599e67e

Please sign in to comment.