Skip to content

Commit

Permalink
Merge branch 'master' into relational-substring-domain
Browse files Browse the repository at this point in the history
  • Loading branch information
@nathanschmidt
nathanschmidt committed Sep 8, 2023
2 parents 5bcac4a + f47d983 commit 36e66dd
Show file tree
Hide file tree
Showing 18 changed files with 1,084 additions and 427 deletions.
2 changes: 1 addition & 1 deletion src/analyses/accessAnalysis.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ struct
let access_one_top ?(force=false) ?(deref=false) ctx (kind: AccessKind.t) reach exp =
if M.tracing then M.traceli "access" "access_one_top %a (kind = %a, reach = %B, deref = %B)\n" CilType.Exp.pretty exp AccessKind.pretty kind reach deref;
if force || !collect_local || !emit_single_threaded || ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) then (
if deref then
if deref && Cil.isPointerType (Cilfacade.typeOf exp) then (* avoid dereferencing integers to unknown pointers, which cause many spurious type-based accesses *)
do_access ctx kind reach exp;
if M.tracing then M.tracei "access" "distribute_access_exp\n";
Access.distribute_access_exp (do_access ctx Read false) exp;
Expand Down
55 changes: 43 additions & 12 deletions src/analyses/base.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -462,7 +462,7 @@ struct
let var = get_var a gs st x in
let v = VD.eval_offset (Queries.to_value_domain_ask a) (fun x -> get a gs st x exp) var offs exp (Some (Var x, Offs.to_cil_offset offs)) x.vtype in
if M.tracing then M.tracec "get" "var = %a, %a = %a\n" VD.pretty var AD.pretty (AD.of_mval (x, offs)) VD.pretty v;
if full then v else match v with
if full then var else match v with
| Blob (c,s,_) -> c
| x -> x
in
Expand Down Expand Up @@ -1261,11 +1261,22 @@ struct
(* ignore @@ printf "BlobSize %a MayPointTo %a\n" d_plainexp e VD.pretty p; *)
match p with
| Address a ->
let r = get ~full:true (Analyses.ask_of_ctx ctx) ctx.global ctx.local a None in
(* ignore @@ printf "BlobSize %a = %a\n" d_plainexp e VD.pretty r; *)
(match r with
| Blob (_,s,_) -> `Lifted s
| _ -> Queries.Result.top q)
let s = addrToLvalSet a in
let has_offset = function
| `NoOffset -> false
| `Field _
| `Index _ -> true
in
(* If there's a non-heap var or an offset in the lval set, we answer with bottom *)
if ValueDomainQueries.LS.exists (fun (v, o) -> (not @@ ctx.ask (Queries.IsHeapVar v)) || has_offset o) s then
Queries.Result.bot q
else (
let r = get ~full:true (Analyses.ask_of_ctx ctx) ctx.global ctx.local a None in
(* ignore @@ printf "BlobSize %a = %a\n" d_plainexp e VD.pretty r; *)
(match r with
| Blob (_,s,_) -> `Lifted s
| _ -> Queries.Result.top q)
)
| _ -> Queries.Result.top q
end
| Q.MayPointTo e -> begin
Expand Down Expand Up @@ -1428,9 +1439,13 @@ struct
let new_value = VD.update_offset (Queries.to_value_domain_ask a) old_value offs projected_value lval_raw ((Var x), cil_offset) t in
if WeakUpdates.mem x st.weak then
VD.join old_value new_value
else if invariant then
else if invariant then (
(* without this, invariant for ambiguous pointer might worsen precision for each individual address to their join *)
VD.meet old_value new_value
try
VD.meet old_value new_value
with Lattice.Uncomparable ->
new_value
)
else
new_value
in
Expand Down Expand Up @@ -2015,6 +2030,16 @@ struct
let st' = invalidate ~deep:false ~ctx (Analyses.ask_of_ctx ctx) gs st shallow_addrs in
invalidate ~deep:true ~ctx (Analyses.ask_of_ctx ctx) gs st' deep_addrs

let check_free_of_non_heap_mem ctx special_fn ptr =
match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local ptr with
| Address a ->
let points_to_set = addrToLvalSet a in
if Q.LS.is_top points_to_set then
M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Points-to set for pointer %a in function %s is top. Potential free of non-dynamically allocated memory may occur" d_exp ptr special_fn.vname
else if (Q.LS.exists (fun (v, _) -> not (ctx.ask (Q.IsHeapVar v))) points_to_set) || (AD.mem Addr.UnknownPtr a) then
M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Free of non-dynamically allocated memory in function %s for pointer %a" special_fn.vname d_exp ptr
| _ -> M.warn ~category:MessageCategory.Analyzer "Pointer %a in function %s doesn't evaluate to a valid address." d_exp ptr special_fn.vname

let special ctx (lv:lval option) (f: varinfo) (args: exp list) =
let invalidate_ret_lv st = match lv with
| Some lv ->
Expand Down Expand Up @@ -2295,6 +2320,8 @@ struct
| _ -> st
end
| Realloc { ptr = p; size }, _ ->
(* Realloc shouldn't be passed non-dynamically allocated memory *)
check_free_of_non_heap_mem ctx f p;
begin match lv with
| Some lv ->
let ask = Analyses.ask_of_ctx ctx in
Expand Down Expand Up @@ -2326,6 +2353,10 @@ struct
| None ->
st
end
| Free ptr, _ ->
(* Free shouldn't be passed non-dynamically allocated memory *)
check_free_of_non_heap_mem ctx f ptr;
st
| Assert { exp; refine; _ }, _ -> assert_fn ctx exp refine
| Setjmp { env }, _ ->
let ask = Analyses.ask_of_ctx ctx in
Expand Down Expand Up @@ -2365,10 +2396,10 @@ struct
set ~ctx ~t_override:t ask ctx.global ctx.local (AD.of_var !longjmp_return) t rv (* Not raising Deadcode here, deadcode is raised at a higher level! *)
| Rand, _ ->
begin match lv with
| Some x ->
let result:value = (Int (ID.starting IInt Z.zero)) in
set ~ctx (Analyses.ask_of_ctx ctx) gs st (eval_lv (Analyses.ask_of_ctx ctx) ctx.global st x) (Cilfacade.typeOfLval x) result
| None -> st
| Some x ->
let result:value = (Int (ID.starting IInt Z.zero)) in
set ~ctx (Analyses.ask_of_ctx ctx) gs st (eval_lv (Analyses.ask_of_ctx ctx) ctx.global st x) (Cilfacade.typeOfLval x) result
| None -> st
end
| _, _ ->
let st =
Expand Down
55 changes: 53 additions & 2 deletions src/analyses/baseInvariant.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -545,6 +545,11 @@ struct
in
let eval e st = eval_rv a gs st e in
let eval_bool e st = match eval e st with Int i -> ID.to_bool i | _ -> None in
let unroll_fk_of_exp e =
match unrollType (Cilfacade.typeOf e) with
| TFloat (fk, _) -> fk
| _ -> failwith "value which was expected to be a float is of different type?!"
in
let rec inv_exp c_typed exp (st:D.t): D.t =
(* trying to improve variables in an expression so it is bottom means dead code *)
if VD.is_bot_value c_typed then contra st
Expand Down Expand Up @@ -681,6 +686,7 @@ struct
| Lval x, (Int _ | Float _ | Address _) -> (* meet x with c *)
let update_lval c x c' pretty = refine_lv ctx a gs st c x c' pretty exp in
let t = Cil.unrollType (Cilfacade.typeOfLval x) in (* unroll type to deal with TNamed *)
if M.tracing then M.trace "invSpecial" "invariant with Lval %a, c_typed %a, type %a\n" d_lval x VD.pretty c_typed d_type t;
begin match c_typed with
| Int c ->
let c' = match t with
Expand All @@ -690,7 +696,32 @@ struct
| TFloat (fk, _) -> Float (FD.of_int fk c)
| _ -> Int c
in
update_lval c x c' ID.pretty
(* handle special calls *)
begin match t with
| TInt (ik, _) ->
begin match x with
| ((Var v), offs) ->
if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty (ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)));
let tv_opt = ID.to_bool c in
begin match tv_opt with
| Some tv ->
begin match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)) with
| `Lifted (Isfinite xFloat) when tv -> inv_exp (Float (FD.finite (unroll_fk_of_exp xFloat))) xFloat st
| `Lifted (Isnan xFloat) when tv -> inv_exp (Float (FD.nan_of (unroll_fk_of_exp xFloat))) xFloat st
(* should be correct according to C99 standard*)
| `Lifted (Isgreater (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))) st
| `Lifted (Isgreaterequal (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Ge, xFloat, yFloat, (typeOf xFloat))) st
| `Lifted (Isless (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))) st
| `Lifted (Islessequal (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Le, xFloat, yFloat, (typeOf xFloat))) st
| `Lifted (Islessgreater (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (LOr, (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))), (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))), (TInt (IBool, [])))) st
| _ -> update_lval c x c' ID.pretty
end
| None -> update_lval c x c' ID.pretty
end
| _ -> update_lval c x c' ID.pretty
end
| _ -> update_lval c x c' ID.pretty
end
| Float c ->
let c' = match t with
(* | TPtr _ -> ..., pointer conversion from/to float is not supported *)
Expand All @@ -700,7 +731,27 @@ struct
| TFloat (fk, _) -> Float (FD.cast_to fk c)
| _ -> Float c
in
update_lval c x c' FD.pretty
(* handle special calls *)
begin match t with
| TFloat (fk, _) ->
begin match x with
| ((Var v), offs) ->
if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty (ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)));
begin match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)) with
| `Lifted (Ceil (ret_fk, xFloat)) -> inv_exp (Float (FD.inv_ceil (FD.cast_to ret_fk c))) xFloat st
| `Lifted (Floor (ret_fk, xFloat)) -> inv_exp (Float (FD.inv_floor (FD.cast_to ret_fk c))) xFloat st
| `Lifted (Fabs (ret_fk, xFloat)) ->
let inv = FD.inv_fabs (FD.cast_to ret_fk c) in
if FD.is_bot inv then
raise Analyses.Deadcode
else
inv_exp (Float inv) xFloat st
| _ -> update_lval c x c' FD.pretty
end
| _ -> update_lval c x c' FD.pretty
end
| _ -> update_lval c x c' FD.pretty
end
| Address c ->
let c' = c_typed in (* TODO: need any of the type-matching nonsense? *)
update_lval c x c' AD.pretty
Expand Down
98 changes: 72 additions & 26 deletions src/analyses/libraryDesc.ml
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(** Library function descriptor (specification). *)

module Cil = GoblintCil

open Cil
(** Pointer argument access specification. *)
module Access =
struct
Expand All @@ -14,31 +14,31 @@ struct
end

type math =
| Nan of (Cil.fkind * Cil.exp)
| Inf of Cil.fkind
| Isfinite of Cil.exp
| Isinf of Cil.exp
| Isnan of Cil.exp
| Isnormal of Cil.exp
| Signbit of Cil.exp
| Isgreater of (Cil.exp * Cil.exp)
| Isgreaterequal of (Cil.exp * Cil.exp)
| Isless of (Cil.exp * Cil.exp)
| Islessequal of (Cil.exp * Cil.exp)
| Islessgreater of (Cil.exp * Cil.exp)
| Isunordered of (Cil.exp * Cil.exp)
| Ceil of (Cil.fkind * Cil.exp)
| Floor of (Cil.fkind * Cil.exp)
| Fabs of (Cil.fkind * Cil.exp)
| Fmax of (Cil.fkind * Cil.exp * Cil.exp)
| Fmin of (Cil.fkind * Cil.exp * Cil.exp)
| Acos of (Cil.fkind * Cil.exp)
| Asin of (Cil.fkind * Cil.exp)
| Atan of (Cil.fkind * Cil.exp)
| Atan2 of (Cil.fkind * Cil.exp * Cil.exp)
| Cos of (Cil.fkind * Cil.exp)
| Sin of (Cil.fkind * Cil.exp)
| Tan of (Cil.fkind * Cil.exp)
| Nan of (CilType.Fkind.t * Basetype.CilExp.t)
| Inf of CilType.Fkind.t
| Isfinite of Basetype.CilExp.t
| Isinf of Basetype.CilExp.t
| Isnan of Basetype.CilExp.t
| Isnormal of Basetype.CilExp.t
| Signbit of Basetype.CilExp.t
| Isgreater of (Basetype.CilExp.t * Basetype.CilExp.t)
| Isgreaterequal of (Basetype.CilExp.t * Basetype.CilExp.t)
| Isless of (Basetype.CilExp.t * Basetype.CilExp.t)
| Islessequal of (Basetype.CilExp.t * Basetype.CilExp.t)
| Islessgreater of (Basetype.CilExp.t * Basetype.CilExp.t)
| Isunordered of (Basetype.CilExp.t * Basetype.CilExp.t)
| Ceil of (CilType.Fkind.t * Basetype.CilExp.t)
| Floor of (CilType.Fkind.t * Basetype.CilExp.t)
| Fabs of (CilType.Fkind.t * Basetype.CilExp.t)
| Fmax of (CilType.Fkind.t * Basetype.CilExp.t * Basetype.CilExp.t)
| Fmin of (CilType.Fkind.t * Basetype.CilExp.t * Basetype.CilExp.t)
| Acos of (CilType.Fkind.t * Basetype.CilExp.t)
| Asin of (CilType.Fkind.t * Basetype.CilExp.t)
| Atan of (CilType.Fkind.t * Basetype.CilExp.t)
| Atan2 of (CilType.Fkind.t * Basetype.CilExp.t * Basetype.CilExp.t)
| Cos of (CilType.Fkind.t * Basetype.CilExp.t)
| Sin of (CilType.Fkind.t * Basetype.CilExp.t)
| Tan of (CilType.Fkind.t * Basetype.CilExp.t) [@@deriving eq, ord, hash]

(** Type of special function, or {!Unknown}. *)
(* Use inline record if not single {!Cil.exp} argument. *)
Expand Down Expand Up @@ -152,3 +152,49 @@ let of_old ?(attrs: attr list=[]) (old_accesses: Accesses.old) (classify_name):
accs = Accesses.of_old old_accesses;
special = special_of_old classify_name;
}

module MathPrintable = struct
include Printable.StdLeaf
type t = math [@@deriving eq, ord, hash]

let name () = "MathPrintable"

let pretty () = function
| Nan (fk, exp) -> Pretty.dprintf "(%a )nan(%a)" d_fkind fk d_exp exp
| Inf fk -> Pretty.dprintf "(%a )inf()" d_fkind fk
| Isfinite exp -> Pretty.dprintf "isFinite(%a)" d_exp exp
| Isinf exp -> Pretty.dprintf "isInf(%a)" d_exp exp
| Isnan exp -> Pretty.dprintf "isNan(%a)" d_exp exp
| Isnormal exp -> Pretty.dprintf "isNormal(%a)" d_exp exp
| Signbit exp -> Pretty.dprintf "signbit(%a)" d_exp exp
| Isgreater (exp1, exp2) -> Pretty.dprintf "isGreater(%a, %a)" d_exp exp1 d_exp exp2
| Isgreaterequal (exp1, exp2) -> Pretty.dprintf "isGreaterEqual(%a, %a)" d_exp exp1 d_exp exp2
| Isless (exp1, exp2) -> Pretty.dprintf "isLess(%a, %a)" d_exp exp1 d_exp exp2
| Islessequal (exp1, exp2) -> Pretty.dprintf "isLessEqual(%a, %a)" d_exp exp1 d_exp exp2
| Islessgreater (exp1, exp2) -> Pretty.dprintf "isLessGreater(%a, %a)" d_exp exp1 d_exp exp2
| Isunordered (exp1, exp2) -> Pretty.dprintf "isUnordered(%a, %a)" d_exp exp1 d_exp exp2
| Ceil (fk, exp) -> Pretty.dprintf "(%a )ceil(%a)" d_fkind fk d_exp exp
| Floor (fk, exp) -> Pretty.dprintf "(%a )floor(%a)" d_fkind fk d_exp exp
| Fabs (fk, exp) -> Pretty.dprintf "(%a )fabs(%a)" d_fkind fk d_exp exp
| Fmax (fk, exp1, exp2) -> Pretty.dprintf "(%a )fmax(%a, %a)" d_fkind fk d_exp exp1 d_exp exp2
| Fmin (fk, exp1, exp2) -> Pretty.dprintf "(%a )fmin(%a, %a)" d_fkind fk d_exp exp1 d_exp exp2
| Acos (fk, exp) -> Pretty.dprintf "(%a )acos(%a)" d_fkind fk d_exp exp
| Asin (fk, exp) -> Pretty.dprintf "(%a )asin(%a)" d_fkind fk d_exp exp
| Atan (fk, exp) -> Pretty.dprintf "(%a )atan(%a)" d_fkind fk d_exp exp
| Atan2 (fk, exp1, exp2) -> Pretty.dprintf "(%a )atan2(%a, %a)" d_fkind fk d_exp exp1 d_exp exp2
| Cos (fk, exp) -> Pretty.dprintf "(%a )cos(%a)" d_fkind fk d_exp exp
| Sin (fk, exp) -> Pretty.dprintf "(%a )sin(%a)" d_fkind fk d_exp exp
| Tan (fk, exp) -> Pretty.dprintf "(%a )tan(%a)" d_fkind fk d_exp exp

include Printable.SimplePretty (
struct
type nonrec t = t
let pretty = pretty
end
)
end

module MathLifted = Lattice.Flat (MathPrintable) (struct
let top_name = "Unknown or no math desc"
let bot_name = "Nonexistent math desc"
end)
Loading

0 comments on commit 36e66dd

Please sign in to comment.