Summary: This commit is for Inferbo: Infer-based buffer overrun analyzer. Closes https://github.com/facebook/infer/pull/549 Reviewed By: jvillard Differential Revision: D4439297 Pulled By: sblackshear fbshipit-source-id: ddfb5bamaster
Kihong Heo
8 years ago
committed by
Facebook Github Bot
parent
c5e962e231
commit
cef2f0e055
@ -0,0 +1,3 @@
|
||||
Kihong Heo <khheo@ropas.snu.ac.kr>
|
||||
Sungkeun Cho <skcho@ropas.snu.ac.kr>
|
||||
Kwangkeun Yi <kwang@ropas.snu.ac.kr>
|
||||
@ -0,0 +1,76 @@
|
||||
(*
|
||||
* Copyright (c) 2016 - present
|
||||
*
|
||||
* Programming Research Laboratory (ROPAS)
|
||||
* Seoul National University, Korea
|
||||
* All rights reserved.
|
||||
*
|
||||
* This source code is licensed under the BSD style license found in the
|
||||
* LICENSE file in the root directory of this source tree. An additional grant
|
||||
* of patent rights can be found in the PATENTS file in the same directory.
|
||||
*)
|
||||
|
||||
module F = Format
|
||||
|
||||
module Allocsite =
|
||||
struct
|
||||
include String
|
||||
let pp fmt s = Format.fprintf fmt "%s" s
|
||||
let make x = x
|
||||
end
|
||||
|
||||
module Loc =
|
||||
struct
|
||||
type t =
|
||||
| Var of Var.t
|
||||
| Allocsite of Allocsite.t
|
||||
| Field of t * Ident.fieldname
|
||||
[@@deriving compare]
|
||||
|
||||
let rec pp fmt = function
|
||||
| Var v ->
|
||||
Var.pp F.str_formatter v;
|
||||
let s = F.flush_str_formatter () in
|
||||
if s.[0] = '&' then
|
||||
F.fprintf fmt "%s" (String.sub s 1 (String.length s - 1))
|
||||
else F.fprintf fmt "%s" s
|
||||
| Allocsite a -> Allocsite.pp fmt a
|
||||
| Field (l, f) -> F.fprintf fmt "%a.%a" pp l Ident.pp_fieldname f
|
||||
let is_var = function Var _ -> true | _ -> false
|
||||
let is_pvar_in_reg v =
|
||||
Var.pp F.str_formatter v;
|
||||
let s = F.flush_str_formatter () in
|
||||
s.[0] = '&'
|
||||
let is_logical_var = function
|
||||
| Var (Var.LogicalVar _) -> true
|
||||
| _ -> false
|
||||
let of_var v = Var v
|
||||
let of_allocsite a = Allocsite a
|
||||
let of_pvar pvar = Var (Var.of_pvar pvar)
|
||||
let of_id id = Var (Var.of_id id)
|
||||
let append_field l f = Field (l, f)
|
||||
|
||||
let is_return = function
|
||||
| Var (Var.ProgramVar x) ->
|
||||
Mangled.equal (Pvar.get_name x) Ident.name_return
|
||||
| _ -> false
|
||||
end
|
||||
|
||||
module PowLoc =
|
||||
struct
|
||||
include AbstractDomain.FiniteSet
|
||||
(struct
|
||||
include Set.Make (struct type t = Loc.t [@@deriving compare] end)
|
||||
let pp_element fmt e = Loc.pp fmt e
|
||||
let pp fmt s =
|
||||
Format.fprintf fmt "{";
|
||||
iter (fun e -> Format.fprintf fmt "%a," pp_element e) s;
|
||||
Format.fprintf fmt "}"
|
||||
end)
|
||||
|
||||
let bot = empty
|
||||
|
||||
let of_pvar pvar = singleton (Loc.of_pvar pvar)
|
||||
let of_id id = singleton (Loc.of_id id)
|
||||
let append_field ploc fn = fold (fun l -> add (Loc.append_field l fn)) ploc empty
|
||||
end
|
||||
@ -0,0 +1,199 @@
|
||||
(*
|
||||
* Copyright (c) 2016 - present
|
||||
*
|
||||
* Programming Research Laboratory (ROPAS)
|
||||
* Seoul National University, Korea
|
||||
* All rights reserved.
|
||||
*
|
||||
* This source code is licensed under the BSD style license found in the
|
||||
* LICENSE file in the root directory of this source tree. An additional grant
|
||||
* of patent rights can be found in the PATENTS file in the same directory.
|
||||
*)
|
||||
|
||||
(* Abstract Array Block *)
|
||||
open! IStd
|
||||
open AbsLoc
|
||||
|
||||
module ArrInfo =
|
||||
struct
|
||||
type t =
|
||||
{ offset : Itv.t;
|
||||
size : Itv.t;
|
||||
stride : Itv.t; }
|
||||
[@@deriving compare]
|
||||
|
||||
type astate = t
|
||||
|
||||
let bot : t
|
||||
= { offset = Itv.bot; size = Itv.bot; stride = Itv.bot; }
|
||||
|
||||
let initial : t
|
||||
= bot
|
||||
|
||||
let top : t
|
||||
= { offset = Itv.top; size = Itv.top; stride = Itv.top; }
|
||||
|
||||
let input : t
|
||||
= { offset = Itv.zero; size = Itv.pos; stride = Itv.one; }
|
||||
|
||||
let make : Itv.t * Itv.t * Itv.t -> t
|
||||
= fun (o, s, stride) -> { offset = o; size = s; stride = stride; }
|
||||
|
||||
let join : t -> t -> t
|
||||
= fun a1 a2 ->
|
||||
if phys_equal a1 a2 then a2 else
|
||||
{ offset = Itv.join a1.offset a2.offset;
|
||||
size = Itv.join a1.size a2.size;
|
||||
stride = Itv.join a1.stride a2.stride; }
|
||||
|
||||
let widen : prev:t -> next:t -> num_iters:int -> t
|
||||
= fun ~prev ~next ~num_iters ->
|
||||
if phys_equal prev next then next else
|
||||
{ offset = Itv.widen ~prev:prev.offset ~next:next.offset ~num_iters;
|
||||
size = Itv.widen ~prev:prev.size ~next:next.size ~num_iters;
|
||||
stride = Itv.widen ~prev:prev.stride ~next:next.stride ~num_iters; }
|
||||
|
||||
let eq : t -> t -> bool
|
||||
= fun a1 a2 ->
|
||||
if phys_equal a1 a2 then true else
|
||||
Itv.eq a1.offset a2.offset
|
||||
&& Itv.eq a1.size a2.size
|
||||
&& Itv.eq a1.stride a2.stride
|
||||
|
||||
let (<=) : lhs:t -> rhs:t -> bool
|
||||
= fun ~lhs ~rhs ->
|
||||
if phys_equal lhs rhs then true else
|
||||
Itv.le ~lhs:lhs.offset ~rhs:rhs.offset
|
||||
&& Itv.le ~lhs:lhs.size ~rhs:rhs.size
|
||||
&& Itv.le ~lhs:lhs.stride ~rhs:rhs.stride
|
||||
|
||||
let weak_plus_size : t -> Itv.t -> t
|
||||
= fun arr i -> { arr with size = Itv.join arr.size (Itv.plus i arr.size) }
|
||||
|
||||
let plus_offset : t -> Itv.t -> t
|
||||
= fun arr i -> { arr with offset = Itv.plus arr.offset i }
|
||||
|
||||
let minus_offset : t -> Itv.astate -> t
|
||||
= fun arr i -> { arr with offset = Itv.minus arr.offset i }
|
||||
|
||||
let diff : t -> t -> Itv.astate
|
||||
= fun arr1 arr2 ->
|
||||
let i1 = Itv.mult arr1.offset arr1.stride in
|
||||
let i2 = Itv.mult arr2.offset arr2.stride in
|
||||
Itv.minus i1 i2
|
||||
|
||||
let subst : t -> Itv.Bound.t Itv.SubstMap.t -> t
|
||||
= fun arr subst_map ->
|
||||
{ arr with offset = Itv.subst arr.offset subst_map;
|
||||
size = Itv.subst arr.size subst_map; }
|
||||
|
||||
let pp : Format.formatter -> t -> unit
|
||||
= fun fmt arr ->
|
||||
Format.fprintf fmt "offset : %a, size : %a"
|
||||
Itv.pp arr.offset Itv.pp arr.size
|
||||
|
||||
let get_symbols : t -> Itv.Symbol.t list
|
||||
= fun arr ->
|
||||
let s1 = Itv.get_symbols arr.offset in
|
||||
let s2 = Itv.get_symbols arr.size in
|
||||
let s3 = Itv.get_symbols arr.stride in
|
||||
IList.flatten [s1; s2; s3]
|
||||
|
||||
let normalize : t -> t
|
||||
= fun arr ->
|
||||
{ offset = Itv.normalize arr.offset;
|
||||
size = Itv.normalize arr.size;
|
||||
stride = Itv.normalize arr.stride }
|
||||
|
||||
let prune_comp : Binop.t -> t -> t -> t
|
||||
= fun c arr1 arr2 ->
|
||||
{ arr1 with offset = Itv.prune_comp c arr1.offset arr2.offset }
|
||||
|
||||
let prune_eq : t -> t -> t
|
||||
= fun arr1 arr2 -> { arr1 with offset = Itv.prune_eq arr1.offset arr2.offset }
|
||||
|
||||
let prune_ne : t -> t -> t
|
||||
= fun arr1 arr2 -> { arr1 with offset = Itv.prune_ne arr1.offset arr2.offset }
|
||||
end
|
||||
|
||||
module PPMap =
|
||||
struct
|
||||
include PrettyPrintable.MakePPMap (struct
|
||||
include Allocsite
|
||||
let pp_key f k = pp f k
|
||||
end)
|
||||
|
||||
let pp ~pp_value fmt m =
|
||||
let pp_item fmt (k, v) = F.fprintf fmt "(%a, %a)" pp_key k pp_value v in
|
||||
PrettyPrintable.pp_collection ~pp_item fmt (bindings m)
|
||||
end
|
||||
|
||||
include AbstractDomain.Map (PPMap) (ArrInfo)
|
||||
|
||||
let bot : astate
|
||||
= empty
|
||||
|
||||
let make : Allocsite.t -> Itv.t -> Itv.t -> Itv.t -> astate
|
||||
= fun a o sz st -> add a (ArrInfo.make (o, sz, st)) bot
|
||||
|
||||
let offsetof : astate -> Itv.t
|
||||
= fun a -> fold (fun _ arr -> Itv.join arr.ArrInfo.offset) a Itv.bot
|
||||
|
||||
let sizeof : astate -> Itv.t
|
||||
= fun a -> fold (fun _ arr -> Itv.join arr.ArrInfo.size) a Itv.bot
|
||||
|
||||
let extern : string -> astate
|
||||
= fun allocsite -> add allocsite ArrInfo.top empty
|
||||
|
||||
let input : string -> astate
|
||||
= fun allocsite -> add allocsite ArrInfo.input empty
|
||||
|
||||
let weak_plus_size : astate -> Itv.t -> astate
|
||||
= fun arr i -> map (fun a -> ArrInfo.weak_plus_size a i) arr
|
||||
|
||||
let plus_offset : astate -> Itv.t -> astate
|
||||
= fun arr i -> map (fun a -> ArrInfo.plus_offset a i) arr
|
||||
|
||||
let minus_offset : astate -> Itv.t -> astate
|
||||
= fun arr i -> map (fun a -> ArrInfo.minus_offset a i) arr
|
||||
|
||||
let diff : astate -> astate -> Itv.t
|
||||
= fun arr1 arr2 ->
|
||||
let diff_join k a2 acc =
|
||||
match find k arr1 with
|
||||
| a1 -> Itv.join acc (ArrInfo.diff a1 a2)
|
||||
| exception Not_found -> acc
|
||||
in
|
||||
fold diff_join arr2 Itv.bot
|
||||
|
||||
let get_pow_loc : astate -> PowLoc.t
|
||||
= fun array ->
|
||||
let pow_loc_of_allocsite k _ acc = PowLoc.add (Loc.of_allocsite k) acc in
|
||||
fold pow_loc_of_allocsite array PowLoc.bot
|
||||
|
||||
let subst : astate -> Itv.Bound.t Itv.SubstMap.t -> astate
|
||||
= fun a subst_map -> map (fun info -> ArrInfo.subst info subst_map) a
|
||||
|
||||
let get_symbols : astate -> Itv.Symbol.t list
|
||||
= fun a ->
|
||||
IList.flatten (IList.map (fun (_, ai) -> ArrInfo.get_symbols ai) (bindings a))
|
||||
|
||||
let normalize : astate -> astate
|
||||
= fun a -> map ArrInfo.normalize a
|
||||
|
||||
let do_prune
|
||||
: (ArrInfo.t -> ArrInfo.t -> ArrInfo.t) -> astate -> astate -> astate
|
||||
= fun arr_info_prune a1 a2 ->
|
||||
if Int.equal (cardinal a2) 1 then
|
||||
let (k, v2) = choose a2 in
|
||||
if mem k a1 then add k (arr_info_prune (find k a1) v2) a1 else a1
|
||||
else a1
|
||||
|
||||
let prune_comp : Binop.t -> astate -> astate -> astate
|
||||
= fun c a1 a2 -> do_prune (ArrInfo.prune_comp c) a1 a2
|
||||
|
||||
let prune_eq : astate -> astate -> astate
|
||||
= fun a1 a2 -> do_prune ArrInfo.prune_eq a1 a2
|
||||
|
||||
let prune_ne : astate -> astate -> astate
|
||||
= fun a1 a2 -> do_prune ArrInfo.prune_ne a1 a2
|
||||
@ -0,0 +1,461 @@
|
||||
(*
|
||||
* Copyright (c) 2016 - present
|
||||
*
|
||||
* Programming Research Laboratory (ROPAS)
|
||||
* Seoul National University, Korea
|
||||
* All rights reserved.
|
||||
*
|
||||
* This source code is licensed under the BSD style license found in the
|
||||
* LICENSE file in the root directory of this source tree. An additional grant
|
||||
* of patent rights can be found in the PATENTS file in the same directory.
|
||||
*)
|
||||
|
||||
open! IStd
|
||||
open AbsLoc
|
||||
|
||||
module F = Format
|
||||
module L = Logging
|
||||
module Dom = BufferOverrunDomain
|
||||
|
||||
module Summary = Summary.Make (struct
|
||||
type summary = Dom.Summary.t
|
||||
|
||||
let update_payload astate payload =
|
||||
{ payload with Specs.buffer_overrun = Some astate }
|
||||
|
||||
let read_from_payload payload =
|
||||
payload.Specs.buffer_overrun
|
||||
end)
|
||||
|
||||
module TransferFunctions (CFG : ProcCfg.S) =
|
||||
struct
|
||||
module CFG = CFG
|
||||
module Domain = Dom.Mem
|
||||
module Sem = BufferOverrunSemantics.Make (CFG)
|
||||
|
||||
type extras = Procname.t -> Procdesc.t option
|
||||
|
||||
(* NOTE: heuristic *)
|
||||
let get_malloc_info : Exp.t -> Typ.t * Exp.t
|
||||
= function
|
||||
| Exp.BinOp (Binop.Mult, Exp.Sizeof (typ, _, _), size)
|
||||
| Exp.BinOp (Binop.Mult, size, Exp.Sizeof (typ, _, _)) -> (typ, size)
|
||||
| Exp.Sizeof (typ, _, _) -> (typ, Exp.one)
|
||||
| x -> (Typ.Tint Typ.IChar, x)
|
||||
|
||||
let model_malloc
|
||||
: Procname.t -> (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> CFG.node
|
||||
-> Dom.Mem.t -> Dom.Mem.t
|
||||
= fun pname ret params node mem ->
|
||||
match ret with
|
||||
| Some (id, _) ->
|
||||
let (typ, size) = get_malloc_info (IList.hd params |> fst) in
|
||||
let size = Sem.eval size mem (CFG.loc node) |> Dom.Val.get_itv in
|
||||
let v = Sem.eval_array_alloc pname node typ Itv.zero size 0 1 in
|
||||
Dom.Mem.add_stack (Loc.of_id id) v mem
|
||||
| _ -> mem
|
||||
|
||||
let model_realloc
|
||||
: Procname.t -> (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> CFG.node
|
||||
-> Dom.Mem.t -> Dom.Mem.t
|
||||
= fun pname ret params node mem ->
|
||||
model_malloc pname ret (IList.tl params) node mem
|
||||
|
||||
let model_natual_itv : (Ident.t * Typ.t) option -> Dom.Mem.t -> Dom.Mem.t
|
||||
= fun ret mem ->
|
||||
match ret with
|
||||
| Some (id, _) -> Dom.Mem.add_stack (Loc.of_id id) Dom.Val.nat_itv mem
|
||||
| _ -> mem
|
||||
|
||||
let model_unknown_itv : (Ident.t * Typ.t) option -> Dom.Mem.t -> Dom.Mem.t
|
||||
= fun ret mem ->
|
||||
match ret with
|
||||
Some (id, _) -> Dom.Mem.add_stack (Loc.of_id id) Dom.Val.top_itv mem
|
||||
| None -> mem
|
||||
|
||||
let model_infer_print
|
||||
: (Exp.t * Typ.t) list -> Dom.Mem.t -> Location.t -> Dom.Mem.t
|
||||
= fun params mem loc ->
|
||||
match params with
|
||||
| (e, _) :: _ ->
|
||||
(* TODO: only print when debug mode? *)
|
||||
F.fprintf F.err_formatter "@[<v>=== Infer Print === at %a@,"
|
||||
Location.pp loc;
|
||||
Dom.Val.pp F.err_formatter (Sem.eval e mem loc);
|
||||
F.fprintf F.err_formatter "@]";
|
||||
mem
|
||||
| _ -> mem
|
||||
|
||||
let handle_unknown_call
|
||||
: Procname.t -> (Ident.t * Typ.t) option -> Procname.t
|
||||
-> (Exp.t * Typ.t) list -> CFG.node -> Dom.Mem.t -> Location.t
|
||||
-> Dom.Mem.t
|
||||
= fun pname ret callee_pname params node mem loc ->
|
||||
match Procname.get_method callee_pname with
|
||||
| "malloc"
|
||||
| "__new_array" -> model_malloc pname ret params node mem
|
||||
| "realloc" -> model_realloc pname ret params node mem
|
||||
| "strlen"
|
||||
| "fgetc" -> model_natual_itv ret mem
|
||||
| "infer_print" -> model_infer_print params mem loc
|
||||
| _ -> model_unknown_itv ret mem
|
||||
|
||||
let rec declare_array
|
||||
: Procname.t -> CFG.node -> Loc.t -> Typ.t -> IntLit.t -> inst_num:int
|
||||
-> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate
|
||||
= fun pname node loc typ len ~inst_num ~dimension mem ->
|
||||
let size = IntLit.to_int len |> Itv.of_int in
|
||||
let arr =
|
||||
Sem.eval_array_alloc pname node typ Itv.zero size inst_num dimension
|
||||
in
|
||||
let mem =
|
||||
if Int.equal dimension 1
|
||||
then Dom.Mem.add_stack loc arr mem
|
||||
else Dom.Mem.add_heap loc arr mem
|
||||
in
|
||||
let loc =
|
||||
Loc.of_allocsite (Sem.get_allocsite pname node inst_num dimension)
|
||||
in
|
||||
match typ with
|
||||
| Typ.Tarray (typ, Some len) ->
|
||||
declare_array pname node loc typ len ~inst_num
|
||||
~dimension:(dimension + 1) mem
|
||||
| _ -> mem
|
||||
|
||||
let declare_symbolic_array
|
||||
: Procname.t -> Tenv.t -> CFG.node -> Loc.t -> Typ.t -> inst_num:int
|
||||
-> sym_num:int -> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate * int
|
||||
= fun pname tenv node loc typ ~inst_num ~sym_num ~dimension mem ->
|
||||
let offset = Itv.make_sym pname sym_num in
|
||||
let size = Itv.make_sym pname (sym_num + 2) in
|
||||
let arr =
|
||||
Sem.eval_array_alloc pname node typ offset size inst_num dimension
|
||||
in
|
||||
let elem_val = Dom.Val.make_sym pname (sym_num + 4) in
|
||||
let arr_loc = arr |> Dom.Val.get_array_blk |> ArrayBlk.get_pow_loc in
|
||||
let mem =
|
||||
mem
|
||||
|> Dom.Mem.add_heap loc arr
|
||||
|> Dom.Mem.strong_update_heap arr_loc elem_val
|
||||
in
|
||||
let decl_fld (mem, sym_num) (fn, typ, _) =
|
||||
let loc =
|
||||
mem |> Dom.Mem.find_heap loc |> Dom.Val.get_all_locs |> PowLoc.choose
|
||||
in
|
||||
let field = Loc.append_field loc fn in
|
||||
match typ with
|
||||
| Typ.Tint _
|
||||
| Typ.Tfloat _ ->
|
||||
let v = Dom.Val.make_sym pname sym_num in
|
||||
(Dom.Mem.add_heap field v mem, sym_num + 2)
|
||||
| Typ.Tptr (typ, _) ->
|
||||
let offset = Itv.make_sym pname sym_num in
|
||||
let size = Itv.make_sym pname (sym_num + 2) in
|
||||
let v =
|
||||
Sem.eval_array_alloc pname node typ offset size inst_num dimension
|
||||
in
|
||||
(Dom.Mem.add_heap field v mem, sym_num + 4)
|
||||
| _ -> (mem, sym_num)
|
||||
in
|
||||
match typ with
|
||||
| Typ.Tstruct typename ->
|
||||
(match Tenv.lookup tenv typename with
|
||||
| Some str ->
|
||||
IList.fold_left decl_fld (mem, sym_num + 6) str.StructTyp.fields
|
||||
| _ -> (mem, sym_num + 6))
|
||||
| _ -> (mem, sym_num + 6)
|
||||
|
||||
let declare_symbolic_parameter
|
||||
: Procdesc.t -> Tenv.t -> CFG.node -> int -> Dom.Mem.t -> Dom.Mem.t
|
||||
= fun pdesc tenv node inst_num mem ->
|
||||
let pname = Procdesc.get_proc_name pdesc in
|
||||
let add_formal (mem, inst_num, sym_num) (pvar, typ) =
|
||||
match typ with
|
||||
| Typ.Tint _ ->
|
||||
let v = Dom.Val.make_sym pname sym_num in
|
||||
let mem = Dom.Mem.add_heap (Loc.of_pvar pvar) v mem in
|
||||
(mem, inst_num + 1, sym_num + 2)
|
||||
| Typ.Tptr (typ, _) ->
|
||||
let (mem, sym_num) =
|
||||
declare_symbolic_array pname tenv node (Loc.of_pvar pvar) typ
|
||||
~inst_num ~sym_num ~dimension:1 mem
|
||||
in
|
||||
(mem, inst_num + 1, sym_num)
|
||||
| _ -> (mem, inst_num, sym_num) (* TODO: add other cases if necessary *)
|
||||
in
|
||||
IList.fold_left add_formal (mem, inst_num, 0) (Sem.get_formals pdesc)
|
||||
|> fst3
|
||||
|
||||
let instantiate_ret
|
||||
: Tenv.t -> Procdesc.t option -> Procname.t -> (Exp.t * Typ.t) list
|
||||
-> Dom.Mem.t -> Dom.Summary.t -> Location.t -> Dom.Val.astate
|
||||
= fun tenv callee_pdesc callee_pname params caller_mem summary loc ->
|
||||
let callee_entry_mem = Dom.Summary.get_input summary in
|
||||
let callee_exit_mem = Dom.Summary.get_output summary in
|
||||
match callee_pdesc with
|
||||
| Some pdesc ->
|
||||
let subst_map =
|
||||
Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem loc
|
||||
in
|
||||
let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in
|
||||
let ret_val = Dom.Mem.find_heap ret_loc callee_exit_mem in
|
||||
Dom.Val.subst ret_val subst_map
|
||||
|> Dom.Val.normalize (* normalize bottom *)
|
||||
| _ -> Dom.Val.bot
|
||||
|
||||
let print_debug_info : Sil.instr -> Dom.Mem.t -> Dom.Mem.t -> unit
|
||||
= fun instr pre post ->
|
||||
if Config.bo_debug >= 2 then
|
||||
begin
|
||||
F.fprintf F.err_formatter "@.@.================================@.";
|
||||
F.fprintf F.err_formatter "@[<v 2>Pre-state : @,";
|
||||
Dom.Mem.pp F.err_formatter pre;
|
||||
F.fprintf F.err_formatter "@]@.@.";
|
||||
Sil.pp_instr Pp.text F.err_formatter instr;
|
||||
F.fprintf F.err_formatter "@.@.";
|
||||
F.fprintf F.err_formatter "@[<v 2>Post-state : @,";
|
||||
Dom.Mem.pp F.err_formatter post;
|
||||
F.fprintf F.err_formatter "@]@.";
|
||||
F.fprintf F.err_formatter "================================@.@."
|
||||
end
|
||||
|
||||
let exec_instr
|
||||
: Dom.Mem.t -> extras ProcData.t -> CFG.node -> Sil.instr -> Dom.Mem.astate
|
||||
= fun mem { pdesc; tenv; extras } node instr ->
|
||||
let pname = Procdesc.get_proc_name pdesc in
|
||||
let try_decl_arr (mem, inst_num) (pvar, typ) =
|
||||
match typ with
|
||||
| Typ.Tarray (typ, Some len) ->
|
||||
let loc = Loc.of_var (Var.of_pvar pvar) in
|
||||
let mem =
|
||||
declare_array pname node loc typ len ~inst_num ~dimension:1 mem
|
||||
in
|
||||
(mem, inst_num + 1)
|
||||
| _ -> (mem, inst_num)
|
||||
in
|
||||
let output_mem =
|
||||
match instr with
|
||||
| Load (id, exp, _, loc) ->
|
||||
let locs = Sem.eval exp mem loc |> Dom.Val.get_all_locs in
|
||||
let v = Dom.Mem.find_heap_set locs mem in
|
||||
Dom.Mem.add_stack (Loc.of_var (Var.of_id id)) v mem
|
||||
|> Dom.Mem.load_alias id exp
|
||||
| Store (exp1, _, exp2, loc) ->
|
||||
let locs = Sem.eval exp1 mem loc |> Dom.Val.get_all_locs in
|
||||
Dom.Mem.update_mem locs (Sem.eval exp2 mem loc) mem
|
||||
|> Dom.Mem.store_alias exp1 exp2
|
||||
| Prune (exp, loc, _, _) -> Sem.prune exp loc mem
|
||||
| Call (ret, Const (Cfun callee_pname), params, loc, _) ->
|
||||
(match Summary.read_summary pdesc callee_pname with
|
||||
| Some summary ->
|
||||
let callee = extras callee_pname in
|
||||
let ret_val =
|
||||
instantiate_ret tenv callee callee_pname params mem summary loc
|
||||
in
|
||||
(match ret with
|
||||
| Some (id, _) ->
|
||||
Dom.Mem.add_stack (Loc.of_var (Var.of_id id)) ret_val mem
|
||||
| _ -> mem)
|
||||
| None ->
|
||||
handle_unknown_call pname ret callee_pname params node mem loc)
|
||||
| Declare_locals (locals, _) ->
|
||||
(* array allocation in stack e.g., int arr[10] *)
|
||||
let (mem, inst_num) = IList.fold_left try_decl_arr (mem, 1) locals in
|
||||
declare_symbolic_parameter pdesc tenv node inst_num mem
|
||||
| Call _
|
||||
| Remove_temps _
|
||||
| Abstract _
|
||||
| Nullify _ -> mem
|
||||
in
|
||||
print_debug_info instr mem output_mem;
|
||||
output_mem
|
||||
end
|
||||
|
||||
module Analyzer =
|
||||
AbstractInterpreter.Make
|
||||
(ProcCfg.Normal)
|
||||
(Scheduler.ReversePostorder)
|
||||
(TransferFunctions)
|
||||
|
||||
module Interprocedural = AbstractInterpreter.Interprocedural (Summary)
|
||||
module CFG = Analyzer.TransferFunctions.CFG
|
||||
module Sem = BufferOverrunSemantics.Make (CFG)
|
||||
|
||||
module Report =
|
||||
struct
|
||||
type extras = Procname.t -> Procdesc.t option
|
||||
|
||||
let add_condition
|
||||
: Procname.t -> CFG.node -> Exp.t -> Location.t -> Dom.Mem.astate
|
||||
-> Dom.ConditionSet.t -> Dom.ConditionSet.t
|
||||
= fun pname node exp loc mem cond_set ->
|
||||
let array_access =
|
||||
match exp with
|
||||
| Exp.Var _ ->
|
||||
let arr = Sem.eval exp mem loc |> Dom.Val.get_array_blk in
|
||||
Some (arr, Itv.zero, true)
|
||||
| Exp.Lindex (e1, e2)
|
||||
| Exp.BinOp (Binop.PlusA, e1, e2) ->
|
||||
let arr = Sem.eval e1 mem loc |> Dom.Val.get_array_blk in
|
||||
let idx = Sem.eval e2 mem loc |> Dom.Val.get_itv in
|
||||
Some (arr, idx, true)
|
||||
| Exp.BinOp (Binop.MinusA, e1, e2) ->
|
||||
let arr = Sem.eval e1 mem loc |> Dom.Val.get_array_blk in
|
||||
let idx = Sem.eval e2 mem loc |> Dom.Val.get_itv in
|
||||
Some (arr, idx, false)
|
||||
| _ -> None
|
||||
in
|
||||
match array_access with
|
||||
| Some (arr, idx, is_plus) ->
|
||||
let site = Sem.get_allocsite pname node 0 0 in
|
||||
let size = ArrayBlk.sizeof arr in
|
||||
let offset = ArrayBlk.offsetof arr in
|
||||
let idx = (if is_plus then Itv.plus else Itv.minus) offset idx in
|
||||
(if Config.bo_debug >= 2 then
|
||||
(F.fprintf F.err_formatter "@[<v 2>Add condition :@,";
|
||||
F.fprintf F.err_formatter "array: %a@," ArrayBlk.pp arr;
|
||||
F.fprintf F.err_formatter " idx: %a@," Itv.pp idx;
|
||||
F.fprintf F.err_formatter "@]@."));
|
||||
if size <> Itv.bot && idx <> Itv.bot then
|
||||
Dom.ConditionSet.add_bo_safety pname loc site ~size ~idx cond_set
|
||||
else cond_set
|
||||
| None -> cond_set
|
||||
|
||||
let instantiate_cond
|
||||
: Tenv.t -> Procname.t -> Procdesc.t option -> (Exp.t * Typ.t) list
|
||||
-> Dom.Mem.t -> Summary.summary -> Location.t -> Dom.ConditionSet.t
|
||||
= fun tenv caller_pname callee_pdesc params caller_mem summary loc ->
|
||||
let callee_entry_mem = Dom.Summary.get_input summary in
|
||||
let callee_cond = Dom.Summary.get_cond_set summary in
|
||||
match callee_pdesc with
|
||||
| Some pdesc ->
|
||||
let subst_map =
|
||||
Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem loc
|
||||
in
|
||||
let pname = Procdesc.get_proc_name pdesc in
|
||||
Dom.ConditionSet.subst callee_cond subst_map caller_pname pname loc
|
||||
| _ -> callee_cond
|
||||
|
||||
let print_debug_info : Sil.instr -> Dom.Mem.t -> Dom.ConditionSet.t -> unit
|
||||
= fun instr pre cond_set ->
|
||||
if Config.bo_debug >= 2 then
|
||||
(F.fprintf F.err_formatter "@.@.================================@.";
|
||||
F.fprintf F.err_formatter "@[<v 2>Pre-state : @,";
|
||||
Dom.Mem.pp F.err_formatter pre;
|
||||
F.fprintf F.err_formatter "@]@.@.";
|
||||
Sil.pp_instr Pp.text F.err_formatter instr;
|
||||
F.fprintf F.err_formatter "@[<v 2>@.@.";
|
||||
Dom.ConditionSet.pp F.err_formatter cond_set;
|
||||
F.fprintf F.err_formatter "@]@.";
|
||||
F.fprintf F.err_formatter "================================@.@.")
|
||||
|
||||
let collect_instr
|
||||
: extras ProcData.t -> CFG.node -> Dom.ConditionSet.t * Dom.Mem.t
|
||||
-> Sil.instr -> Dom.ConditionSet.t * Dom.Mem.t
|
||||
= fun ({ pdesc; tenv; extras } as pdata) node (cond_set, mem) instr ->
|
||||
let pname = Procdesc.get_proc_name pdesc in
|
||||
let cond_set =
|
||||
match instr with
|
||||
| Sil.Load (_, exp, _, loc)
|
||||
| Sil.Store (exp, _, _, loc) ->
|
||||
add_condition pname node exp loc mem cond_set
|
||||
| Sil.Call (_, Const (Cfun callee_pname), params, loc, _) ->
|
||||
(match Summary.read_summary pdesc callee_pname with
|
||||
| Some summary ->
|
||||
let callee = extras callee_pname in
|
||||
instantiate_cond tenv pname callee params mem summary loc
|
||||
|> Dom.ConditionSet.rm_invalid
|
||||
|> Dom.ConditionSet.join cond_set
|
||||
| _ -> cond_set)
|
||||
| _ -> cond_set
|
||||
in
|
||||
let mem = Analyzer.TransferFunctions.exec_instr mem pdata node instr in
|
||||
print_debug_info instr mem cond_set;
|
||||
(cond_set, mem)
|
||||
|
||||
let collect_instrs
|
||||
: extras ProcData.t -> CFG.node -> Sil.instr list -> Dom.Mem.t
|
||||
-> Dom.ConditionSet.t -> Dom.ConditionSet.t
|
||||
= fun pdata node instrs mem cond_set ->
|
||||
IList.fold_left (collect_instr pdata node) (cond_set, mem) instrs
|
||||
|> fst
|
||||
|
||||
let collect_node
|
||||
: extras ProcData.t -> Analyzer.invariant_map -> Dom.ConditionSet.t ->
|
||||
CFG.node -> Dom.ConditionSet.t
|
||||
= fun pdata inv_map cond_set node ->
|
||||
let instrs = CFG.instr_ids node |> IList.map fst in
|
||||
match Analyzer.extract_pre (CFG.id node) inv_map with
|
||||
| Some mem -> collect_instrs pdata node instrs mem cond_set
|
||||
| _ -> cond_set
|
||||
|
||||
let collect : extras ProcData.t -> Analyzer.invariant_map -> Dom.ConditionSet.t
|
||||
= fun ({ pdesc } as pdata) inv_map ->
|
||||
let add_node1 acc node = collect_node pdata inv_map acc node in
|
||||
Procdesc.fold_nodes add_node1 Dom.ConditionSet.empty pdesc
|
||||
|
||||
let report_error : Procdesc.t -> Dom.ConditionSet.t -> unit
|
||||
= fun pdesc conds ->
|
||||
let pname = Procdesc.get_proc_name pdesc in
|
||||
let report1 cond =
|
||||
let alarm = Dom.Condition.check cond in
|
||||
let (caller_pname, loc) =
|
||||
match Dom.Condition.get_trace cond with
|
||||
| Dom.Condition.Inter (caller_pname, _, loc) -> (caller_pname, loc)
|
||||
| Dom.Condition.Intra pname -> (pname, Dom.Condition.get_location cond)
|
||||
in
|
||||
match alarm with
|
||||
| None -> ()
|
||||
| Some bucket when Procname.equal pname caller_pname ->
|
||||
let description = Dom.Condition.to_string cond in
|
||||
let error_desc = Localise.desc_buffer_overrun bucket description in
|
||||
let exn = Exceptions.Checkers (Localise.to_string Localise.buffer_overrun, error_desc) in
|
||||
let trace = [Errlog.make_trace_element 0 loc description []] in
|
||||
Reporting.log_error pname ~loc ~ltr:trace exn
|
||||
| _ -> ()
|
||||
in
|
||||
Dom.ConditionSet.iter report1 conds
|
||||
end
|
||||
|
||||
let compute_post
|
||||
: Analyzer.TransferFunctions.extras ProcData.t -> Summary.summary option
|
||||
= fun { pdesc; tenv; extras = get_pdesc } ->
|
||||
let cfg = CFG.from_pdesc pdesc in
|
||||
let pdata = ProcData.make pdesc tenv get_pdesc in
|
||||
let pname = Procdesc.get_proc_name pdesc in
|
||||
let inv_map = Analyzer.exec_pdesc ~initial:Dom.Mem.bot pdata in
|
||||
let entry_mem =
|
||||
let entry_id = CFG.id (CFG.start_node cfg) in
|
||||
Analyzer.extract_post entry_id inv_map
|
||||
in
|
||||
let exit_mem =
|
||||
let exit_id = CFG.id (CFG.exit_node cfg) in
|
||||
Analyzer.extract_post exit_id inv_map
|
||||
in
|
||||
let cond_set = Report.collect pdata inv_map in
|
||||
Report.report_error pdesc cond_set;
|
||||
match entry_mem, exit_mem with
|
||||
| Some entry_mem, Some exit_mem ->
|
||||
Summary.write_summary pname (entry_mem, exit_mem, cond_set);
|
||||
Some (entry_mem, exit_mem, cond_set)
|
||||
| _ -> None
|
||||
|
||||
let print_summary : Procname.t -> Dom.Summary.t -> unit
|
||||
= fun proc_name s ->
|
||||
F.fprintf F.err_formatter "@.@[<v 2>Summary of %a :@,"
|
||||
Procname.pp proc_name;
|
||||
Dom.Summary.pp_summary F.err_formatter s;
|
||||
F.fprintf F.err_formatter "@]@."
|
||||
|
||||
let checker : Callbacks.proc_callback_args -> unit
|
||||
= fun ({ proc_name } as callback) ->
|
||||
let make_extras _ = callback.get_proc_desc in
|
||||
let post =
|
||||
Interprocedural.compute_and_store_post
|
||||
~compute_post
|
||||
~make_extras
|
||||
callback
|
||||
in
|
||||
match post with
|
||||
| Some s when Config.bo_debug >= 1 -> print_summary proc_name s
|
||||
| _ -> ()
|
||||
@ -0,0 +1,707 @@
|
||||
(*
|
||||
* Copyright (c) 2016 - present
|
||||
*
|
||||
* Programming Research Laboratory (ROPAS)
|
||||
* Seoul National University, Korea
|
||||
* All rights reserved.
|
||||
*
|
||||
* This source code is licensed under the BSD style license found in the
|
||||
* LICENSE file in the root directory of this source tree. An additional grant
|
||||
* of patent rights can be found in the PATENTS file in the same directory.
|
||||
*)
|
||||
|
||||
open! IStd
|
||||
open AbsLoc
|
||||
|
||||
module F = Format
|
||||
module L = Logging
|
||||
|
||||
module Condition =
|
||||
struct
|
||||
type t =
|
||||
{ idx : Itv.astate;
|
||||
size : Itv.astate;
|
||||
proc_name : Procname.t;
|
||||
loc : Location.t;
|
||||
trace : trace;
|
||||
id : string }
|
||||
[@@deriving compare]
|
||||
and trace = Intra of Procname.t
|
||||
| Inter of Procname.t * Procname.t * Location.t
|
||||
[@@deriving compare]
|
||||
|
||||
and astate = t
|
||||
|
||||
let set_size_pos : t -> t
|
||||
= fun c ->
|
||||
let size =
|
||||
if Itv.Bound.le (Itv.lb c.size) Itv.Bound.zero
|
||||
then Itv.make Itv.Bound.zero (Itv.ub c.size)
|
||||
else c.size
|
||||
in
|
||||
{ c with size }
|
||||
|
||||
let string_of_location : Location.t -> string
|
||||
= fun loc ->
|
||||
let fname = SourceFile.to_string loc.Location.file in
|
||||
let pos = Location.to_string loc in
|
||||
F.fprintf F.str_formatter "%s:%s" fname pos;
|
||||
F.flush_str_formatter ()
|
||||
|
||||
let pp_location : F.formatter -> t -> unit
|
||||
= fun fmt c ->
|
||||
F.fprintf fmt "%s" (string_of_location c.loc)
|
||||
|
||||
let pp : F.formatter -> t -> unit
|
||||
= fun fmt c ->
|
||||
let c = set_size_pos c in
|
||||
if Config.bo_debug <= 1 then
|
||||
F.fprintf fmt "%a < %a at %a" Itv.pp c.idx Itv.pp c.size pp_location c
|
||||
else
|
||||
match c.trace with
|
||||
Inter (_, pname, loc) ->
|
||||
let pname = Procname.to_string pname in
|
||||
F.fprintf fmt "%a < %a at %a by call %s() at %s"
|
||||
Itv.pp c.idx Itv.pp c.size pp_location c pname (string_of_location loc)
|
||||
| Intra _ -> F.fprintf fmt "%a < %a at %a" Itv.pp c.idx Itv.pp c.size pp_location c
|
||||
|
||||
let pp_element : F.formatter -> t -> unit
|
||||
= pp
|
||||
|
||||
let get_location : t -> Location.t
|
||||
= fun c -> c.loc
|
||||
|
||||
let get_trace : t -> trace
|
||||
= fun c -> c.trace
|
||||
|
||||
let get_proc_name : t -> Procname.t
|
||||
= fun c -> c.proc_name
|
||||
|
||||
let make : Procname.t -> Location.t -> string -> idx:Itv.t -> size:Itv.t -> t
|
||||
= fun proc_name loc id ~idx ~size ->
|
||||
{ proc_name; idx; size; loc; id ; trace = Intra proc_name }
|
||||
|
||||
let filter1 : t -> bool
|
||||
= fun c ->
|
||||
Itv.eq c.idx Itv.top || Itv.eq c.size Itv.top
|
||||
|| (try Itv.Bound.eq (Itv.lb c.idx) Itv.Bound.MInf with _ -> false)
|
||||
|| (try Itv.Bound.eq (Itv.lb c.size) Itv.Bound.MInf with _ -> false)
|
||||
|| (Itv.eq c.idx Itv.nat && Itv.eq c.size Itv.nat)
|
||||
|
||||
let filter2 : t -> bool
|
||||
= fun c ->
|
||||
(not (Itv.is_finite c.idx) || not (Itv.is_finite c.size)) (* basically, alarms involving infinify are filtered *)
|
||||
&& (* except the following cases : *)
|
||||
not ((Itv.Bound.is_not_infty (Itv.lb c.idx) && (* idx non-infty lb < 0 *)
|
||||
Itv.Bound.lt (Itv.lb c.idx) Itv.Bound.zero)
|
||||
||
|
||||
(Itv.Bound.is_not_infty (Itv.lb c.idx) && (* idx non-infty lb > size lb *)
|
||||
(Itv.Bound.gt (Itv.lb c.idx) (Itv.lb c.size)))
|
||||
||
|
||||
(Itv.Bound.is_not_infty (Itv.lb c.idx) && (* idx non-infty lb > size ub *)
|
||||
(Itv.Bound.gt (Itv.lb c.idx) (Itv.ub c.size)))
|
||||
||
|
||||
(Itv.Bound.is_not_infty (Itv.ub c.idx) && (* idx non-infty ub > size lb *)
|
||||
(Itv.Bound.gt (Itv.ub c.idx) (Itv.lb c.size)))
|
||||
||
|
||||
(Itv.Bound.is_not_infty (Itv.ub c.idx) && (* idx non-infty ub > size ub *)
|
||||
(Itv.Bound.gt (Itv.ub c.idx) (Itv.ub c.size))))
|
||||
|
||||
(* check buffer overrun and return its confidence *)
|
||||
let check : t -> string option
|
||||
= fun c ->
|
||||
if Config.bo_debug <= 1 && (Itv.is_symbolic c.idx || Itv.is_symbolic c.size)
|
||||
then None
|
||||
else if filter1 c then Some Localise.BucketLevel.b5
|
||||
else if filter2 c then Some Localise.BucketLevel.b3
|
||||
else
|
||||
let c = set_size_pos c in
|
||||
let not_overrun = Itv.lt_sem c.idx c.size in
|
||||
let not_underrun = Itv.le_sem Itv.zero c.idx in
|
||||
if (Itv.eq not_overrun Itv.one) && (Itv.eq not_underrun Itv.one) then None
|
||||
else Some Localise.BucketLevel.b1
|
||||
|
||||
let invalid : t -> bool
|
||||
= fun x -> Itv.invalid x.idx || Itv.invalid x.size
|
||||
|
||||
let to_string : t -> string
|
||||
= fun c ->
|
||||
let c = set_size_pos c in
|
||||
"Offset : " ^ Itv.to_string c.idx ^ " Size : " ^ Itv.to_string c.size
|
||||
^ " @ " ^ string_of_location c.loc
|
||||
^ (match c.trace with
|
||||
Inter (_, pname, _) ->
|
||||
" by call "
|
||||
^ Procname.to_string pname
|
||||
^ "() "
|
||||
| Intra _ -> "")
|
||||
|
||||
let subst : t -> Itv.Bound.t Itv.SubstMap.t -> Procname.t -> Procname.t -> Location.t -> t
|
||||
= fun c subst_map caller_pname callee_pname loc ->
|
||||
if Itv.is_symbolic c.idx || Itv.is_symbolic c.size then
|
||||
{ c with idx = Itv.subst c.idx subst_map;
|
||||
size = Itv.subst c.size subst_map;
|
||||
trace = Inter (caller_pname, callee_pname, loc) }
|
||||
else c
|
||||
end
|
||||
|
||||
module ConditionSet =
|
||||
struct
|
||||
module PPSet = PrettyPrintable.MakePPSet (Condition)
|
||||
include AbstractDomain.FiniteSet (PPSet)
|
||||
|
||||
module Map = Caml.Map.Make (struct
|
||||
type t = Location.t [@@deriving compare]
|
||||
end)
|
||||
|
||||
let add_bo_safety
|
||||
: Procname.t -> Location.t -> string -> idx:Itv.t -> size:Itv.t -> t -> t
|
||||
= fun pname loc id ~idx ~size cond ->
|
||||
add (Condition.make pname loc id ~idx ~size) cond
|
||||
|
||||
let subst : t -> Itv.Bound.t Itv.SubstMap.t -> Procname.t -> Procname.t -> Location.t -> t
|
||||
= fun x subst_map caller_pname callee_pname loc ->
|
||||
fold (fun e -> add (Condition.subst e subst_map caller_pname callee_pname loc)) x empty
|
||||
|
||||
let group : t -> t Map.t
|
||||
= fun x ->
|
||||
fold (fun cond map ->
|
||||
let old_set = try Map.find cond.loc map with _ -> empty in
|
||||
Map.add cond.loc (add cond old_set) map) x Map.empty
|
||||
|
||||
let pp_summary : F.formatter -> t -> unit
|
||||
= fun fmt x ->
|
||||
let pp_sep fmt () = F.fprintf fmt ", @," in
|
||||
let pp_element fmt v = Condition.pp fmt v in
|
||||
F.fprintf fmt "@[<v 0>Safety conditions:@,";
|
||||
F.fprintf fmt "@[<hov 2>{ ";
|
||||
F.pp_print_list ~pp_sep pp_element fmt (elements x);
|
||||
F.fprintf fmt " }@]";
|
||||
F.fprintf fmt "@]"
|
||||
|
||||
let pp : Format.formatter -> t -> unit
|
||||
= fun fmt x ->
|
||||
let pp_sep fmt () = F.fprintf fmt ", @," in
|
||||
let pp_element fmt v = Condition.pp fmt v in
|
||||
F.fprintf fmt "@[<v 2>Safety conditions :@,";
|
||||
F.fprintf fmt "@[<hov 1>{";
|
||||
F.pp_print_list ~pp_sep pp_element fmt (elements x);
|
||||
F.fprintf fmt " }@]";
|
||||
F.fprintf fmt "@]"
|
||||
|
||||
let rm_invalid : t -> t
|
||||
= fun x -> filter (fun c -> not (Condition.invalid c)) x
|
||||
end
|
||||
|
||||
module Val =
|
||||
struct
|
||||
type astate = {
|
||||
itv : Itv.astate;
|
||||
powloc : PowLoc.astate;
|
||||
arrayblk : ArrayBlk.astate;
|
||||
}
|
||||
|
||||
type t = astate
|
||||
|
||||
let bot : t
|
||||
= { itv = Itv.bot; powloc = PowLoc.bot; arrayblk = ArrayBlk.bot }
|
||||
|
||||
let (<=) ~lhs ~rhs =
|
||||
if phys_equal lhs rhs then true
|
||||
else
|
||||
Itv.(<=) ~lhs:(lhs.itv) ~rhs:(rhs.itv)
|
||||
&& PowLoc.(<=) ~lhs:(lhs.powloc) ~rhs:(rhs.powloc)
|
||||
&& ArrayBlk.(<=) ~lhs:(lhs.arrayblk) ~rhs:(rhs.arrayblk)
|
||||
|
||||
let widen ~prev ~next ~num_iters =
|
||||
if phys_equal prev next then prev
|
||||
else
|
||||
{ itv = Itv.widen ~prev:(prev.itv) ~next:(next.itv) ~num_iters;
|
||||
powloc = PowLoc.widen ~prev:(prev.powloc) ~next:(next.powloc) ~num_iters;
|
||||
arrayblk = ArrayBlk.widen ~prev:(prev.arrayblk) ~next:(next.arrayblk) ~num_iters; }
|
||||
|
||||
let pp fmt x =
|
||||
F.fprintf fmt "(%a, %a, %a)" Itv.pp x.itv PowLoc.pp x.powloc ArrayBlk.pp x.arrayblk
|
||||
|
||||
let join : t -> t -> t
|
||||
= fun x y ->
|
||||
if phys_equal x y then x
|
||||
else
|
||||
{ itv = Itv.join x.itv y.itv;
|
||||
powloc = PowLoc.join x.powloc y.powloc;
|
||||
arrayblk = ArrayBlk.join x.arrayblk y.arrayblk }
|
||||
|
||||
let rec joins : t list -> t
|
||||
= function
|
||||
| [] -> bot
|
||||
| [a] -> a
|
||||
| a :: b -> join a (joins b)
|
||||
|
||||
let get_itv : t -> Itv.t
|
||||
= fun x -> x.itv
|
||||
|
||||
let get_pow_loc : t -> PowLoc.t
|
||||
= fun x -> x.powloc
|
||||
|
||||
let get_array_blk : t -> ArrayBlk.astate
|
||||
= fun x -> x.arrayblk
|
||||
|
||||
let get_all_locs : t -> PowLoc.t
|
||||
= fun x -> ArrayBlk.get_pow_loc x.arrayblk |> PowLoc.join x.powloc
|
||||
|
||||
let top_itv : t
|
||||
= { bot with itv = Itv.top }
|
||||
|
||||
let pos_itv : t
|
||||
= { bot with itv = Itv.pos }
|
||||
|
||||
let nat_itv : t
|
||||
= { bot with itv = Itv.nat }
|
||||
|
||||
let of_int : int -> t
|
||||
= fun n -> { bot with itv = Itv.of_int n }
|
||||
|
||||
let of_pow_loc : PowLoc.t -> t
|
||||
= fun x -> { bot with powloc = x }
|
||||
|
||||
let of_array_blk : ArrayBlk.astate -> t
|
||||
= fun a -> { bot with arrayblk = a }
|
||||
|
||||
let zero : t
|
||||
= of_int 0
|
||||
|
||||
let modify_itv : Itv.t -> t -> t
|
||||
= fun i x -> { x with itv = i }
|
||||
|
||||
let make_sym : Procname.t -> int -> t
|
||||
= fun pname i -> { bot with itv = Itv.make_sym pname i }
|
||||
|
||||
let unknown_bit : t -> t
|
||||
= fun x -> { x with itv = Itv.top }
|
||||
|
||||
let neg : t -> t
|
||||
= fun x -> { x with itv = Itv.neg x.itv }
|
||||
|
||||
let lnot : t -> t
|
||||
= fun x -> { x with itv = Itv.lnot x.itv }
|
||||
|
||||
let lift_itv : (Itv.t -> Itv.t -> Itv.t) -> t -> t -> t
|
||||
= fun f x y -> { bot with itv = f x.itv y.itv }
|
||||
|
||||
let plus : t -> t -> t
|
||||
= fun x y ->
|
||||
{ x with itv = Itv.plus x.itv y.itv; arrayblk = ArrayBlk.plus_offset x.arrayblk y.itv }
|
||||
|
||||
let minus : t -> t -> t
|
||||
= fun x y ->
|
||||
let n = Itv.join (Itv.minus x.itv y.itv) (ArrayBlk.diff x.arrayblk y.arrayblk) in
|
||||
let a = ArrayBlk.minus_offset x.arrayblk y.itv in
|
||||
{ bot with itv = n; arrayblk = a}
|
||||
|
||||
let mult : t -> t -> t
|
||||
= lift_itv Itv.mult
|
||||
|
||||
let div : t -> t -> t
|
||||
= lift_itv Itv.div
|
||||
|
||||
let mod_sem : t -> t -> t
|
||||
= lift_itv Itv.mod_sem
|
||||
|
||||
let shiftlt : t -> t -> t
|
||||
= lift_itv Itv.shiftlt
|
||||
|
||||
let shiftrt : t -> t -> t
|
||||
= lift_itv Itv.shiftrt
|
||||
|
||||
let lt_sem : t -> t -> t
|
||||
= lift_itv Itv.lt_sem
|
||||
|
||||
let gt_sem : t -> t -> t
|
||||
= lift_itv Itv.gt_sem
|
||||
|
||||
let le_sem : t -> t -> t
|
||||
= lift_itv Itv.le_sem
|
||||
|
||||
let ge_sem : t -> t -> t
|
||||
= lift_itv Itv.ge_sem
|
||||
|
||||
let eq_sem : t -> t -> t
|
||||
= lift_itv Itv.eq_sem
|
||||
|
||||
let ne_sem : t -> t -> t
|
||||
= lift_itv Itv.ne_sem
|
||||
|
||||
let land_sem : t -> t -> t
|
||||
= lift_itv Itv.land_sem
|
||||
|
||||
let lor_sem : t -> t -> t
|
||||
= lift_itv Itv.lor_sem
|
||||
|
||||
let lift_prune1 : (Itv.t -> Itv.t) -> t -> t
|
||||
= fun f x -> { x with itv = f x.itv }
|
||||
|
||||
let lift_prune2
|
||||
: (Itv.t -> Itv.t -> Itv.t)
|
||||
-> (ArrayBlk.astate -> ArrayBlk.astate -> ArrayBlk.astate) -> t -> t -> t
|
||||
= fun f g x y ->
|
||||
{ x with itv = f x.itv y.itv; arrayblk = g x.arrayblk y.arrayblk }
|
||||
|
||||
let prune_zero : t -> t
|
||||
= lift_prune1 Itv.prune_zero
|
||||
|
||||
let prune_comp : Binop.t -> t -> t -> t
|
||||
= fun c -> lift_prune2 (Itv.prune_comp c) (ArrayBlk.prune_comp c)
|
||||
|
||||
let prune_eq : t -> t -> t
|
||||
= lift_prune2 Itv.prune_eq ArrayBlk.prune_eq
|
||||
|
||||
let prune_ne : t -> t -> t
|
||||
= lift_prune2 Itv.prune_ne ArrayBlk.prune_eq
|
||||
|
||||
let plus_pi : t -> t -> t
|
||||
= fun x y ->
|
||||
{ bot with arrayblk = ArrayBlk.plus_offset x.arrayblk y.itv }
|
||||
|
||||
let minus_pi : t -> t -> t
|
||||
= fun x y ->
|
||||
{ bot with arrayblk = ArrayBlk.minus_offset x.arrayblk y.itv }
|
||||
|
||||
let minus_pp : t -> t -> t
|
||||
= fun x y ->
|
||||
{ bot with itv = ArrayBlk.diff x.arrayblk y.arrayblk }
|
||||
|
||||
let subst : t -> Itv.Bound.t Itv.SubstMap.t -> t
|
||||
= fun x subst_map ->
|
||||
{ x with itv = Itv.subst x.itv subst_map;
|
||||
arrayblk = ArrayBlk.subst x.arrayblk subst_map }
|
||||
|
||||
let get_symbols : t -> Itv.Symbol.t list
|
||||
= fun x ->
|
||||
IList.append (Itv.get_symbols x.itv) (ArrayBlk.get_symbols x.arrayblk)
|
||||
|
||||
let normalize : t -> t
|
||||
= fun x ->
|
||||
{ x with itv = Itv.normalize x.itv; arrayblk = ArrayBlk.normalize x.arrayblk }
|
||||
|
||||
let pp_summary : F.formatter -> t -> unit
|
||||
= fun fmt x -> F.fprintf fmt "(%a, %a)" Itv.pp x.itv ArrayBlk.pp x.arrayblk
|
||||
end
|
||||
|
||||
module Stack =
|
||||
struct
|
||||
module PPMap =
|
||||
struct
|
||||
module Ord = struct include Loc let pp_key = pp end
|
||||
include PrettyPrintable.MakePPMap (Ord)
|
||||
|
||||
let pp_collection
|
||||
: pp_item:(F.formatter -> 'a -> unit) -> F.formatter -> 'a list -> unit
|
||||
= fun ~pp_item fmt c ->
|
||||
let pp_sep fmt () = F.fprintf fmt ",@," in
|
||||
F.pp_print_list ~pp_sep pp_item fmt c
|
||||
|
||||
let pp
|
||||
: pp_value:(F.formatter -> 'a -> unit) -> F.formatter -> 'a t -> unit
|
||||
= fun ~pp_value fmt m ->
|
||||
let pp_item fmt (k, v) =
|
||||
F.fprintf fmt "%a -> %a" Ord.pp_key k pp_value v
|
||||
in
|
||||
F.fprintf fmt "@[<v 2>{ ";
|
||||
pp_collection ~pp_item fmt (bindings m);
|
||||
F.fprintf fmt " }@]"
|
||||
end
|
||||
|
||||
include AbstractDomain.Map (PPMap) (Val)
|
||||
|
||||
let bot = empty
|
||||
|
||||
let find : Loc.t -> astate -> Val.t
|
||||
= fun l m ->
|
||||
try find l m with
|
||||
| Not_found -> Val.bot
|
||||
|
||||
let find_set : PowLoc.t -> astate -> Val.t
|
||||
= fun locs mem ->
|
||||
let find_join loc acc = Val.join acc (find loc mem) in
|
||||
PowLoc.fold find_join locs Val.bot
|
||||
|
||||
let strong_update : PowLoc.t -> Val.astate -> astate -> astate
|
||||
= fun locs v mem ->
|
||||
PowLoc.fold (fun x -> add x v) locs mem
|
||||
|
||||
let weak_update : PowLoc.t -> Val.astate -> astate -> astate
|
||||
= fun locs v mem ->
|
||||
PowLoc.fold (fun x -> add x (Val.join v (find x mem))) locs mem
|
||||
|
||||
let pp_summary : F.formatter -> astate -> unit
|
||||
= fun fmt mem ->
|
||||
let pp_not_logical_var k v =
|
||||
if Loc.is_logical_var k then () else
|
||||
F.fprintf fmt "%a -> %a@," Loc.pp k Val.pp_summary v
|
||||
in
|
||||
iter pp_not_logical_var mem
|
||||
end
|
||||
|
||||
module Heap =
|
||||
struct
|
||||
module PPMap =
|
||||
struct
|
||||
module Ord = struct include Loc let pp_key = pp end
|
||||
include PrettyPrintable.MakePPMap (Ord)
|
||||
|
||||
let pp_collection
|
||||
: pp_item:(F.formatter -> 'a -> unit) -> F.formatter -> 'a list -> unit
|
||||
= fun ~pp_item fmt c ->
|
||||
let pp_sep fmt () = F.fprintf fmt ",@," in
|
||||
F.pp_print_list ~pp_sep pp_item fmt c
|
||||
|
||||
let pp : pp_value:(F.formatter -> 'a -> unit) -> F.formatter -> 'a t -> unit
|
||||
= fun ~pp_value fmt m ->
|
||||
let pp_item fmt (k, v) =
|
||||
F.fprintf fmt "%a -> %a" Ord.pp_key k pp_value v
|
||||
in
|
||||
F.fprintf fmt "@[<v 2>{ ";
|
||||
pp_collection ~pp_item fmt (bindings m);
|
||||
F.fprintf fmt " }@]"
|
||||
end
|
||||
|
||||
include AbstractDomain.Map (PPMap) (Val)
|
||||
|
||||
let bot = empty
|
||||
|
||||
let find : Loc.t -> astate -> Val.t
|
||||
= fun l m ->
|
||||
try find l m with
|
||||
| Not_found -> Val.bot
|
||||
|
||||
let find_set : PowLoc.t -> astate -> Val.t
|
||||
= fun locs mem ->
|
||||
let find_join loc acc = Val.join acc (find loc mem) in
|
||||
PowLoc.fold find_join locs Val.bot
|
||||
|
||||
let strong_update : PowLoc.t -> Val.t -> astate -> astate
|
||||
= fun locs v mem ->
|
||||
PowLoc.fold (fun x -> add x v) locs mem
|
||||
|
||||
let weak_update : PowLoc.t -> Val.t -> astate -> astate
|
||||
= fun locs v mem ->
|
||||
PowLoc.fold (fun x -> add x (Val.join v (find x mem))) locs mem
|
||||
|
||||
let pp_summary : F.formatter -> astate -> unit
|
||||
= fun fmt mem ->
|
||||
let pp_map fmt (k, v) = F.fprintf fmt "%a -> %a" Loc.pp k Val.pp_summary v in
|
||||
F.fprintf fmt "@[<v 2>{ ";
|
||||
F.pp_print_list pp_map fmt (bindings mem);
|
||||
F.fprintf fmt " }@]"
|
||||
|
||||
let get_symbols : astate -> Itv.Symbol.t list
|
||||
= fun mem ->
|
||||
IList.flatten (IList.map (fun (_, v) -> Val.get_symbols v) (bindings mem))
|
||||
|
||||
let get_return : astate -> Val.t
|
||||
= fun mem ->
|
||||
let mem = filter (fun l _ -> Loc.is_return l) mem in
|
||||
if is_empty mem then Val.bot else snd (choose mem)
|
||||
end
|
||||
|
||||
module Alias =
|
||||
struct
|
||||
module M = Caml.Map.Make (Ident)
|
||||
|
||||
type t = Pvar.t M.t
|
||||
|
||||
type astate = t
|
||||
|
||||
let bot : t
|
||||
= M.empty
|
||||
|
||||
let (<=) : lhs:t -> rhs:t -> bool
|
||||
= fun ~lhs ~rhs ->
|
||||
let is_in_rhs k v =
|
||||
match M.find k rhs with
|
||||
| v' -> Pvar.equal v v'
|
||||
| exception Not_found -> false
|
||||
in
|
||||
M.for_all is_in_rhs lhs
|
||||
|
||||
let join : t -> t -> t
|
||||
= fun x y ->
|
||||
let join_v _ v1_opt v2_opt =
|
||||
match v1_opt, v2_opt with
|
||||
| None, None -> None
|
||||
| Some v, None
|
||||
| None, Some v -> Some v
|
||||
| Some v1, Some v2 -> if Pvar.equal v1 v2 then Some v1 else assert false
|
||||
in
|
||||
M.merge join_v x y
|
||||
|
||||
let widen : prev:t -> next:t -> num_iters:int -> t
|
||||
= fun ~prev ~next ~num_iters:_ -> join prev next
|
||||
|
||||
let pp : F.formatter -> t -> unit
|
||||
= fun fmt x ->
|
||||
let pp_sep fmt () = F.fprintf fmt ", @," in
|
||||
let pp1 fmt (k, v) =
|
||||
F.fprintf fmt "%a=%a" (Ident.pp Pp.text) k (Pvar.pp Pp.text) v
|
||||
in
|
||||
(* F.fprintf fmt "@[<v 0>Logical Variables :@,"; *)
|
||||
F.fprintf fmt "@[<hov 2>{ @,";
|
||||
F.pp_print_list ~pp_sep pp1 fmt (M.bindings x);
|
||||
F.fprintf fmt " }@]";
|
||||
F.fprintf fmt "@]"
|
||||
|
||||
let load : Ident.t -> Exp.t -> t -> t
|
||||
= fun id exp m ->
|
||||
match exp with
|
||||
| Exp.Lvar x -> M.add id x m
|
||||
| _ -> m
|
||||
|
||||
let store : Exp.t -> Exp.t -> t -> t
|
||||
= fun e _ m ->
|
||||
match e with
|
||||
| Exp.Lvar x -> M.filter (fun _ y -> not (Pvar.equal x y)) m
|
||||
| _ -> m
|
||||
|
||||
let find : Ident.t -> t -> Pvar.t option
|
||||
= fun k m -> try Some (M.find k m) with Not_found -> None
|
||||
end
|
||||
|
||||
module Mem =
|
||||
struct
|
||||
type astate = { stack : Stack.astate; heap : Heap.astate; alias : Alias.astate }
|
||||
type t = astate
|
||||
|
||||
let bot : t
|
||||
= { stack = Stack.bot; heap = Heap.bot; alias = Alias.bot }
|
||||
|
||||
let (<=) ~lhs ~rhs =
|
||||
if phys_equal lhs rhs then true
|
||||
else
|
||||
Stack.(<=) ~lhs:(lhs.stack) ~rhs:(rhs.stack)
|
||||
&& Heap.(<=) ~lhs:(lhs.heap) ~rhs:(rhs.heap)
|
||||
&& Alias.(<=) ~lhs:(lhs.alias) ~rhs:(rhs.alias)
|
||||
|
||||
let widen ~prev ~next ~num_iters =
|
||||
if phys_equal prev next then prev
|
||||
else
|
||||
{ stack = Stack.widen ~prev:(prev.stack) ~next:(next.stack) ~num_iters;
|
||||
heap = Heap.widen ~prev:(prev.heap) ~next:(next.heap) ~num_iters;
|
||||
alias = Alias.widen ~prev:(prev.alias) ~next:(next.alias) ~num_iters; }
|
||||
|
||||
let join : t -> t -> t
|
||||
= fun x y ->
|
||||
{ stack = Stack.join x.stack y.stack;
|
||||
heap = Heap.join x.heap y.heap;
|
||||
alias = Alias.join x.alias y.alias }
|
||||
|
||||
let pp : F.formatter -> t -> unit
|
||||
= fun fmt x ->
|
||||
F.fprintf fmt "Stack :@,";
|
||||
F.fprintf fmt "%a@," Stack.pp x.stack;
|
||||
F.fprintf fmt "Heap :@,";
|
||||
F.fprintf fmt "%a" Heap.pp x.heap
|
||||
|
||||
let pp_summary : F.formatter -> t -> unit
|
||||
= fun fmt x ->
|
||||
F.fprintf fmt "@[<v 0>Parameters :@,";
|
||||
F.fprintf fmt "%a" Heap.pp_summary x.heap ;
|
||||
F.fprintf fmt "@]"
|
||||
|
||||
let find_stack : Loc.t -> t -> Val.t
|
||||
= fun k m -> Stack.find k m.stack
|
||||
|
||||
let find_stack_set : PowLoc.t -> t -> Val.t
|
||||
= fun k m -> Stack.find_set k m.stack
|
||||
|
||||
let find_heap : Loc.t -> t -> Val.t
|
||||
= fun k m -> Heap.find k m.heap
|
||||
|
||||
let find_heap_set : PowLoc.t -> t -> Val.t
|
||||
= fun k m -> Heap.find_set k m.heap
|
||||
|
||||
let find_alias : Ident.t -> t -> Pvar.t option
|
||||
= fun k m -> Alias.find k m.alias
|
||||
|
||||
let load_alias : Ident.t -> Exp.t -> t -> t
|
||||
= fun id e m -> { m with alias = Alias.load id e m.alias }
|
||||
|
||||
let store_alias : Exp.t -> Exp.t -> t -> t
|
||||
= fun e1 e2 m -> { m with alias = Alias.store e1 e2 m.alias }
|
||||
|
||||
let add_stack : Loc.t -> Val.t -> t -> t
|
||||
= fun k v m -> { m with stack = Stack.add k v m.stack }
|
||||
|
||||
let add_heap : Loc.t -> Val.t -> t -> t
|
||||
= fun k v m -> { m with heap = Heap.add k v m.heap }
|
||||
|
||||
let strong_update_stack : PowLoc.t -> Val.t -> t -> t
|
||||
= fun p v m -> { m with stack = Stack.strong_update p v m.stack }
|
||||
|
||||
let strong_update_heap : PowLoc.t -> Val.t -> t -> t
|
||||
= fun p v m -> { m with heap = Heap.strong_update p v m.heap }
|
||||
|
||||
let weak_update_stack : PowLoc.t -> Val.t -> t -> t
|
||||
= fun p v m -> { m with stack = Stack.weak_update p v m.stack }
|
||||
|
||||
let weak_update_heap : PowLoc.t -> Val.t -> t -> t
|
||||
= fun p v m -> { m with heap = Heap.weak_update p v m.heap }
|
||||
|
||||
let get_heap_symbols : t -> Itv.Symbol.t list
|
||||
= fun m -> Heap.get_symbols m.heap
|
||||
|
||||
let get_return : t -> Val.t
|
||||
= fun m -> Heap.get_return m.heap
|
||||
|
||||
let can_strong_update : PowLoc.t -> bool
|
||||
= fun ploc ->
|
||||
if Int.equal (PowLoc.cardinal ploc) 1 then Loc.is_var (PowLoc.choose ploc) else false
|
||||
|
||||
let update_mem : PowLoc.t -> Val.t -> t -> t
|
||||
= fun ploc v s ->
|
||||
if can_strong_update ploc
|
||||
then strong_update_heap ploc v s
|
||||
else weak_update_heap ploc v s
|
||||
end
|
||||
|
||||
module Summary =
|
||||
struct
|
||||
type t = Mem.t * Mem.t * ConditionSet.t
|
||||
|
||||
let get_input : t -> Mem.t
|
||||
= fst3
|
||||
|
||||
let get_output : t -> Mem.t
|
||||
= snd3
|
||||
|
||||
let get_cond_set : t -> ConditionSet.t
|
||||
= trd3
|
||||
|
||||
let get_symbols : t -> Itv.Symbol.t list
|
||||
= fun s -> Mem.get_heap_symbols (get_input s)
|
||||
|
||||
let get_return : t -> Val.t
|
||||
= fun s -> Mem.get_return (get_output s)
|
||||
|
||||
let pp_symbols : F.formatter -> t -> unit
|
||||
= fun fmt s ->
|
||||
let pp_sep fmt () = F.fprintf fmt ", @," in
|
||||
F.fprintf fmt "@[<hov 2>Symbols: {";
|
||||
F.pp_print_list ~pp_sep Itv.Symbol.pp fmt (get_symbols s);
|
||||
F.fprintf fmt "}@]"
|
||||
|
||||
let pp_symbol_map : F.formatter -> t -> unit
|
||||
= fun fmt s -> Mem.pp_summary fmt (get_input s)
|
||||
|
||||
let pp_return : F.formatter -> t -> unit
|
||||
= fun fmt s -> F.fprintf fmt "Return value: %a" Val.pp_summary (get_return s)
|
||||
|
||||
let pp_summary : F.formatter -> t -> unit
|
||||
= fun fmt s ->
|
||||
F.fprintf fmt "%a@,%a@,%a" pp_symbol_map s pp_return s
|
||||
ConditionSet.pp_summary (get_cond_set s)
|
||||
|
||||
let pp : F.formatter -> t -> unit
|
||||
= fun fmt (entry_mem, exit_mem, condition_set) ->
|
||||
F.fprintf fmt "%a@,%a@,%a@"
|
||||
Mem.pp entry_mem Mem.pp exit_mem ConditionSet.pp condition_set
|
||||
end
|
||||
@ -0,0 +1,351 @@
|
||||
(*
|
||||
* Copyright (c) 2016 - present
|
||||
*
|
||||
* Programming Research Laboratory (ROPAS)
|
||||
* Seoul National University, Korea
|
||||
* All rights reserved.
|
||||
*
|
||||
* This source code is licensed under the BSD style license found in the
|
||||
* LICENSE file in the root directory of this source tree. An additional grant
|
||||
* of patent rights can be found in the PATENTS file in the same directory.
|
||||
*)
|
||||
|
||||
open! IStd
|
||||
open Core_kernel.Fn
|
||||
open AbsLoc
|
||||
|
||||
module F = Format
|
||||
module L = Logging
|
||||
module Domain = BufferOverrunDomain
|
||||
open Domain
|
||||
|
||||
module Make (CFG : ProcCfg.S) =
|
||||
struct
|
||||
exception Not_implemented
|
||||
|
||||
let eval_const : Const.t -> Val.t
|
||||
= function
|
||||
| Const.Cint intlit -> Val.of_int (IntLit.to_int intlit)
|
||||
| Const.Cfloat f -> f |> int_of_float |> Val.of_int
|
||||
| _ -> Val.bot (* TODO *)
|
||||
|
||||
let sizeof_ikind : Typ.ikind -> int
|
||||
= function
|
||||
| Typ.IChar | Typ.ISChar | Typ.IUChar | Typ.IBool -> 1
|
||||
| Typ.IInt | Typ.IUInt -> 4
|
||||
| Typ.IShort | Typ.IUShort -> 2
|
||||
| Typ.ILong | Typ.IULong -> 4
|
||||
| Typ.ILongLong | Typ.IULongLong -> 8
|
||||
| Typ.I128 | Typ.IU128 -> 16
|
||||
|
||||
let sizeof_fkind : Typ.fkind -> int
|
||||
= function
|
||||
| Typ.FFloat -> 4
|
||||
| Typ.FDouble | Typ.FLongDouble -> 8
|
||||
|
||||
(* NOTE: assume 32bit machine *)
|
||||
let rec sizeof : Typ.t -> int
|
||||
= function
|
||||
| Typ.Tint ikind -> sizeof_ikind ikind
|
||||
| Typ.Tfloat fkind -> sizeof_fkind fkind
|
||||
| Typ.Tvoid -> 1
|
||||
| Typ.Tptr (_, _) -> 4
|
||||
| Typ.Tstruct _ -> 4 (* TODO *)
|
||||
| Typ.Tarray (typ, Some ilit) -> sizeof typ * IntLit.to_int ilit
|
||||
| _ -> 4
|
||||
|
||||
let rec eval : Exp.t -> Mem.astate -> Location.t -> Val.t
|
||||
= fun exp mem loc ->
|
||||
match exp with
|
||||
| Exp.Var id -> Mem.find_stack (Var.of_id id |> Loc.of_var) mem
|
||||
| Exp.Lvar pvar ->
|
||||
let ploc = pvar |> Loc.of_pvar |> PowLoc.singleton in
|
||||
let arr = Mem.find_stack_set ploc mem in
|
||||
ploc |> Val.of_pow_loc |> Val.join arr
|
||||
| Exp.UnOp (uop, e, _) -> eval_unop uop e mem loc
|
||||
| Exp.BinOp (bop, e1, e2) -> eval_binop bop e1 e2 mem loc
|
||||
| Exp.Const c -> eval_const c
|
||||
| Exp.Cast (_, e) -> eval e mem loc
|
||||
| Exp.Lfield (e, fn, _) ->
|
||||
eval e mem loc
|
||||
|> Val.get_all_locs
|
||||
|> flip PowLoc.append_field fn
|
||||
|> Val.of_pow_loc
|
||||
| Exp.Lindex (e1, _) ->
|
||||
let arr = eval e1 mem loc in (* must have array blk *)
|
||||
(* let idx = eval e2 mem loc in *)
|
||||
let ploc = arr |> Val.get_array_blk |> ArrayBlk.get_pow_loc in
|
||||
(* if nested array, add the array blk *)
|
||||
let arr = Mem.find_heap_set ploc mem in
|
||||
Val.join (Val.of_pow_loc ploc) arr
|
||||
| Exp.Sizeof (typ, _, _) -> Val.of_int (sizeof typ)
|
||||
| Exp.Exn _
|
||||
| Exp.Closure _ -> Val.bot
|
||||
|
||||
and eval_unop : Unop.t -> Exp.t -> Mem.astate -> Location.t -> Val.t
|
||||
= fun unop e mem loc ->
|
||||
let v = eval e mem loc in
|
||||
match unop with
|
||||
| Unop.Neg -> Val.neg v
|
||||
| Unop.BNot -> Val.unknown_bit v
|
||||
| Unop.LNot -> Val.lnot v
|
||||
|
||||
and eval_binop
|
||||
: Binop.t -> Exp.t -> Exp.t -> Mem.astate -> Location.t -> Val.t
|
||||
= fun binop e1 e2 mem loc ->
|
||||
let v1 = eval e1 mem loc in
|
||||
let v2 = eval e2 mem loc in
|
||||
match binop with
|
||||
| Binop.PlusA ->
|
||||
Val.join (Val.plus v1 v2) (Val.plus_pi v1 v2)
|
||||
| Binop.PlusPI -> Val.plus_pi v1 v2
|
||||
| Binop.MinusA ->
|
||||
Val.joins
|
||||
[ Val.minus v1 v2
|
||||
; Val.minus_pi v1 v2
|
||||
; Val.minus_pp v1 v2 ]
|
||||
| Binop.MinusPI -> Val.minus_pi v1 v2
|
||||
| Binop.MinusPP -> Val.minus_pp v1 v2
|
||||
| Binop.Mult -> Val.mult v1 v2
|
||||
| Binop.Div -> Val.div v1 v2
|
||||
| Binop.Mod -> Val.mod_sem v1 v2
|
||||
| Binop.Shiftlt -> Val.shiftlt v1 v2
|
||||
| Binop.Shiftrt -> Val.shiftrt v1 v2
|
||||
| Binop.Lt -> Val.lt_sem v1 v2
|
||||
| Binop.Gt -> Val.gt_sem v1 v2
|
||||
| Binop.Le -> Val.le_sem v1 v2
|
||||
| Binop.Ge -> Val.ge_sem v1 v2
|
||||
| Binop.Eq -> Val.eq_sem v1 v2
|
||||
| Binop.Ne -> Val.ne_sem v1 v2
|
||||
| Binop.BAnd
|
||||
| Binop.BXor
|
||||
| Binop.BOr -> Val.unknown_bit v1
|
||||
| Binop.LAnd -> Val.land_sem v1 v2
|
||||
| Binop.LOr -> Val.lor_sem v1 v2
|
||||
| Binop.PtrFld -> raise Not_implemented
|
||||
|
||||
let get_allocsite : Procname.t -> CFG.node -> int -> int -> string
|
||||
= fun proc_name node inst_num dimension ->
|
||||
let proc_name = Procname.to_string proc_name in
|
||||
let node_num = CFG.hash node |> string_of_int in
|
||||
let inst_num = string_of_int inst_num in
|
||||
let dimension = string_of_int dimension in
|
||||
(proc_name ^ "-" ^ node_num ^ "-" ^ inst_num ^ "-" ^ dimension)
|
||||
|> Allocsite.make
|
||||
|
||||
let eval_array_alloc
|
||||
: Procname.t -> CFG.node -> Typ.t -> Itv.t -> Itv.t -> int -> int -> Val.t
|
||||
= fun pdesc node typ offset size inst_num dimension ->
|
||||
let allocsite = get_allocsite pdesc node inst_num dimension in
|
||||
let stride = sizeof typ |> Itv.of_int in
|
||||
ArrayBlk.make allocsite offset size stride
|
||||
|> Val.of_array_blk
|
||||
|
||||
let prune_unop : Exp.t -> Mem.astate -> Mem.astate
|
||||
= fun e mem ->
|
||||
match e with
|
||||
| Exp.Var x ->
|
||||
(match Mem.find_alias x mem with
|
||||
| Some x' ->
|
||||
let lv = Loc.of_pvar x' in
|
||||
let v = Mem.find_heap lv mem in
|
||||
let v' = Val.prune_zero v in
|
||||
Mem.update_mem (PowLoc.singleton lv) v' mem
|
||||
| None -> mem)
|
||||
| Exp.UnOp (Unop.LNot, Exp.Var x, _) ->
|
||||
(match Mem.find_alias x mem with
|
||||
| Some x' ->
|
||||
let lv = Loc.of_pvar x' in
|
||||
let v = Mem.find_heap lv mem in
|
||||
let itv_v =
|
||||
if Itv.is_bot (Val.get_itv v) then Itv.bot else
|
||||
Val.get_itv Val.zero
|
||||
in
|
||||
let v' = Val.modify_itv itv_v v in
|
||||
Mem.update_mem (PowLoc.singleton lv) v' mem
|
||||
| None -> mem)
|
||||
| _ -> mem
|
||||
|
||||
let prune_binop_left : Exp.t -> Location.t -> Mem.astate -> Mem.astate
|
||||
= fun e loc mem ->
|
||||
match e with
|
||||
| Exp.BinOp (Binop.Lt as comp, Exp.Var x, e')
|
||||
| Exp.BinOp (Binop.Gt as comp, Exp.Var x, e')
|
||||
| Exp.BinOp (Binop.Le as comp, Exp.Var x, e')
|
||||
| Exp.BinOp (Binop.Ge as comp, Exp.Var x, e') ->
|
||||
(match Mem.find_alias x mem with
|
||||
| Some x' ->
|
||||
let lv = Loc.of_pvar x' in
|
||||
let v = Mem.find_heap lv mem in
|
||||
let v' = Val.prune_comp comp v (eval e' mem loc) in
|
||||
Mem.update_mem (PowLoc.singleton lv) v' mem
|
||||
| None -> mem)
|
||||
| Exp.BinOp (Binop.Eq, Exp.Var x, e') ->
|
||||
(match Mem.find_alias x mem with
|
||||
| Some x' ->
|
||||
let lv = Loc.of_pvar x' in
|
||||
let v = Mem.find_heap lv mem in
|
||||
let v' = Val.prune_eq v (eval e' mem loc) in
|
||||
Mem.update_mem (PowLoc.singleton lv) v' mem
|
||||
| None -> mem)
|
||||
| Exp.BinOp (Binop.Ne, Exp.Var x, e') ->
|
||||
(match Mem.find_alias x mem with
|
||||
| Some x' ->
|
||||
let lv = Loc.of_pvar x' in
|
||||
let v = Mem.find_heap lv mem in
|
||||
let v' = Val.prune_ne v (eval e' mem loc) in
|
||||
Mem.update_mem (PowLoc.singleton lv) v' mem
|
||||
| None -> mem)
|
||||
| _ -> mem
|
||||
|
||||
let comp_rev : Binop.t -> Binop.t
|
||||
= function
|
||||
| Binop.Lt -> Binop.Gt
|
||||
| Binop.Gt -> Binop.Lt
|
||||
| Binop.Le -> Binop.Ge
|
||||
| Binop.Ge -> Binop.Le
|
||||
| Binop.Eq -> Binop.Eq
|
||||
| Binop.Ne -> Binop.Ne
|
||||
| _ -> assert (false)
|
||||
|
||||
let comp_not : Binop.t -> Binop.t
|
||||
= function
|
||||
| Binop.Lt -> Binop.Ge
|
||||
| Binop.Gt -> Binop.Le
|
||||
| Binop.Le -> Binop.Gt
|
||||
| Binop.Ge -> Binop.Lt
|
||||
| Binop.Eq -> Binop.Ne
|
||||
| Binop.Ne -> Binop.Eq
|
||||
| _ -> assert (false)
|
||||
|
||||
let prune_binop_right : Exp.t -> Location.t -> Mem.astate -> Mem.astate
|
||||
= fun e loc mem ->
|
||||
match e with
|
||||
| Exp.BinOp (Binop.Lt as c, e', Exp.Var x)
|
||||
| Exp.BinOp (Binop.Gt as c, e', Exp.Var x)
|
||||
| Exp.BinOp (Binop.Le as c, e', Exp.Var x)
|
||||
| Exp.BinOp (Binop.Ge as c, e', Exp.Var x)
|
||||
| Exp.BinOp (Binop.Eq as c, e', Exp.Var x)
|
||||
| Exp.BinOp (Binop.Ne as c, e', Exp.Var x) ->
|
||||
prune_binop_left (Exp.BinOp (comp_rev c, Exp.Var x, e')) loc mem
|
||||
| _ -> mem
|
||||
|
||||
let rec prune : Exp.t -> Location.t -> Mem.astate -> Mem.astate
|
||||
= fun e loc mem ->
|
||||
let mem =
|
||||
mem |> prune_unop e |> prune_binop_left e loc |> prune_binop_right e loc
|
||||
in
|
||||
match e with
|
||||
| Exp.BinOp (Binop.Ne, e, Exp.Const (Const.Cint i)) when IntLit.iszero i ->
|
||||
prune e loc mem
|
||||
| Exp.BinOp (Binop.Eq, e, Exp.Const (Const.Cint i)) when IntLit.iszero i ->
|
||||
prune (Exp.UnOp (Unop.LNot, e, None)) loc mem
|
||||
| Exp.UnOp (Unop.Neg, Exp.Var x, _) -> prune (Exp.Var x) loc mem
|
||||
| Exp.BinOp (Binop.LAnd, e1, e2) ->
|
||||
mem |> prune e1 loc |> prune e2 loc
|
||||
| Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LOr, e1, e2), t) ->
|
||||
mem
|
||||
|> prune (Exp.UnOp (Unop.LNot, e1, t)) loc
|
||||
|> prune (Exp.UnOp (Unop.LNot, e2, t)) loc
|
||||
| Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Lt as c, e1, e2), _)
|
||||
| Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Gt as c, e1, e2), _)
|
||||
| Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Le as c, e1, e2), _)
|
||||
| Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Ge as c, e1, e2), _)
|
||||
| Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Eq as c, e1, e2), _)
|
||||
| Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Ne as c, e1, e2), _) ->
|
||||
prune (Exp.BinOp (comp_not c, e1, e2)) loc mem
|
||||
| _ -> mem
|
||||
|
||||
let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list
|
||||
= fun pdesc ->
|
||||
let proc_name = Procdesc.get_proc_name pdesc in
|
||||
Procdesc.get_formals pdesc
|
||||
|> IList.map (fun (name, typ) -> (Pvar.mk name proc_name, typ))
|
||||
|
||||
let get_matching_pairs
|
||||
: Tenv.t -> Val.t -> Val.t -> Typ.t -> Mem.astate -> Mem.astate
|
||||
-> (Itv.Bound.t * Itv.Bound.t) list
|
||||
= fun tenv formal actual typ caller_mem callee_mem ->
|
||||
let get_itv v = Val.get_itv v in
|
||||
let get_offset v = v |> Val.get_array_blk |> ArrayBlk.offsetof in
|
||||
let get_size v = v |> Val.get_array_blk |> ArrayBlk.sizeof in
|
||||
let get_field_name (fn, _, _) = fn in
|
||||
let deref_field v fn mem =
|
||||
Mem.find_heap_set (PowLoc.append_field (Val.get_all_locs v) fn) mem
|
||||
in
|
||||
let deref_ptr v mem = Mem.find_heap_set (Val.get_all_locs v) mem in
|
||||
let add_pair_itv itv1 itv2 l =
|
||||
let open Itv in
|
||||
if itv1 <> bot && itv2 <> bot then
|
||||
(lb itv1, lb itv2) :: (ub itv1, ub itv2) :: l
|
||||
else if itv1 <> bot && Itv.eq itv2 bot then
|
||||
(lb itv1, Bound.Bot) :: (ub itv1, Bound.Bot) :: l
|
||||
else
|
||||
l
|
||||
in
|
||||
let add_pair_val v1 v2 pairs =
|
||||
pairs
|
||||
|> add_pair_itv (get_itv v1) (get_itv v2)
|
||||
|> add_pair_itv (get_offset v1) (get_offset v2)
|
||||
|> add_pair_itv (get_size v1) (get_size v2)
|
||||
in
|
||||
let add_pair_field v1 v2 pairs fn =
|
||||
let v1' = deref_field v1 fn callee_mem in
|
||||
let v2' = deref_field v2 fn caller_mem in
|
||||
add_pair_val v1' v2' pairs
|
||||
in
|
||||
let add_pair_ptr typ v1 v2 pairs =
|
||||
match typ with
|
||||
| Typ.Tptr (Typ.Tstruct typename, _) ->
|
||||
(match Tenv.lookup tenv typename with
|
||||
| Some str ->
|
||||
let fns = IList.map get_field_name str.StructTyp.fields in
|
||||
IList.fold_left (add_pair_field v1 v2) pairs fns
|
||||
| _ -> pairs)
|
||||
| Typ.Tptr (_ ,_) ->
|
||||
let v1' = deref_ptr v1 callee_mem in
|
||||
let v2' = deref_ptr v2 caller_mem in
|
||||
add_pair_val v1' v2' pairs
|
||||
| _ -> pairs
|
||||
in
|
||||
[] |> add_pair_val formal actual |> add_pair_ptr typ formal actual
|
||||
|
||||
let subst_map_of_pairs
|
||||
: (Itv.Bound.t * Itv.Bound.t) list -> Itv.Bound.t Itv.SubstMap.t
|
||||
= fun pairs ->
|
||||
let add_pair map (formal, actual) =
|
||||
match formal with
|
||||
| Itv.Bound.Linear (0, se1) when Itv.SymLinear.cardinal se1 > 0 ->
|
||||
let (symbol, coeff) = Itv.SymLinear.choose se1 in
|
||||
if Int.equal coeff 1
|
||||
then Itv.SubstMap.add symbol actual map
|
||||
else assert false
|
||||
| _ -> assert false
|
||||
in
|
||||
IList.fold_left add_pair Itv.SubstMap.empty pairs
|
||||
|
||||
let rec list_fold2_def
|
||||
: Val.t -> ('a -> Val.t -> 'b -> 'b) -> 'a list -> Val.t list -> 'b -> 'b
|
||||
= fun default f xs ys acc ->
|
||||
match xs, ys with
|
||||
| [x], _ -> f x (IList.fold_left Val.join Val.bot ys) acc
|
||||
| [], _ -> acc
|
||||
| x :: xs', [] -> list_fold2_def default f xs' ys (f x default acc)
|
||||
| x :: xs', y :: ys' -> list_fold2_def default f xs' ys' (f x y acc)
|
||||
|
||||
let get_subst_map
|
||||
: Tenv.t -> Procdesc.t -> (Exp.t * 'a) list -> Mem.astate -> Mem.astate
|
||||
-> Location.t -> Itv.Bound.t Itv.SubstMap.t
|
||||
= fun tenv callee_pdesc params caller_mem callee_entry_mem loc ->
|
||||
let add_pair (formal, typ) actual l =
|
||||
let formal = Mem.find_heap (Loc.of_pvar formal) callee_entry_mem in
|
||||
let new_matching =
|
||||
get_matching_pairs tenv formal actual typ caller_mem callee_entry_mem
|
||||
in
|
||||
IList.append new_matching l
|
||||
in
|
||||
let formals = get_formals callee_pdesc in
|
||||
let actuals = IList.map (fun (a, _) -> eval a caller_mem loc) params in
|
||||
list_fold2_def Val.bot add_pair formals actuals []
|
||||
|> subst_map_of_pairs
|
||||
end
|
||||
File diff suppressed because it is too large
Load Diff
@ -0,0 +1,30 @@
|
||||
# Copyright (c) 2016 - present
|
||||
#
|
||||
# Programming Research Laboratory (ROPAS)
|
||||
# Seoul National University, Korea
|
||||
# All rights reserved.
|
||||
#
|
||||
# This source code is licensed under the BSD style license found in the
|
||||
# LICENSE file in the root directory of this source tree. An additional grant
|
||||
# of patent rights can be found in the PATENTS file in the same directory.
|
||||
|
||||
TESTS_DIR = ../../..
|
||||
|
||||
ANALYZER = bufferoverrun
|
||||
CLANG_OPTIONS = -c
|
||||
INFER_OPTIONS = -nf --project-root $(TESTS_DIR)
|
||||
INFERPRINT_OPTIONS = --issues-tests
|
||||
|
||||
SOURCES = \
|
||||
trivial.c \
|
||||
function_call.c \
|
||||
for_loop.c \
|
||||
while_loop.c \
|
||||
do_while.c \
|
||||
nested_loop.c \
|
||||
nested_loop_with_label.c \
|
||||
break_continue_return.c \
|
||||
goto_loop.c \
|
||||
inf_loop.c
|
||||
|
||||
include $(TESTS_DIR)/clang.make
|
||||
@ -0,0 +1,33 @@
|
||||
/*
|
||||
* Copyright (c) 2016 - present
|
||||
*
|
||||
* Programming Research Laboratory (ROPAS)
|
||||
* Seoul National University, Korea
|
||||
* All rights reserved.
|
||||
*
|
||||
* This source code is licensed under the BSD style license found in the
|
||||
* LICENSE file in the root directory of this source tree. An additional grant
|
||||
* of patent rights can be found in the PATENTS file in the same directory.
|
||||
*/
|
||||
|
||||
int break_continue_return() {
|
||||
int i = 0;
|
||||
char a[10];
|
||||
|
||||
while (1) {
|
||||
i++;
|
||||
if (i >= 10)
|
||||
break;
|
||||
if (i < 2)
|
||||
continue;
|
||||
a[i] = 'a'; /* SAFE */
|
||||
}
|
||||
i = 0;
|
||||
while (1) {
|
||||
if (i > 10)
|
||||
return 0;
|
||||
a[i] = 'a'; /* BUG */
|
||||
i++;
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
@ -0,0 +1,27 @@
|
||||
/*
|
||||
* Copyright (c) 2016 - present
|
||||
*
|
||||
* Programming Research Laboratory (ROPAS)
|
||||
* Seoul National University, Korea
|
||||
* All rights reserved.
|
||||
*
|
||||
* This source code is licensed under the BSD style license found in the
|
||||
* LICENSE file in the root directory of this source tree. An additional grant
|
||||
* of patent rights can be found in the PATENTS file in the same directory.
|
||||
*/
|
||||
|
||||
#include <stdlib.h>
|
||||
|
||||
void do_while_sub(char* a, int len) {
|
||||
int i = 0;
|
||||
do {
|
||||
a[i] = i;
|
||||
i++;
|
||||
} while (i < len);
|
||||
}
|
||||
|
||||
void do_while() {
|
||||
char* a = malloc(10);
|
||||
do_while_sub(a, 10); /* SAFE */
|
||||
do_while_sub(a, 11); /* BUG */
|
||||
}
|
||||
@ -0,0 +1,40 @@
|
||||
/*
|
||||
* Copyright (c) 2016 - present
|
||||
*
|
||||
* Programming Research Laboratory (ROPAS)
|
||||
* Seoul National University, Korea
|
||||
* All rights reserved.
|
||||
*
|
||||
* This source code is licensed under the BSD style license found in the
|
||||
* LICENSE file in the root directory of this source tree. An additional grant
|
||||
* of patent rights can be found in the PATENTS file in the same directory.
|
||||
*/
|
||||
|
||||
#include <stdlib.h>
|
||||
|
||||
char* safealloc(int n) {
|
||||
char* x;
|
||||
if (n > 0)
|
||||
x = malloc(n);
|
||||
else
|
||||
x = malloc(10);
|
||||
|
||||
if (!x)
|
||||
return x;
|
||||
else
|
||||
exit(1);
|
||||
}
|
||||
|
||||
void for_loop() {
|
||||
char* a;
|
||||
int i;
|
||||
|
||||
a = safealloc(10);
|
||||
for (i = 0; i < 10; i++) {
|
||||
a[i] = 'a'; /* SAFE */
|
||||
}
|
||||
a = safealloc(5);
|
||||
for (i = 0; i < 10; i++) {
|
||||
a[i] = 'a'; /* BUG */
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,26 @@
|
||||
/*
|
||||
* Copyright (c) 2016 - present
|
||||
*
|
||||
* Programming Research Laboratory (ROPAS)
|
||||
* Seoul National University, Korea
|
||||
* All rights reserved.
|
||||
*
|
||||
* This source code is licensed under the BSD style license found in the
|
||||
* LICENSE file in the root directory of this source tree. An additional grant
|
||||
* of patent rights can be found in the PATENTS file in the same directory.
|
||||
*/
|
||||
|
||||
#include <stdlib.h>
|
||||
|
||||
void arr_access(int* arr, char* p, int i) {
|
||||
int x = arr[0];
|
||||
arr[x] = 1; /* BUG */
|
||||
*(p + i) = 'a'; /* BUG */
|
||||
}
|
||||
|
||||
void function_call() {
|
||||
int arr[10];
|
||||
arr[0] = 100;
|
||||
char* p = malloc(10);
|
||||
arr_access(arr, p, 20);
|
||||
}
|
||||
@ -0,0 +1,25 @@
|
||||
/*
|
||||
* Copyright (c) 2016 - present
|
||||
*
|
||||
* Programming Research Laboratory (ROPAS)
|
||||
* Seoul National University, Korea
|
||||
* All rights reserved.
|
||||
*
|
||||
* This source code is licensed under the BSD style license found in the
|
||||
* LICENSE file in the root directory of this source tree. An additional grant
|
||||
* of patent rights can be found in the PATENTS file in the same directory.
|
||||
*/
|
||||
|
||||
void goto_loop() {
|
||||
int i = 0;
|
||||
char a[10];
|
||||
|
||||
loop_start:
|
||||
if (i >= 10)
|
||||
goto loop_end;
|
||||
a[i] = 'a'; /* SAFE */
|
||||
i++;
|
||||
goto loop_start;
|
||||
loop_end:
|
||||
a[i] = 'a'; /* BUG */
|
||||
}
|
||||
@ -0,0 +1,23 @@
|
||||
/*
|
||||
* Copyright (c) 2016 - present
|
||||
*
|
||||
* Programming Research Laboratory (ROPAS)
|
||||
* Seoul National University, Korea
|
||||
* All rights reserved.
|
||||
*
|
||||
* This source code is licensed under the BSD style license found in the
|
||||
* LICENSE file in the root directory of this source tree. An additional grant
|
||||
* of patent rights can be found in the PATENTS file in the same directory.
|
||||
*/
|
||||
|
||||
void inf_loop() {
|
||||
int i = 0;
|
||||
char a[10];
|
||||
|
||||
while (1) {
|
||||
if (i >= 10)
|
||||
i = 0;
|
||||
a[i] = 'a'; /* SAFE */
|
||||
i++;
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,11 @@
|
||||
codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16, BUFFER_OVERRUN, [Offset : [0, 10] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/break_continue_return.c:29:5]
|
||||
codetoanalyze/c/bufferoverrun/do_while.c, do_while, 2, BUFFER_OVERRUN, [Offset : [0, +oo] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call do_while_sub() ]
|
||||
codetoanalyze/c/bufferoverrun/do_while.c, do_while, 3, BUFFER_OVERRUN, [Offset : [0, +oo] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call do_while_sub() ]
|
||||
codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN, [Offset : [0, 9] Size : [5, 10] @ codetoanalyze/c/bufferoverrun/for_loop.c:38:5]
|
||||
codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, [Offset : [100, 100] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:17:3 by call arr_access() ]
|
||||
codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, [Offset : [20, 20] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:18:3 by call arr_access() ]
|
||||
codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN, [Offset : [10, +oo] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/goto_loop.c:24:3]
|
||||
codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN, [Offset : [0, 10] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop.c:20:7]
|
||||
codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN, [Offset : [0, +oo] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop_with_label.c:19:5]
|
||||
codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN, [Offset : [10, 10] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/trivial.c:15:3]
|
||||
codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN, [Offset : [0, +oo] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/while_loop.c:18:10]
|
||||
@ -0,0 +1,23 @@
|
||||
/*
|
||||
* Copyright (c) 2016 - present
|
||||
*
|
||||
* Programming Research Laboratory (ROPAS)
|
||||
* Seoul National University, Korea
|
||||
* All rights reserved.
|
||||
*
|
||||
* This source code is licensed under the BSD style license found in the
|
||||
* LICENSE file in the root directory of this source tree. An additional grant
|
||||
* of patent rights can be found in the PATENTS file in the same directory.
|
||||
*/
|
||||
|
||||
void nested_loop() {
|
||||
int i, j;
|
||||
char a[10];
|
||||
|
||||
for (i = 0; i < 10; i++) {
|
||||
a[i] = 'a'; /* SAFE */
|
||||
for (j = 0; j <= 10; j++) {
|
||||
a[j] = 'a'; /* BUG */
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,25 @@
|
||||
/*
|
||||
* Copyright (c) 2016 - present
|
||||
*
|
||||
* Programming Research Laboratory (ROPAS)
|
||||
* Seoul National University, Korea
|
||||
* All rights reserved.
|
||||
*
|
||||
* This source code is licensed under the BSD style license found in the
|
||||
* LICENSE file in the root directory of this source tree. An additional grant
|
||||
* of patent rights can be found in the PATENTS file in the same directory.
|
||||
*/
|
||||
|
||||
void nested_loop_with_label() {
|
||||
int i, j = 0;
|
||||
char a[10];
|
||||
|
||||
for (i = 0; i < 10; i++) {
|
||||
outer_loop:
|
||||
a[j] = 'a'; /* BUG */
|
||||
for (j = 0; j <= 10; j++) {
|
||||
if (j >= 10)
|
||||
goto outer_loop;
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,16 @@
|
||||
/*
|
||||
* Copyright (c) 2016 - present
|
||||
*
|
||||
* Programming Research Laboratory (ROPAS)
|
||||
* Seoul National University, Korea
|
||||
* All rights reserved.
|
||||
*
|
||||
* This source code is licensed under the BSD style license found in the
|
||||
* LICENSE file in the root directory of this source tree. An additional grant
|
||||
* of patent rights can be found in the PATENTS file in the same directory.
|
||||
*/
|
||||
|
||||
void trivial() {
|
||||
int a[10];
|
||||
a[10] = 0; /* BUG */
|
||||
}
|
||||
@ -0,0 +1,20 @@
|
||||
/*
|
||||
* Copyright (c) 2016 - present
|
||||
*
|
||||
* Programming Research Laboratory (ROPAS)
|
||||
* Seoul National University, Korea
|
||||
* All rights reserved.
|
||||
*
|
||||
* This source code is licensed under the BSD style license found in the
|
||||
* LICENSE file in the root directory of this source tree. An additional grant
|
||||
* of patent rights can be found in the PATENTS file in the same directory.
|
||||
*/
|
||||
|
||||
char* safealloc(int n);
|
||||
|
||||
void while_loop() {
|
||||
int i = 0;
|
||||
char* a = safealloc(10);
|
||||
while (*(a + i) && i < 10) /* BUG */
|
||||
a[i++] = 1; /* SAFE */
|
||||
}
|
||||
Loading…
Reference in new issue