@ -10,7 +10,7 @@ module L = Logging
open Result . Monad_infix open Result . Monad_infix
(* * An abstract address in memory. *) (* * An abstract address in memory. *)
module Abstract Location : sig module Abstract Address : sig
type t = private int [ @@ deriving compare ]
type t = private int [ @@ deriving compare ]
val equal : t -> t -> bool
val equal : t -> t -> bool
@ -33,18 +33,18 @@ end = struct
let pp = F . pp_print_int
let pp = F . pp_print_int
end end
module Abstract Location Domain : AbstractDomain . S with type astate = Abstract Location . t = struct module Abstract Address Domain : AbstractDomain . S with type astate = Abstract Address . t = struct
type astate = Abstract Location . t
type astate = Abstract Address . t
let ( < = ) ~ lhs ~ rhs = Abstract Location . equal lhs rhs
let ( < = ) ~ lhs ~ rhs = Abstract Address . equal lhs rhs
let join l1 l2 =
let join l1 l2 =
if Abstract Location . equal l1 l2 then l1 else (* TODO: scary *) Abstract Location . mk_fresh ()
if Abstract Address . equal l1 l2 then l1 else (* TODO: scary *) Abstract Address . mk_fresh ()
let widen ~ prev ~ next ~ num_iters : _ = join prev next
let widen ~ prev ~ next ~ num_iters : _ = join prev next
let pp = Abstract Location . pp
let pp = Abstract Address . pp
end end
module Access = struct module Access = struct
@ -53,32 +53,64 @@ module Access = struct
let pp = AccessPath . pp_access
let pp = AccessPath . pp_access
end end
module MemoryEdges = AbstractDomain . InvertedMap ( Access ) ( Abstract Location Domain) module MemoryEdges = AbstractDomain . InvertedMap ( Access ) ( Abstract Address Domain)
module MemoryDomain = struct module MemoryDomain = struct
include AbstractDomain . InvertedMap ( Abstract Location ) ( MemoryEdges )
include AbstractDomain . InvertedMap ( Abstract Address ) ( MemoryEdges )
let add_edge loc_src access loc _end memory =
let add_edge addr_src access addr _end memory =
let edges =
let edges =
match find_opt loc _src memory with Some edges -> edges | None -> MemoryEdges . empty
match find_opt addr _src memory with Some edges -> edges | None -> MemoryEdges . empty
in
in
add loc_src ( MemoryEdges . add access loc _end edges ) memory
add addr_src ( MemoryEdges . add access addr _end edges ) memory
let find_edge_opt loc access memory =
let find_edge_opt addr access memory =
let open Option . Monad_infix in
let open Option . Monad_infix in
find_opt loc memory > > = MemoryEdges . find_opt access
find_opt addr memory > > = MemoryEdges . find_opt access
end end
module AliasingDomain = AbstractDomain . InvertedMap ( Var ) ( AbstractLocationDomain ) module AliasingDomain = AbstractDomain . InvertedMap ( Var ) ( AbstractAddressDomain )
module AbstractLocationsDomain = AbstractDomain . FiniteSet ( AbstractLocation )
module InvalidLocationsDomain = AbstractLocationsDomain type actor = { access_expr : AccessExpression . t ; location : Location . t }
let pp_actor f { access_expr ; location } =
F . fprintf f " %a@%a " AccessExpression . pp access_expr Location . pp location
module type InvalidAddressesDomain = sig
include AbstractDomain . S
val empty : astate
val add : AbstractAddress . t -> actor -> astate -> astate
val get_invalidation : AbstractAddress . t -> astate -> actor option
end
module InvalidAddressesDomain : InvalidAddressesDomain = struct
module InvalidationReason = struct
type astate = actor
let join actor _ = actor
let ( < = ) ~ lhs : _ ~ rhs : _ = true
let widen ~ prev ~ next : _ ~ num_iters : _ = prev
let pp = pp_actor
end
include AbstractDomain . Map ( AbstractAddress ) ( InvalidationReason )
let get_invalidation address invalids = find_opt address invalids
end
type t = type t =
{ heap : MemoryDomain . astate ; stack : AliasingDomain . astate ; invalids : InvalidLocationsDomain . astate }
{ heap : MemoryDomain . astate ; stack : AliasingDomain . astate ; invalids : Invalid Addresse sDomain. astate }
let initial = let initial =
{ heap = MemoryDomain . empty ; stack = AliasingDomain . empty ; invalids = AbstractLocationsDomain . empty }
{ heap = MemoryDomain . empty ; stack = AliasingDomain . empty ; invalids = InvalidAddresse sDomain. empty }
module Domain : AbstractDomain . S with type astate = t = struct module Domain : AbstractDomain . S with type astate = t = struct
@ -91,7 +123,7 @@ module Domain : AbstractDomain.S with type astate = t = struct
into the heap . * )
into the heap . * )
let ( < = ) ~ lhs ~ rhs =
let ( < = ) ~ lhs ~ rhs =
phys_equal lhs rhs
phys_equal lhs rhs
| | Invalid Location sDomain. ( < = ) ~ lhs : lhs . invalids ~ rhs : rhs . invalids
| | Invalid Addresse sDomain. ( < = ) ~ lhs : lhs . invalids ~ rhs : rhs . invalids
&& AliasingDomain . ( < = ) ~ lhs : lhs . stack ~ rhs : rhs . stack
&& AliasingDomain . ( < = ) ~ lhs : lhs . stack ~ rhs : rhs . stack
&& MemoryDomain . ( < = ) ~ lhs : lhs . heap ~ rhs : rhs . heap
&& MemoryDomain . ( < = ) ~ lhs : lhs . heap ~ rhs : rhs . heap
@ -102,7 +134,7 @@ module Domain : AbstractDomain.S with type astate = t = struct
else
else
{ heap = MemoryDomain . join astate1 . heap astate2 . heap
{ heap = MemoryDomain . join astate1 . heap astate2 . heap
; stack = AliasingDomain . join astate1 . stack astate2 . stack
; stack = AliasingDomain . join astate1 . stack astate2 . stack
; invalids = Invalid Location sDomain. join astate1 . invalids astate2 . invalids }
; invalids = Invalid Addresse sDomain. join astate1 . invalids astate2 . invalids }
let max_widening = 5
let max_widening = 5
@ -116,117 +148,146 @@ module Domain : AbstractDomain.S with type astate = t = struct
else
else
{ heap = MemoryDomain . widen ~ num_iters ~ prev : prev . heap ~ next : next . heap
{ heap = MemoryDomain . widen ~ num_iters ~ prev : prev . heap ~ next : next . heap
; stack = AliasingDomain . widen ~ num_iters ~ prev : prev . stack ~ next : next . stack
; stack = AliasingDomain . widen ~ num_iters ~ prev : prev . stack ~ next : next . stack
; invalids = Invalid Location sDomain. widen ~ num_iters ~ prev : prev . invalids ~ next : next . invalids
; invalids = Invalid Addresse sDomain. widen ~ num_iters ~ prev : prev . invalids ~ next : next . invalids
}
}
let pp fmt { heap ; stack ; invalids } =
let pp fmt { heap ; stack ; invalids } =
F . fprintf fmt " {@[<v1> heap=@[<hv>%a@];@;stack=@[<hv>%a@];@;invalids=@[<hv>%a@];@]} "
F . fprintf fmt " {@[<v1> heap=@[<hv>%a@];@;stack=@[<hv>%a@];@;invalids=@[<hv>%a@];@]} "
MemoryDomain . pp heap AliasingDomain . pp stack Invalid Location sDomain. pp invalids
MemoryDomain . pp heap AliasingDomain . pp stack Invalid Addresse sDomain. pp invalids
end end
include Domain include Domain
module Diagnostic = struct module Diagnostic = struct
(* TODO: more structured error type so that we can actually report something informative about
type t =
the variables being accessed along with a trace * )
| AccessToInvalidAddress of
type t = InvalidLocation of AbstractLocation . t
{ invalidated_at : actor
; accessed_by : actor
; address : AbstractAddress . t }
let get_location ( AccessToInvalidAddress { accessed_by = { location } } ) = location
let to_string ( InvalidLocation loc ) = F . asprintf " invalid location %a " AbstractLocation . pp loc
let get_message ( AccessToInvalidAddress { accessed_by ; invalidated_at ; address } ) =
let pp_debug_address f =
if Config . debug_mode then F . fprintf f " (debug: %a) " AbstractAddress . pp address
in
F . asprintf " `%a` accesses address `%a` past its lifetime%t " AccessExpression . pp
accessed_by . access_expr AccessExpression . pp invalidated_at . access_expr pp_debug_address
let get_trace ( AccessToInvalidAddress { accessed_by ; invalidated_at } ) =
[ Errlog . make_trace_element 0 invalidated_at . location
( F . asprintf " invalidated `%a` here " AccessExpression . pp invalidated_at . access_expr )
[]
; Errlog . make_trace_element 0 accessed_by . location
( F . asprintf " accessed `%a` here " AccessExpression . pp accessed_by . access_expr )
[] ]
let get_issue_type ( AccessToInvalidAddress _ ) = IssueType . use_after_lifetime
end end
type ' a access_result = ( ' a , t * Diagnostic . t ) result type ' a access_result = ( ' a , t * Diagnostic . t ) result
(* * Check that the location is not known to be invalid *) (* * Check that the address is not known to be invalid *)
let check_loc_access loc astate = let check_addr_access actor address astate =
if AbstractLocationsDomain . mem loc astate . invalids then
match InvalidAddressesDomain . get_invalidation address astate . invalids with
Error ( astate , Diagnostic . InvalidLocation loc )
| Some invalidated_at ->
else Ok astate
Error
( astate , Diagnostic . AccessToInvalidAddress { invalidated_at ; accessed_by = actor ; address } )
| None ->
Ok astate
(* * Walk the heap starting from [loc] and following [path]. Stop either at the element before last (* * Walk the heap starting from [ addr ] and following [path]. Stop either at the element before last
and return [ new_loc ] if [ overwrite_last ] is [ Some new_loc ] , or go until the end of the path if it
and return [ new_ addr ] if [ overwrite_last ] is [ Some new_ addr ] , or go until the end of the path if it
is [ None ] . Create more locations into the heap as needed to follow the [ path ] . Check that each
is [ None ] . Create more addresse s into the heap as needed to follow the [ path ] . Check that each
location reached is valid . * )
address reached is valid . * )
let rec walk ~ overwrite_last loc path astate = let rec walk actor ~ overwrite_last addr path astate =
match ( path , overwrite_last ) with
match ( path , overwrite_last ) with
| [] , None ->
| [] , None ->
Ok ( astate , loc )
Ok ( astate , addr )
| [] , Some _ ->
| [] , Some _ ->
L . die InternalError " Cannot overwrite last location in empty path"
L . die InternalError " Cannot overwrite last address in empty path"
| [ a ] , Some new_ loc ->
| [ a ] , Some new_ addr ->
check_ loc_access loc astate
check_ addr_access actor addr astate
> > | fun astate ->
> > | fun astate ->
let heap = MemoryDomain . add_edge loc a new_loc astate . heap in
let heap = MemoryDomain . add_edge addr a new_addr astate . heap in
( { astate with heap } , new_ loc )
( { astate with heap } , new_ addr )
| a :: path , _ -> (
| a :: path , _ -> (
check_ loc_access loc astate
check_ addr_access actor addr astate
> > = fun astate ->
> > = fun astate ->
match MemoryDomain . find_edge_opt loc a astate . heap with
match MemoryDomain . find_edge_opt addr a astate . heap with
| None ->
| None ->
let loc' = AbstractLocation . mk_fresh () in
let addr' = AbstractAddress . mk_fresh () in
let heap = MemoryDomain . add_edge loc a loc ' astate . heap in
let heap = MemoryDomain . add_edge addr a addr ' astate . heap in
let astate = { astate with heap } in
let astate = { astate with heap } in
walk ~ overwrite_last loc path astate
walk actor ~ overwrite_last addr path astate
| Some loc ' ->
| Some addr ' ->
walk ~ overwrite_last loc path astate )
walk actor ~ overwrite_last addr path astate )
(* * add locations to the state to give a location to the destination of the given access path *) (* * add addresses to the state to give a address to the destination of the given access path *)
let walk_access_expr ? overwrite_last astate access_expr = let walk_access_expr ? overwrite_last astate access_expr location =
let ( access_var , _ ) , access_list = AccessExpression . to_access_path access_expr in
let ( access_var , _ ) , access_list = AccessExpression . to_access_path access_expr in
match ( overwrite_last , access_list ) with
match ( overwrite_last , access_list ) with
| Some new_ loc , [] ->
| Some new_ addr , [] ->
let stack = AliasingDomain . add access_var new_ loc astate . stack in
let stack = AliasingDomain . add access_var new_ addr astate . stack in
Ok ( { astate with stack } , new_ loc )
Ok ( { astate with stack } , new_ addr )
| None , _ | Some _ , _ :: _ ->
| None , _ | Some _ , _ :: _ ->
let astate , base_ loc =
let astate , base_ addr =
match AliasingDomain . find_opt access_var astate . stack with
match AliasingDomain . find_opt access_var astate . stack with
| Some loc ->
| Some addr ->
( astate , loc )
( astate , addr )
| None ->
| None ->
let loc = AbstractLocation . mk_fresh () in
let addr = AbstractAddress . mk_fresh () in
let stack = AliasingDomain . add access_var loc astate . stack in
let stack = AliasingDomain . add access_var addr astate . stack in
( { astate with stack } , loc )
( { astate with stack } , addr )
in
in
walk ~ overwrite_last base_loc access_list astate
let actor = { access_expr ; location } in
walk actor ~ overwrite_last base_addr access_list astate
(* * Use the stack and heap to walk the access path represented by the given expression down to an (* * Use the stack and heap to walk the access path represented by the given expression down to an
abstract location representing what the expression points to .
abstract address representing what the expression points to .
Return an error state if it traverses some known invalid location or if the end destination is
Return an error state if it traverses some known invalid address or if the end destination is
known to be invalid . * )
known to be invalid . * )
let materialize_ location astate access_expr = walk_access_expr astate access_expr let materialize_ address astate access_expr = walk_access_expr astate access_expr
(* * Use the stack and heap to walk the access path represented by the given expression down to an (* * Use the stack and heap to walk the access path represented by the given expression down to an
abstract location representing what the expression points to , and replace that with the given
abstract address representing what the expression points to , and replace that with the given
location .
address .
Return an error state if it traverses some known invalid location . * )
Return an error state if it traverses some known invalid address . * )
let overwrite_ location astate access_expr new_loc = let overwrite_ address astate access_expr new_addr =
walk_access_expr ~ overwrite_last : new_ loc astate access_expr
walk_access_expr ~ overwrite_last : new_ addr astate access_expr
(* * Add the given location to the set of know invalid location s. *) (* * Add the given address to the set of know invalid addresse s. *)
let mark_invalid loc astate = let mark_invalid actor address astate =
{ astate with invalids = AbstractLocationsDomain. add loc astate . invalids }
{ astate with invalids = InvalidAddressesDomain. add address actor astate . invalids }
let read access_expr astate = let read location access_expr astate =
materialize_location astate access_expr
materialize_address astate access_expr location
> > = fun ( astate , loc ) -> check_loc_access loc astate > > | fun astate -> ( astate , loc )
> > = fun ( astate , addr ) ->
let actor = { access_expr ; location } in
check_addr_access actor addr astate > > | fun astate -> ( astate , addr )
let read_all astate = let read_all location access_exprs astate =
List . fold_result access_exprs ~ init : astate ~ f : ( fun astate access_expr ->
List . fold_result access_exprs ~ init : astate ~ f : ( fun astate access_expr ->
read astate > > | fst )
read location access_expr astate > > | fst )
let write access_expr loc astate = let write location access_expr addr astate =
overwrite_ location astate access_expr loc > > | fun ( astate , _ ) -> astate
overwrite_ address astate access_expr addr location > > | fun ( astate , _ ) -> astate
let invalidate access_expr astate = let invalidate location access_expr astate =
materialize_location astate access_expr
materialize_address astate access_expr location
> > = fun ( astate , loc ) -> check_loc_access loc astate > > | mark_invalid loc
> > = fun ( astate , addr ) ->
let actor = { access_expr ; location } in
check_addr_access actor addr astate > > | mark_invalid actor addr
Jules Villard
6 years ago
committed by
Facebook Github Bot