pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[pulse] move domain operations in their own submodule

Browse Source 
Summary: Just to organise PulseDomain a bit more since it's quite big.

Reviewed By: mbouaziz

Differential Revision: D10509334

fbshipit-source-id: a81b36aa6
master
Jules Villard 7 years ago committed by Facebook Github Bot
parent cb4bf4443f
commit 2c35ba51ea
1 changed files with 79 additions and 76 deletions
Show Stats Download Patch File Download Diff File

155
infer/src/checkers/PulseDomain.ml
Unescape View File

@ -376,110 +376,113 @@ module Diagnostic = struct
let get_issue_type (AccessToInvalidAddress _) = IssueType.use_after_lifetime let get_issue_type (AccessToInvalidAddress _) = IssueType.use_after_lifetime
end end
type 'a access_result = ('a, Diagnostic.t) result (** operations on the domain *)
module Operations = struct
type 'a access_result = ('a, Diagnostic.t) result
(** Check that the address is not known to be invalid *) (** Check that the address is not known to be invalid *)
let check_addr_access actor address astate = let check_addr_access actor address astate =
match InvalidAddressesDomain.get_invalidation address astate.invalids with match InvalidAddressesDomain.get_invalidation address astate.invalids with
| Some invalidated_at -> | Some invalidated_at ->
Error (Diagnostic.AccessToInvalidAddress {invalidated_at; accessed_by= actor; address}) Error (Diagnostic.AccessToInvalidAddress {invalidated_at; accessed_by= actor; address})
| None -> | None ->
Ok astate Ok astate
(** Walk the heap starting from [addr] 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_addr] if [overwrite_last] is [Some new_addr], 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 addresses into the heap as needed to follow the [path]. Check that each is [None]. Create more addresses into the heap as needed to follow the [path]. Check that each
address reached is valid. *) address reached is valid. *)
let rec walk actor ~overwrite_last addr 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, addr) Ok (astate, addr)
| [], Some _ -> | [], Some _ ->
L.die InternalError "Cannot overwrite last address in empty path" L.die InternalError "Cannot overwrite last address in empty path"
| [a], Some new_addr -> | [a], Some new_addr ->
check_addr_access actor addr astate check_addr_access actor addr astate
>>| fun astate -> >>| fun astate ->
let heap = Memory.add_edge addr a new_addr astate.heap in let heap = Memory.add_edge addr a new_addr astate.heap in
({astate with heap}, new_addr) ({astate with heap}, new_addr)
| a :: path, _ -> ( | a :: path, _ -> (
check_addr_access actor addr astate check_addr_access actor addr astate
>>= fun astate -> >>= fun astate ->
match Memory.find_edge_opt addr a astate.heap with match Memory.find_edge_opt addr a astate.heap with
| None ->
let addr' = AbstractAddress.mk_fresh () in
let heap = Memory.add_edge addr a addr' astate.heap in
let astate = {astate with heap} in
walk actor ~overwrite_last addr' path astate
| Some addr' ->
walk actor ~overwrite_last addr' path astate )
(** 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 location =
let (access_var, _), access_list = AccessExpression.to_access_path access_expr in
match (overwrite_last, access_list) with
| Some new_addr, [] ->
let stack = AliasingDomain.add access_var new_addr astate.stack in
Ok ({astate with stack}, new_addr)
| None, _ | Some _, _ :: _ ->
let astate, base_addr =
match AliasingDomain.find_opt access_var astate.stack with
| Some addr ->
(astate, addr)
| None -> | None ->
let addr = AbstractAddress.mk_fresh () in let addr' = AbstractAddress.mk_fresh () in
let stack = AliasingDomain.add access_var addr astate.stack in let heap = Memory.add_edge addr a addr' astate.heap in
({astate with stack}, addr) let astate = {astate with heap} in
in walk actor ~overwrite_last addr' path astate
let actor = {access_expr; location} in | Some addr' ->
walk actor ~overwrite_last base_addr access_list astate walk actor ~overwrite_last addr' path astate )
(** 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 location =
let (access_var, _), access_list = AccessExpression.to_access_path access_expr in
match (overwrite_last, access_list) with
| Some new_addr, [] ->
let stack = AliasingDomain.add access_var new_addr astate.stack in
Ok ({astate with stack}, new_addr)
| None, _ | Some _, _ :: _ ->
let astate, base_addr =
match AliasingDomain.find_opt access_var astate.stack with
| Some addr ->
(astate, addr)
| None ->
let addr = AbstractAddress.mk_fresh () in
let stack = AliasingDomain.add access_var addr astate.stack in
({astate with stack}, addr)
in
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 address representing what the expression points to. abstract address representing what the expression points to.
Return an error state if it traverses some known invalid address 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_address 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 address 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
address. address.
Return an error state if it traverses some known invalid address. *) Return an error state if it traverses some known invalid address. *)
let overwrite_address astate access_expr new_addr = let overwrite_address astate access_expr new_addr =
walk_access_expr ~overwrite_last:new_addr astate access_expr walk_access_expr ~overwrite_last:new_addr astate access_expr
(** Add the given address to the set of know invalid addresses. *) (** Add the given address to the set of know invalid addresses. *)
let mark_invalid actor address astate = let mark_invalid actor address astate =
{astate with invalids= InvalidAddressesDomain.add address actor astate.invalids} {astate with invalids= InvalidAddressesDomain.add address actor astate.invalids}
let read location access_expr astate = let read location access_expr astate =
materialize_address astate access_expr location materialize_address astate access_expr location
>>= fun (astate, addr) -> >>= fun (astate, addr) ->
let actor = {access_expr; location} in let actor = {access_expr; location} in
check_addr_access actor addr astate >>| fun astate -> (astate, addr) check_addr_access actor addr astate >>| fun astate -> (astate, addr)
let read_all location access_exprs 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 location access_expr astate >>| fst ) read location access_expr astate >>| fst )
let write location access_expr addr astate = let write location access_expr addr astate =
overwrite_address astate access_expr addr location >>| fun (astate, _) -> astate overwrite_address astate access_expr addr location >>| fun (astate, _) -> astate
let havoc var astate = {astate with stack= AliasingDomain.remove var astate.stack} let havoc var astate = {astate with stack= AliasingDomain.remove var astate.stack}
let invalidate location access_expr astate =
materialize_address astate access_expr location
>>= fun (astate, addr) ->
let actor = {access_expr; location} in
check_addr_access actor addr astate >>| mark_invalid actor addr
let invalidate location access_expr astate =
materialize_address astate access_expr location
>>= fun (astate, addr) ->
let actor = {access_expr; location} in
check_addr_access actor addr astate >>| mark_invalid actor addr
end
include Domain include Domain
include Operations

Write Preview
Loading…
Cancel
Save