diff --git a/Makefile b/Makefile
index 69e9b86684f6cde8b04d6a6f5b12987de89a81e7..fa46f8a3cd2c5d575a9fc6e3ad508a50c506e1c6 100644
--- a/Makefile
+++ b/Makefile
@@ -893,11 +893,11 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
domains/cvalue/cvalue_transfer domains/cvalue/cvalue_init \
domains/cvalue/cvalue_specification \
domains/cvalue/cvalue_domain \
- engine/subdivided_evaluation engine/evaluation engine/abstractions \
- engine/recursion engine/transfer_stmt engine/transfer_specification \
partitioning/auto_loop_unroll \
partitioning/partition partitioning/partitioning_parameters \
partitioning/partitioning_index partitioning/trace_partitioning \
+ engine/subdivided_evaluation engine/evaluation engine/abstractions \
+ engine/recursion engine/transfer_stmt engine/transfer_specification \
engine/mem_exec engine/iterator engine/initialization \
engine/compute_functions engine/analysis register \
domains/taint_domain \
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index a93a27e8d5108786d89fc716f2bae3d2361dcdf7..f1903160445882ac1afdab06a6f9c72748c59495 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -164,7 +164,7 @@ module Make (Abstract: Abstractions.Eva) = struct
is the instruction at which the call takes place, and is used to update
the statuses of the preconditions of [kf]. If [show_progress] is true,
the callstack and additional information are printed. *)
- let compute_using_spec_or_body call_kinstr call recursion pkey state =
+ let compute_using_spec_or_body call_kinstr call recursion state =
let kf = call.kf in
Value_results.mark_kf_as_called kf;
let global = match call_kinstr with Kglobal -> true | _ -> false in
@@ -199,8 +199,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let vi = Kernel_function.get_vi kf in
if Cil.is_in_libc vi.vattr then
Library_functions.warn_unsupported_spec vi.vorig_name;
- Spec.compute_using_specification ~warn:true
- call_kinstr call spec (pkey,state),
+ Spec.compute_using_specification ~warn:true call_kinstr call spec state,
Eval.Cacheable
| `Def _fundec ->
Db.Value.Call_Type_Value_Callbacks.apply (`Def, cvalue_state, call_stack);
@@ -216,9 +215,9 @@ module Make (Abstract: Abstractions.Eva) = struct
module MemExec = Mem_exec.Make (Abstract.Val) (Abstract.Dom)
- let compute_and_cache_call stmt call recursion pkey init_state =
+ let compute_and_cache_call stmt call recursion init_state =
let default () =
- compute_using_spec_or_body (Kstmt stmt) call recursion pkey init_state
+ compute_using_spec_or_body (Kstmt stmt) call recursion init_state
in
if Value_parameters.MemExecAll.get () then
let args =
@@ -275,14 +274,14 @@ module Make (Abstract: Abstractions.Eva) = struct
let rest = List.map (fun (e, assgn) -> e, lift_assigned assgn) call.rest in
{ call with arguments; rest }
- let join_states default_key = function
+ let join_states = function
| [] -> `Bottom
| (_k,s) :: l ->
- `Value (default_key, List.fold_left Abstract.Dom.join s (List.map snd l))
+ `Value (List.fold_left Abstract.Dom.join s (List.map snd l))
- let compute_call_or_builtin stmt call recursion pkey state =
+ let compute_call_or_builtin stmt call recursion state =
match Builtins.find_builtin_override call.kf with
- | None -> compute_and_cache_call stmt call recursion pkey state
+ | None -> compute_and_cache_call stmt call recursion state
| Some (name, builtin, cacheable, spec) ->
Value_results.mark_kf_as_called call.kf;
let kinstr = Kstmt stmt in
@@ -295,9 +294,9 @@ module Make (Abstract: Abstractions.Eva) = struct
as the result of the cvalue builtin will overwrite them. *)
Locations.Location_Bytes.do_track_garbled_mix false;
let states = Spec.compute_using_specification
- ~warn:false kinstr call spec (pkey,state) in
+ ~warn:false kinstr call spec state in
Locations.Location_Bytes.do_track_garbled_mix true;
- let final_state = join_states pkey states in
+ let final_state = join_states states in
let cvalue_state = Abstract.Dom.get_cvalue_or_top state in
match final_state with
| `Bottom ->
@@ -305,32 +304,25 @@ module Make (Abstract: Abstractions.Eva) = struct
Db.Value.Call_Type_Value_Callbacks.apply (`Spec spec, cvalue_state, cs);
let cacheable = Eval.Cacheable in
Transfer.{states; cacheable; builtin=true}
- | `Value (pkey,final_state) ->
+ | `Value final_state ->
let cvalue_call = get_cvalue_call call in
let post = Abstract.Dom.get_cvalue_or_top final_state in
let cvalue_states =
Builtins.apply_builtin builtin cvalue_call ~pre:cvalue_state ~post
in
let insert cvalue_state =
- pkey,Abstract.Dom.set Cvalue_domain.State.key cvalue_state final_state
+ Partition.Key.zero,
+ Abstract.Dom.set Cvalue_domain.State.key cvalue_state final_state
in
let states = List.map insert cvalue_states in
Transfer.{states; cacheable; builtin=true}
- let recombine_keys compute =
- fun stmt call recursion pkey state ->
- let result = compute stmt call recursion Partition.Key.zero state in
- let recombine (pkey',state') =
- Partition.Key.recombine pkey pkey', state'
- in
- Transfer.{ result with states = List.map recombine result.states }
-
let compute_call =
if Abstract.Dom.mem Cvalue_domain.State.key
&& Abstract.Val.mem Main_values.CVal.key
&& Abstract.Loc.mem Main_locations.PLoc.key
- then recombine_keys compute_call_or_builtin
- else recombine_keys compute_and_cache_call
+ then compute_call_or_builtin
+ else compute_and_cache_call
let () = Transfer.compute_call_ref := compute_call
@@ -347,9 +339,8 @@ module Make (Abstract: Abstractions.Eva) = struct
let call =
{ kf; callstack = []; arguments = []; rest = []; return = None; }
in
- let pkey = Partition.Key.zero in
let final_result =
- compute_using_spec_or_body Kglobal call None pkey init_state
+ compute_using_spec_or_body Kglobal call None init_state
in
let final_states = List.map snd (final_result.Transfer.states) in
let final_state = PowersetDomain.(final_states |> of_list |> join) in
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index dac195362c4838e0e2c6c5ed536eb915f08b3253..17ae93256275156c24a8165202a06f6c7b5418f2 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -275,12 +275,13 @@ module Make_Dataflow
let transfer_call (stmt : stmt) (dest : lval option) (callee : exp)
(args : exp list) (key,state : key * state) : (key*state) list =
let result, call_cacheable =
- Transfer.call stmt dest callee args key state
+ Transfer.call stmt dest callee args state
in
if call_cacheable = Eval.NoCacheCallers then
(* Propagate info that the current call cannot be cached either *)
cacheable := Eval.NoCacheCallers;
- result
+ (* Recombine callee partitioning keys with caller key *)
+ List.map (fun (k,s) -> Partition.Key.recombine key k, s) result
let transfer_instr (stmt : stmt) (instr : instr) : transfer_function =
match instr with
diff --git a/src/plugins/value/engine/transfer_specification.ml b/src/plugins/value/engine/transfer_specification.ml
index 955d7456f848531140c68746290251ebe463f06a..76c7d21cb0f2760bb9400292dad68fe166ab5d1c 100644
--- a/src/plugins/value/engine/transfer_specification.ml
+++ b/src/plugins/value/engine/transfer_specification.ml
@@ -564,7 +564,7 @@ module Make
evaluates the assigns, and finally reduces by the post-conditions.
[warn] is false for the specification of cvalue builtins — in this case,
some warnings are disabled, such as warnings about new garbled mixes. *)
- let compute_using_specification ~warn kinstr call spec (key,state) =
+ let compute_using_specification ~warn kinstr call spec state =
let vi = Kernel_function.get_vi call.kf in
if Cil.hasAttribute "noreturn" vi.vattr
then []
@@ -582,6 +582,6 @@ module Make
let states =
compute_specification ~warn kinstr call.kf call.return spec state
in
- List.map (fun x -> key,x) (States.to_list states)
+ List.map (fun s -> Partition.Key.zero, s) (States.to_list states)
end
diff --git a/src/plugins/value/engine/transfer_specification.mli b/src/plugins/value/engine/transfer_specification.mli
index 4c5a61b77674fa895cb60a48096afe8b6b98f850..93ea891b66ca643709c14845b09d4b984bf4f2a6 100644
--- a/src/plugins/value/engine/transfer_specification.mli
+++ b/src/plugins/value/engine/transfer_specification.mli
@@ -35,6 +35,6 @@ module Make
val compute_using_specification:
warn:bool ->
kinstr -> (Abstract.Loc.location, Abstract.Val.t) call -> spec ->
- (Partition.key * Abstract.Dom.t) -> (Partition.key * Abstract.Dom.t) list
+ Abstract.Dom.t -> (Partition.key*Abstract.Dom.t) list
end
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 48c36f6d513015abedea72815d5ee725a23d886a..e391fe01811f771f99a0f70b024f7270c402d76e 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -32,7 +32,7 @@ module type S = sig
val assign: state -> kinstr -> lval -> exp -> state or_bottom
val assume: state -> stmt -> exp -> bool -> state or_bottom
val call:
- stmt -> lval option -> exp -> exp list -> pkey -> state ->
+ stmt -> lval option -> exp -> exp list -> state ->
(pkey*state) list * Eval.cacheable
val check_unspecified_sequence:
stmt ->
@@ -45,7 +45,7 @@ module type S = sig
builtin: bool;
}
val compute_call_ref:
- (stmt -> (loc, value) call -> recursion option -> pkey -> state ->
+ (stmt -> (loc, value) call -> recursion option -> state ->
call_result) ref
end
@@ -306,13 +306,13 @@ module Make (Abstract: Abstractions.Eva) = struct
(* Forward reference to [Eval_funs.compute_call] *)
let compute_call_ref :
- (stmt -> (loc, value) call -> recursion option -> pkey -> state ->
+ (stmt -> (loc, value) call -> recursion option -> state ->
call_result) ref
= ref (fun _ -> assert false)
(* Returns the result of a call, and a boolean that indicates whether a
builtin has been used to interpret the call. *)
- let process_call stmt call recursion valuation pkey state =
+ let process_call stmt call recursion valuation state =
Value_util.push_call_stack call.kf (Kstmt stmt);
let cleanup () =
Value_util.pop_call_stack ();
@@ -326,7 +326,7 @@ module Make (Abstract: Abstractions.Eva) = struct
match Domain.start_call stmt call recursion domain_valuation state with
| `Value state ->
Domain.Store.register_initial_state (Value_util.call_stack ()) state;
- !compute_call_ref stmt call recursion pkey state
+ !compute_call_ref stmt call recursion state
| `Bottom ->
{ states = []; cacheable = Cacheable; builtin=false }
in
@@ -459,11 +459,11 @@ module Make (Abstract: Abstractions.Eva) = struct
Kernel_function.get_formals kf @ locals
(* Do the call to one function. *)
- let do_one_call valuation stmt lv call recursion key state =
+ let do_one_call valuation stmt lv call recursion state =
let kf_callee = call.kf in
let pre = state in
(* Process the call according to the domain decision. *)
- let call_result = process_call stmt call recursion valuation key state in
+ let call_result = process_call stmt call recursion valuation state in
let leaving_vars = leaving_vars kf_callee in
(* Do not try to reduce concrete arguments if a builtin was used. *)
let gather_reduced_arguments =
@@ -739,7 +739,7 @@ module Make (Abstract: Abstractions.Eva) = struct
(* --------------------- Process the call statement ---------------------- *)
- let call stmt lval_option funcexp args pkey state =
+ let call stmt lval_option funcexp args state =
let ki_call = Kstmt stmt in
let subdivnb = subdivide_stmt stmt in
(* Resolve [funcexp] into the called kernel functions. *)
@@ -756,7 +756,7 @@ module Make (Abstract: Abstractions.Eva) = struct
if apply_special_directives ~subdivnb kf args state
then
let () = apply_cvalue_callback kf ki_call state in
- [(pkey,state)]
+ [(Partition.Key.zero,state)]
else
(* Create the call. *)
let eval, alarms = make_call ~subdivnb kf args valuation state in
@@ -766,7 +766,7 @@ module Make (Abstract: Abstractions.Eva) = struct
Value_results.add_kf_caller call.kf ~caller:(current_kf, stmt);
(* Do the call. *)
let c, states =
- do_one_call valuation stmt lval_option call recursion pkey state
+ do_one_call valuation stmt lval_option call recursion state
in
(* If needed, propagate that callers cannot be cached. *)
if c = NoCacheCallers then
diff --git a/src/plugins/value/engine/transfer_stmt.mli b/src/plugins/value/engine/transfer_stmt.mli
index 4be96180e162ce26dd3b62cd884fc94a3500e5ad..7952b23f35e8a2fe2508f0c6aaeb5f489a130040 100644
--- a/src/plugins/value/engine/transfer_stmt.mli
+++ b/src/plugins/value/engine/transfer_stmt.mli
@@ -37,7 +37,7 @@ module type S = sig
val assume: state -> stmt -> exp -> bool -> state or_bottom
val call:
- stmt -> lval option -> exp -> exp list -> pkey -> state ->
+ stmt -> lval option -> exp -> exp list -> state ->
(pkey*state) list * Eval.cacheable
val check_unspecified_sequence:
@@ -56,7 +56,7 @@ module type S = sig
}
val compute_call_ref:
- (stmt -> (loc, value) call -> recursion option -> pkey -> state -> call_result) ref
+ (stmt -> (loc, value) call -> recursion option -> state -> call_result) ref
end
module Make (Abstract: Abstractions.Eva)