Skip to content

simplify: implement standard copyprop #418

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.

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

Open
wants to merge 5 commits into
base: main
Choose a base branch
from
Open

simplify: implement standard copyprop #418

wants to merge 5 commits into from

Conversation

ailrst
Copy link
Contributor

@ailrst ailrst commented May 1, 2025

Implements a more standard implementation of flow-insensitive copyprop (disabled) as well as a similar transform targeted specifically at address calculations: for values conforming to a (variable + constant) structure.

By deferring substitution we avoid tracking clobbers so this is >2x faster than the existing 'DSACopyProp', and is more effective at removing redundant dsa copies involved in loops. It is still sufficient to fully propagate through stack address calculations so none of the tests should timeout.

This does not handle propagating flag calculations at all, so that relies entirely on #413

note: translation validation succeeds for this program https://github.com/UQ-PAC/basil-tests/blob/main/src/test/csmith/csmith4/csmith4.c#L3552-L3601

@ailrst ailrst force-pushed the simple-copyprop branch from 91a0ff8 to eedf2ad Compare May 1, 2025 07:34
@ncough
Copy link
Contributor

ncough commented May 5, 2025

Not sure if this is ready to look at, but I took a glance at the simple copyprop implementation. I understand this is intended to work over the DSA form, traversing blocks in a topological order. So, without loops, all uses should be resolved when traversing. But with a loop, could the abstract value for a loop defined variable change after it has been used for some intermediate reasoning? I think the following example may illustrate this, but I haven't run it through.

x = 1;
do {
  y = x;
  if (P x) {
    z = 1;
  } else {
    z = y;
  }
  x = x + 1;
} while (Q x);
return z;

I think this is in DSA form, but maybe I am mistaken. Assuming it is, this can lead to a final state where z -> 1.
Assume z = 1 is seen before z = y. After processing z = 1, the abstract state should be:

z -> 1,
y -> x,
x -> 1,

As every assignment up to this point is fresh. Processing z = y should retain this abstract state, as find(z) = find(y).
The final assignment to x should remap its abstract value to top. Substitution can then incorrectly replace the final operation with return 1;.

Maybe there is some constraint I am missing that prevents the issue. If not, I'd suggest changing this analysis to be flow sensitive. It practically already is, the worklist simply needs to track whether the state changed due to a block and push all successors in this case.

@ailrst
Copy link
Contributor Author

ailrst commented May 5, 2025

Thanks for looking at this, I think this is a legitimate issue and the reason the previous implementation tracks everything used in intermediate reasoning and traverses the abstract state to clobber everything dependent on x when x=x+1 is visited. Making it flow sensitive is definitely more efficient and easier

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants