Skip to content

Commit

Permalink
Slightly more aggressive elimination of temporaries
Browse files Browse the repository at this point in the history
This fixes AeneasVerif/eurydice#128 -- but
this uncovered a shortcoming that ought to be fixed.
  • Loading branch information
msprotz committed Jan 10, 2025
1 parent e111ce5 commit f6b3233
Showing 1 changed file with 11 additions and 5 deletions.
16 changes: 11 additions & 5 deletions lib/Simplify.ml
Original file line number Diff line number Diff line change
Expand Up @@ -132,11 +132,17 @@ let use_mark_to_inline_temporaries = object (self)
b.node.name = "scrut" ||
Structs.should_rewrite b.typ = NoCopies
) &&
v = AtMost 1 && (
is_readonly_c_expression e1 &&
safe_readonly_use e2 ||
safe_pure_use e2
) (* || is_readonly_and_variable_free_c_expression e1 && b.node.mut *)
(v = AtMost 1 && (
is_readonly_c_expression e1 &&
safe_readonly_use e2 ||
safe_pure_use e2
) ||
is_readonly_and_variable_free_c_expression e1 && not b.node.mut)
(* b.node.mut is an approximation of "the address of this variable is taken"
-- TODO this is somewhat incompatible with the phase that changes size-1
arrays into variables who address is taken, so we should also check beore
inlining that the address of this variable is not taken... this is
starting to be quite an expensive check! *)
then
(* Don't drop a potentially useful comment into the ether *)
let e1 = { e1 with meta = e1.meta @ b.meta } in
Expand Down

0 comments on commit f6b3233

Please sign in to comment.