Skip to content

Use LazyEval instead of Lazy in C2PODomain. #1717

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Mar 26, 2025
Merged

Use LazyEval instead of Lazy in C2PODomain. #1717

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
4632f6a
Use LazyEval instead of Lazy in C2PODomain.
jerhard Mar 25, 2025
e8e6b58
Undo spurious changes to c2poAnalysis.
jerhard Mar 25, 2025
26d7695
Remove unused open GoblintCil.
jerhard Mar 26, 2025
8d90b50
Avoid excessive let binding.
jerhard Mar 26, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
95 changes: 52 additions & 43 deletions src/analyses/c2poAnalysis.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,8 @@ struct
(* Returns Some true if we know for sure that it is true,
and Some false if we know for sure that it is false,
and None if we don't know anyhing. *)
let eval_guard ask cc e ik =
let eval_guard ask d e ik =
let cc = d.data in
let open Queries in
let prop_list = T.prop_of_cil ask e true in
match split prop_list with
Expand Down Expand Up @@ -71,28 +72,30 @@ struct
let open Queries in
match ctx.local with
| `Bot -> Result.top q
| `Lifted cc ->
| `Lifted d ->
match q with
| EvalInt e ->
let ik = Cilfacade.get_ikind_exp e in
eval_guard (ask_of_man ctx) cc e ik
eval_guard (ask_of_man ctx) d e ik
| Queries.Invariant context ->
let scope = Node.find_fundec ctx.node in
let t = D.remove_vars_not_in_scope scope cc in
let conj = get_conjunction t in
let cc = D.remove_vars_not_in_scope scope d.data in
let conj = get_conjunction_from_data cc in
let ask = ask_of_man ctx in
conj_to_invariant ask conj
| _ ->
Result.top q

(** Assign the right hand side rhs (that is already
converted to a C-2PO term) to the term `lterm`. *)
let assign_term cc ask lterm rhs lval_t =
let assign_term d ask lterm rhs lval_t =
let cc = d.data in
(* ignore assignments to values that are not 64 bits *)
match T.get_element_size_in_bits lval_t, rhs with
(* Indefinite assignment *)
| lval_size, (None, _) ->
D.remove_may_equal_terms ask lval_size lterm cc
let cc = D.remove_may_equal_terms ask lval_size lterm cc in
data_to_t cc
(* Definite assignment *)
| lval_size, (Some rterm, Some roffset) ->
let dummy_var = MayBeEqual.dummy_var lval_t in
Expand All @@ -106,8 +109,8 @@ struct
meet_conjs_opt equal_dummy_rterm |>
D.remove_may_equal_terms ask lval_size lterm |>
meet_conjs_opt equal_dummy_lterm |>
D.remove_terms_containing_aux_variable

D.remove_terms_containing_aux_variable |>
data_to_t
| _ -> (* this is impossible *)
C2PODomain.top ()

Expand All @@ -131,8 +134,8 @@ struct
match ctx.local with
| `Bot ->
`Bot
| `Lifted cc ->
let cc = assign_lval cc ask lval (T.of_cil ask expr) in
| `Lifted d ->
let cc = assign_lval d ask lval (T.of_cil ask expr) in
let cc = reset_normal_form cc in
let res = `Lifted cc in
if M.tracing then M.trace "c2po-assign" "assign: var: %a; expr: %a; result: %s.\n" d_lval lval d_plainexp expr (D.show res);
Expand All @@ -144,13 +147,13 @@ struct
let res =
match ctx.local with
| `Bot -> `Bot
| `Lifted cc ->
| `Lifted d ->
if List.is_empty valid_props then
`Lifted cc
`Lifted d
else
try
let meet = meet_conjs_opt valid_props cc in
let t = reset_normal_form meet in
let meet = meet_conjs_opt valid_props d.data in
let t = data_to_t meet in
`Lifted t
with Unsat ->
`Bot
Expand All @@ -167,8 +170,8 @@ struct
match T.of_cil ask expr with
| (Some term, Some offset) ->
let ret_var_eq_term = [Equal (return_var, term, offset)] in
let assign_by_meet = meet_conjs_opt ret_var_eq_term d in
reset_normal_form assign_by_meet
let assign_by_meet = meet_conjs_opt ret_var_eq_term d.data in
data_to_t assign_by_meet
| _ -> d

let return ctx exp_opt f =
Expand All @@ -194,25 +197,27 @@ struct
let ask = ask_of_man ctx in
match ctx.local with
| `Bot -> `Bot
| `Lifted cc ->
| `Lifted d ->
let t =
begin match lval_opt with
| None ->
cc
d
| Some lval ->
(* forget information about var,
but ignore assignments to values that are not 64 bits *)
try
let size = T.get_element_size_in_bits (typeOfLval lval) in
let lterm = T.of_lval ask lval in
let cc = D.remove_may_equal_terms ask size lterm cc in
begin match desc.special exprs with
let cc = D.remove_may_equal_terms ask size lterm d.data in
let cc = begin match desc.special exprs with
| Malloc _
| Calloc _
| Alloca _ ->
add_block_diseqs cc lterm
| _ -> cc
end
in
data_to_t cc
with T.UnsupportedCilExpression _ ->
C2PODomain.top ()
end
Expand All @@ -224,7 +229,7 @@ struct
else
branch ctx exp true
| _ ->
`Lifted (reset_normal_form t)
`Lifted t

(** First all local variables of the function are duplicated,
then we remember the value of each local variable at the beginning of the function by using the analysis startState.
Expand All @@ -233,13 +238,14 @@ struct
(* add duplicated variables, and set them equal to the original variables *)
match ctx.local with
| `Bot -> [`Bot, `Bot]
| `Lifted cc ->
| `Lifted d ->
let ghost_equality v =
Equal (T.term_of_varinfo (DuplicVar v), T.term_of_varinfo (NormalVar v), Z.zero)
in
let ghost_equalities_for_params = List.map ghost_equality f.sformals in
let equalities_to_add = T.filter_valid_pointers ghost_equalities_for_params in
let state_with_ghosts = meet_conjs_opt equalities_to_add cc in
let state_with_ghosts = meet_conjs_opt equalities_to_add d.data in
let state_with_ghosts = data_to_t state_with_ghosts in
if M.tracing then begin
let dummy_lval = Var (Var.dummy_varinfo (TVoid [])), NoOffset in
let lval = BatOption.default dummy_lval var_opt in
Expand All @@ -250,7 +256,8 @@ struct
let reachable = f.sformals @ f.slocals @ reachable_from_args ctx args in
Var.from_varinfo reachable f.sformals
in
let new_state = D.remove_terms_not_containing_variables reachable_variables state_with_ghosts in
let new_state = D.remove_terms_not_containing_variables reachable_variables state_with_ghosts.data in
let new_state = data_to_t new_state in
if M.tracing then M.trace "c2po-function" "enter2: result: %s\n" (C2PODomain.show new_state);
let new_state = reset_normal_form new_state in
[ctx.local, `Lifted new_state]
Expand All @@ -264,7 +271,7 @@ struct
let combine_env ctx lval_opt expr f args t_context_opt f_d (f_ask: Queries.ask) =
match ctx.local with
| `Bot -> `Bot
| `Lifted cc ->
| `Lifted d ->
let caller_ask = ask_of_man ctx in
(* assign function parameters to duplicated values *)
let arg_assigns = GobList.combine_short f.sformals args in
Expand All @@ -273,30 +280,32 @@ struct
let arg = T.of_cil f_ask arg in
assign_term st caller_ask ghost_var arg var.vtype
in
let state_with_assignments = List.fold_left assign_term cc arg_assigns in
let state_with_assignments = List.fold_left assign_term d arg_assigns in

if M.tracing then M.trace "c2po-function" "combine_env0: state_with_assignments: %s\n" (C2PODomain.show state_with_assignments);

(*remove all variables that were tainted by the function*)
let tainted = f_ask.f (MayBeTainted) in
if M.tracing then M.trace "c2po-tainted" "combine_env1: %a\n" MayBeEqual.AD.pretty tainted;

let local = D.remove_tainted_terms caller_ask tainted state_with_assignments in
let local = D.remove_tainted_terms caller_ask tainted state_with_assignments.data in
let local = data_to_t local in
match D.meet (`Lifted local) f_d with
| `Bot -> `Bot
| `Lifted cc ->
let cc = reset_normal_form @@ remove_out_of_scope_vars cc f in
| `Lifted d ->
let cc = remove_out_of_scope_vars d.data f in
let d = data_to_t cc in
if M.tracing then begin
let dummy_lval = Var (Var.dummy_varinfo (TVoid[])), NoOffset in
let lval = BatOption.default dummy_lval lval_opt in
M.trace "c2po-function" "combine_env2: var_opt: %a; local_state: %s; f_state: %s; meeting everything: %s\n" d_lval lval (D.show ctx.local) (D.show f_d) (C2PODomain.show cc)
M.trace "c2po-function" "combine_env2: var_opt: %a; local_state: %s; f_state: %s; meeting everything: %s\n" d_lval lval (D.show ctx.local) (D.show f_d) (C2PODomain.show d)
end;
`Lifted cc
`Lifted d

let combine_assign ctx var_opt expr f args t_context_opt f_d (f_ask: Queries.ask) =
match ctx.local with
| `Bot -> `Bot
| `Lifted cc ->
| `Lifted d ->
let caller_ask = ask_of_man ctx in
(* assign function parameters to duplicated values *)
let arg_assigns = GobList.combine_short f.sformals args in
Expand All @@ -305,24 +314,24 @@ struct
let arg = T.of_cil f_ask arg in
assign_term st caller_ask ghost_var arg var.vtype
in
let state_with_assignments = List.fold_left assign_term cc arg_assigns in
let state_with_assignments = List.fold_left assign_term d arg_assigns in
match D.meet (`Lifted state_with_assignments) f_d with
| `Bot -> `Bot
| `Lifted cc ->
let cc = match var_opt with
| `Lifted d ->
let d = match var_opt with
| None ->
cc
d
| Some lval ->
let return_type = typeOfLval lval in
let return_var = MayBeEqual.return_var return_type in
let return_var = (Some return_var, Some Z.zero) in
assign_lval cc f_ask lval return_var
assign_lval d f_ask lval return_var
in
if M.tracing then M.trace "c2po-function" "combine_assign1: assigning return value: %s\n" (C2PODomain.show cc);
let cc = remove_out_of_scope_vars cc f in
let cc = reset_normal_form cc in
if M.tracing then M.trace "c2po-function" "combine_assign2: result: %s\n" (C2PODomain.show cc);
`Lifted cc
if M.tracing then M.trace "c2po-function" "combine_assign1: assigning return value: %s\n" (C2PODomain.show d);
let d = remove_out_of_scope_vars d.data f in
let d = data_to_t d in
if M.tracing then M.trace "c2po-function" "combine_assign2: result: %s\n" (C2PODomain.show d);
`Lifted d

let startstate v =
D.top ()
Expand Down
Loading
Loading