@ -66,20 +66,108 @@ end
module Analyzer = AbstractInterpreter . MakeRPO ( TransferFunctions )
module Analyzer = AbstractInterpreter . MakeRPO ( TransferFunctions )
let try_keep_original ~ default orig new_ ~ f = if phys_equal orig new_ then default else f new_
let try_keep_original2 ~ default orig1 new1 orig2 new2 ~ f =
if phys_equal orig1 new1 && phys_equal orig2 new2 then default else f new1 new2
let exec_pvar pname pvar = Pvar . swap_proc_in_local_pvar pvar pname
let exec_var pname var =
let open Var in
match var with
| LogicalVar _ ->
var
| ProgramVar pvar ->
try_keep_original ~ default : var pvar ( exec_pvar pname pvar ) ~ f : of_pvar
let rec exec_exp pname e =
let open Exp in
match e with
| Var _ | Const _ ->
e
| UnOp ( unop , e1 , typ ) ->
try_keep_original ~ default : e e1 ( exec_exp pname e1 ) ~ f : ( fun e1' -> UnOp ( unop , e1' , typ ) )
| BinOp ( binop , e1 , e2 ) ->
try_keep_original2 ~ default : e e1 ( exec_exp pname e1 ) e2 ( exec_exp pname e2 ) ~ f : ( fun e1' e2' ->
BinOp ( binop , e1' , e2' ) )
| Exn e1 ->
try_keep_original ~ default : e e1 ( exec_exp pname e1 ) ~ f : ( fun e1' -> Exn e1' )
| Closure { name ; captured_vars } ->
let updated = ref false in
let captured_vars =
List . map captured_vars ~ f : ( fun ( ( e , pvar , typ , captured_mode ) as captured_var ) ->
try_keep_original2 ~ default : captured_var e ( exec_exp pname e ) pvar
( exec_pvar pname pvar ) ~ f : ( fun e' pvar' ->
updated := true ;
( e' , pvar' , typ , captured_mode ) ) )
in
if ! updated then Closure { name ; captured_vars } else e
| Cast ( typ , e1 ) ->
try_keep_original ~ default : e e1 ( exec_exp pname e1 ) ~ f : ( fun e1' -> Cast ( typ , e1' ) )
| Lvar pvar ->
try_keep_original ~ default : e pvar ( exec_pvar pname pvar ) ~ f : ( fun pvar' -> Lvar pvar' )
| Lfield ( e1 , fn , typ ) ->
try_keep_original ~ default : e e1 ( exec_exp pname e1 ) ~ f : ( fun e1' -> Lfield ( e1' , fn , typ ) )
| Lindex ( e1 , e2 ) ->
try_keep_original2 ~ default : e e1 ( exec_exp pname e1 ) e2 ( exec_exp pname e2 ) ~ f : ( fun e1' e2' ->
Lindex ( e1' , e2' ) )
| Sizeof { typ ; nbytes ; dynamic_length ; subtype } ->
Option . value_map dynamic_length ~ default : e ~ f : ( fun dynamic_length ->
try_keep_original ~ default : e dynamic_length ( exec_exp pname dynamic_length )
~ f : ( fun dynamic_length' ->
Sizeof { typ ; nbytes ; dynamic_length = Some dynamic_length' ; subtype } ) )
let exec_metadata pname metadata =
let open Sil in
match metadata with
| Abstract _ | Skip ->
metadata
| ExitScope ( vars , loc ) ->
let updated = ref false in
let vars' =
List . map vars ~ f : ( fun var ->
try_keep_original ~ default : var var ( exec_var pname var ) ~ f : ( fun var' ->
updated := true ;
var' ) )
in
if ! updated then ExitScope ( vars' , loc ) else metadata
| Nullify ( pvar , loc ) ->
try_keep_original ~ default : metadata pvar ( exec_pvar pname pvar ) ~ f : ( fun pvar' ->
Nullify ( pvar' , loc ) )
| VariableLifetimeBegins ( pvar , typ , loc ) ->
try_keep_original ~ default : metadata pvar ( exec_pvar pname pvar ) ~ f : ( fun pvar' ->
VariableLifetimeBegins ( pvar' , typ , loc ) )
let exec_args proc_name args =
let updated = ref false in
let args' =
List . map
~ f : ( fun ( ( exp , typ ) as exp_typ ) ->
try_keep_original ~ default : exp_typ exp ( exec_exp proc_name exp ) ~ f : ( fun exp' ->
updated := true ;
( exp' , typ ) ) )
args
in
if ! updated then args' else args
let exec_instr proc_name ( id_to_pvar_map , pvars_to_blocks_map ) instr =
let exec_instr proc_name ( id_to_pvar_map , pvars_to_blocks_map ) instr =
let open Sil in
let open Sil in
let res =
let res =
let exec_exp exp =
let exec_pvar pvar = Pvar . swap_proc_in_local_pvar pvar proc_name in
match exp with Exp . Lvar origin_pvar -> Exp . Lvar ( exec_pvar origin_pvar ) | exp -> exp
in
match instr with
match instr with
| Load { id ; e ; root_typ ; loc } ->
| Load { id ; e ; root_typ ; loc } ->
[ Load { id ; e = exec_exp e ; root_typ ; typ = root_typ ; loc } ]
[ try_keep_original ~ default : instr e ( exec_exp proc_name e ) ~ f : ( fun e' ->
Load { id ; e = e' ; root_typ ; typ = root_typ ; loc } ) ]
| Store { e1 ; root_typ ; typ ; e2 ; loc } ->
| Store { e1 ; root_typ ; typ ; e2 ; loc } ->
[ Store { e1 = exec_exp e1 ; root_typ ; typ ; e2 = exec_exp e2 ; loc } ]
[ try_keep_original2 ~ default : instr e1 ( exec_exp proc_name e1 ) e2 ( exec_exp proc_name e2 )
~ f : ( fun e1' e2' -> Store { e1 = e1' ; root_typ ; typ ; e2 = e2' ; loc } ) ]
| Call ( ret_id_typ , Var id , origin_args , loc , call_flags ) -> (
| Call ( ret_id_typ , Var id , origin_args , loc , call_flags ) -> (
let converted_args = List . map ~ f : ( fun ( exp , typ ) -> ( exec_exp exp , typ ) ) origin_args in
let converted_args = exec_args proc_name origin_args in
match Option . bind ~ f : VDom . get ( BlockIdMap . find_opt id id_to_pvar_map ) with
match Option . bind ~ f : VDom . get ( BlockIdMap . find_opt id id_to_pvar_map ) with
| None ->
| None ->
[ instr ]
[ instr ]
@ -107,12 +195,16 @@ let exec_instr proc_name (id_to_pvar_map, pvars_to_blocks_map) instr =
| None ->
| None ->
[ instr ] ) )
[ instr ] ) )
| Call ( return_ids , origin_call_exp , origin_args , loc , call_flags ) ->
| Call ( return_ids , origin_call_exp , origin_args , loc , call_flags ) ->
let converted_args = List . map ~ f : ( fun ( exp , typ ) -> ( exec_exp exp , typ ) ) origin_args in
[ try_keep_original2 ~ default : instr origin_call_exp ( exec_exp proc_name origin_call_exp )
[ Call ( return_ids , exec_exp origin_call_exp , converted_args , loc , call_flags ) ]
origin_args ( exec_args proc_name origin_args )
~ f : ( fun converted_call_exp converted_args ->
Call ( return_ids , converted_call_exp , converted_args , loc , call_flags ) ) ]
| Prune ( origin_exp , loc , is_true_branch , if_kind ) ->
| Prune ( origin_exp , loc , is_true_branch , if_kind ) ->
[ Prune ( exec_exp origin_exp , loc , is_true_branch , if_kind ) ]
[ try_keep_original ~ default : instr origin_exp ( exec_exp proc_name origin_exp )
| _ ->
~ f : ( fun converted_exp -> Prune ( converted_exp , loc , is_true_branch , if_kind ) ) ]
[ instr ]
| Metadata metadata ->
[ try_keep_original ~ default : instr metadata ( exec_metadata proc_name metadata )
~ f : ( fun metadata' -> Metadata metadata' ) ]
in
in
Array . of_list res
Array . of_list res