Skip to content

Commit

Permalink
Add kinds to unknown_ptr, not_null and top_ptr calls
Browse files Browse the repository at this point in the history
  • Loading branch information
karoliineh committed Sep 4, 2023
1 parent 9b5ca80 commit f43c594
Show file tree
Hide file tree
Showing 4 changed files with 20 additions and 14 deletions.
8 changes: 4 additions & 4 deletions src/analyses/base.ml
Original file line number Diff line number Diff line change
Expand Up @@ -310,7 +310,7 @@ struct
let n = ID.neg (ID.cast_to (Cilfacade.ptrdiff_ikind ()) n) in
Address (AD.map (addToAddr n) p)
| Mod -> Int (ID.top_of (Cilfacade.ptrdiff_ikind ())) (* we assume that address is actually casted to int first*)
| _ -> Address (AD.top_ptr Unknown)
| _ -> Address (AD.top_ptr PointerArithmetic)
in
(* The main function! *)
match a1,a2 with
Expand Down Expand Up @@ -1044,7 +1044,7 @@ struct
| Bot -> AD.bot ()
| _ ->
M.debug ~category:Analyzer "Failed evaluating %a to lvalue" d_lval lval;
AD.unknown_ptr Unknown
AD.unknown_ptr TypeMismatch
end

(* run eval_rv from above and keep a result that is bottom *)
Expand Down Expand Up @@ -2300,8 +2300,8 @@ struct
| 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 -> AD.top_ptr Unknown
| _ -> AD.top_ptr Unknown (* TODO: why does this ever happen? *)
| Int i -> AD.top_ptr Cast
| _ -> AD.top_ptr TypeMismatch (* TODO: why does this ever happen? *)
in
let p_addr' = AD.remove NullPtr p_addr in (* realloc with NULL is same as malloc, remove to avoid unknown value from NullPtr access *)
let p_addr_get = get ask gs st p_addr' None in (* implicitly includes join of malloc value (VD.bot) *)
Expand Down
9 changes: 6 additions & 3 deletions src/cdomains/addressDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,10 @@ module Mval_outer = Mval

type unknownKind =
| Cast
| Join
| PointerArithmetic
| TypeMismatch
| Uninitialized
| Unknown
[@@deriving eq, ord, hash]

Expand Down Expand Up @@ -286,10 +289,10 @@ struct
let of_int i =
match ID.to_int i with
| x when GobOption.exists BigIntOps.(equal (zero)) x -> null_ptr
| x when GobOption.exists BigIntOps.(equal (one)) x -> not_null Unknown
| x when GobOption.exists BigIntOps.(equal (one)) x -> not_null Cast
| _ -> match ID.to_excl_list i with
| Some (xs, _) when List.exists BigIntOps.(equal (zero)) xs -> not_null Unknown
| _ -> top_ptr Unknown
| Some (xs, _) when List.exists BigIntOps.(equal (zero)) xs -> not_null Cast
| _ -> top_ptr Cast

let to_int x =
let ik = Cilfacade.ptr_ikind () in
Expand Down
3 changes: 3 additions & 0 deletions src/cdomains/addressDomain_intf.ml
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,10 @@ sig

type unknownKind =
| Cast
| Join
| PointerArithmetic
| TypeMismatch
| Uninitialized
| Unknown
[@@deriving eq, ord, hash]

Expand Down
14 changes: 7 additions & 7 deletions src/cdomains/valueDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -175,7 +175,7 @@ struct
| t when is_mutexattr_type t -> MutexAttr (MutexAttrDomain.top ())
| TInt (ik,_) -> Int (ID.top_of ik)
| TFloat (fkind, _) when not (Cilfacade.isComplexFKind fkind) -> Float (FD.top_of fkind)
| TPtr _ -> Address (AD.top_ptr Unknown)
| TPtr _ -> Address (AD.top_ptr Uninitialized)
| TComp ({cstruct=true; _} as ci,_) -> Struct (Structs.create (fun fd -> init_value ~varAttr:fd.fattr fd.ftype) ci)
| TComp ({cstruct=false; _},_) -> Union (Unions.top ())
| TArray (ai, length, _) ->
Expand Down Expand Up @@ -454,11 +454,11 @@ struct
| TPtr (t,_) ->
Address (match v with
| Int x when ID.to_int x = Some BI.zero -> AD.null_ptr
| Int x -> AD.top_ptr Unknown
| Int x -> AD.top_ptr Cast
(* we ignore casts to void*! TODO report UB! *)
| Address x -> (match t with TVoid _ -> x | _ -> cast_addr t x)
(*| Address x -> x*)
| _ -> log_top __POS__; AD.top_ptr Unknown
| _ -> log_top __POS__; AD.top_ptr Cast
)
| TArray (ta, l, _) -> (* TODO, why is the length exp option? *)
(* TODO handle casts between different sizes? *)
Expand Down Expand Up @@ -541,8 +541,8 @@ struct
| (Int x, Address y)
| (Address y, Int x) -> Address (match ID.to_int x with
| Some x when BI.equal x BI.zero -> AD.join AD.null_ptr y
| Some x -> AD.(join y (not_null Unknown))
| None -> AD.join y (AD.top_ptr Unknown))
| Some x -> AD.(join y (not_null Join))
| None -> AD.join y (AD.top_ptr Join))
| (Address x, Address y) -> Address (AD.join x y)
| (Struct x, Struct y) -> Struct (Structs.join x y)
| (Union x, Union y) -> Union (Unions.join x y)
Expand Down Expand Up @@ -576,8 +576,8 @@ struct
| (Int x, Address y)
| (Address y, Int x) -> Address (match ID.to_int x with
| Some x when BI.equal x BI.zero -> AD.widen AD.null_ptr (AD.join AD.null_ptr y)
| Some x -> AD.(widen y (join y (not_null Unknown)))
| None -> AD.widen y (AD.join y (AD.top_ptr Unknown)))
| Some x -> AD.(widen y (join y (not_null Join)))
| None -> AD.widen y (AD.join y (AD.top_ptr Join)))
| (Address x, Address y) -> Address (AD.widen x y)
| (Struct x, Struct y) -> Struct (Structs.widen x y)
| (Union x, Union y) -> Union (Unions.widen x y)
Expand Down

0 comments on commit f43c594

Please sign in to comment.