Skip to content

Improvements to PHI instruction handling#38

Open
syang-ng wants to merge 99 commits into
ucsb-seclab:phi_as_instructionfrom
syang-ng:phi_as_instruction
Open

Improvements to PHI instruction handling#38
syang-ng wants to merge 99 commits into
ucsb-seclab:phi_as_instructionfrom
syang-ng:phi_as_instruction

Conversation

@syang-ng

@syang-ng syang-ng commented Aug 10, 2025

Copy link
Copy Markdown
Contributor

Motivation

The current implementation of phi_as_instruction tracks the last written register and assigns this register to the variable determined by the PHI instruction. This can cause an issue when there are multiple PHI instructions with overlapping sources — all variables may come from the same register. For example, if vf1b0arg1 uses the most recently written register, it could be assigned to 0xc110xf1b0_0x0, 0xc110xf1b0_0x2, and 0xc110xf1b0_0x3. This could lead to false negatives in the analysis, as these variables are supposed to have different values.

function 0x00000c11(vf1b0arg0, vf1b0arg1, vf1b0arg2, vf1b0arg3, vf1b0arg4, vf1b0arg5, vf1b0arg6) public {
    Begin block 0xf1b0
    prev=[0x406e00xf1b0], succ=[0xc110xf1b0]
    =================================
    0xf1b2: vf1b2(0xc11) = CONST 
    0xf1b5: JUMP vf1b2(0xc11)

    Begin block 0xc110xf1b0
    prev=[0xf1b0], succ=[0xc1f0xf1b0]
    =================================
    0xc110xf1b0_0x0: vc11f1b0_0 = PHI vf1b0arg1, vf1b0c85
    0xc110xf1b0_0x2: vc11f1b0_2 = PHI vf1b0arg1, vf1b0arg2, vf1b0arg3, vf1b0arg4, vf1b0arg5, vf1b0arg6, vf1b0c1e_0, vf1b0c85, vf1b0c12(0x60), vf1b0b79
    0xc110xf1b0_0x3: vc11f1b0_3 = PHI vf1b0arg1, vf1b0arg2, vf1b0arg3, vf1b0arg4, vf1b0arg5, vf1b0arg6, vf1b0c1e_0, vf1b0c85, vf1b0c12(0x60), vf1b0b79
    0xc120xf1b0: vf1b0c12(0x60) = CONST 
    0xc150xf1b0: vf1b0c15(0xc1f) = CONST 
    0xc1b0xf1b0: vf1b0c1b(0x999) = CONST 
    0xc1e0xf1b0: vf1b0c1e_0 = CALLPRIVATE vf1b0c1b(0x999), vc11f1b0_0, vc11f1b0_2, vc11f1b0_3, vf1b0c15(0xc1f)
// ...

Solution

First, I merged the changes from the main branch into phi_as_instruction (but I still use the old parse_blocks in greed/TAC/TAC_parser.py, as the new parsing logic will trigger an error).
Then, in this pull request, I implemented a simple solution to prevent the repeated usage of the same registers by counting their usage and avoiding reuse within the same block.

Specifically, I've added the following code (in greed/TAC/gigahorse_ops.py) to track the number of times a block has been entered in the trace:
image

and then avoid repeated usage of the same registers:
image

Summary: The handling of PHI instructions is a significant challenge. This pull request provides a temporary solution for specific issues I encountered in the smart contracts I tested. A more robust and complete solution may require continued effort :)

robmcl4 and others added 30 commits January 23, 2024 14:58
…rivate

Add a sanity check for CALLPRIVATE argument count match
Signed-off-by: degrigis <degrigis@ucsb.edu>
…olic options for PartialConcreteStorage

Signed-off-by: degrigis <degrigis@ucsb.edu>
Signed-off-by: degrigis <degrigis@ucsb.edu>
@degrigis

Copy link
Copy Markdown
Collaborator

Hey there! Thanks a lot for the contribution, we'll take a look at the PR and get back to you :)

robmcl4 and others added 2 commits August 20, 2025 03:41
bugfix: YicesTermBVZeroExtend not suppported in symbols_referenced_at
@degrigis

Copy link
Copy Markdown
Collaborator

Hey @syang-ng , really appreciate this contrib but we are currently not 100% sure if we want to merge the phi_as_instruction on main 🤔 The reason is that was an experimental feature that @robmcl4 implemented, but didn't have much testing. We talked with him, and he was unsure about how reliable that implementation is, so we are a bit afraid to merge it on main.

While we are disscussing what is the best way to go here, do you mind rebasing that branch phi_as_instruction on main (rather than merging) and then apply on top your edits? That would make it for a little more clear PR :)

Thanks a lot!

@robmcl4

robmcl4 commented Aug 22, 2025

Copy link
Copy Markdown
Collaborator

Can you maybe clarify your use case for requiring phi as an instruction? Ultimately I never found a justification for the change; I didn't observe any situation where it helps our analyses over the current solution (even if the current solution is a bit odd). Can you comment on that?

@syang-ng

syang-ng commented Aug 22, 2025

Copy link
Copy Markdown
Contributor Author

I agree that the current handling of PHI on main works fine in most cases.
The motivation for my change is that in some contracts I analyzed, the current substitution rules for PHI end up treating certain values as equivalent even though they are not, which leads to false negatives in the analysis. I think the code snippet I attached at the beginning illustrates this issue as well.

I like the idea of treating PHI as an instruction in that branch: it explores an alternative way of handling such cases. I am not suggesting that this should be merged into main -- I am simply extending that branch as an experiment to see whether it can help in situations where the current solution falls short. so others may also find that branch useful for addressing some additional problems :)

@ruaronicola

Copy link
Copy Markdown
Collaborator

I agree it would be great to have this merged into the phi_as_instruction branch, since it could be useful to others in the community! As @degrigis mentioned, could you first rebase the branch and then apply your changes on top? A clean, minimal PR would help us review and merge your contribution more quickly. Thanks! :)

@syang-ng syang-ng force-pushed the phi_as_instruction branch from ece7dda to 3a44049 Compare August 23, 2025 01:08
@syang-ng

Copy link
Copy Markdown
Contributor Author

Sure! I updated it as you suggested, @degrigis. Thanks everyone for reviewing -- let me know if there are any issues.

@degrigis

degrigis commented Sep 2, 2025

Copy link
Copy Markdown
Collaborator

@robmcl4 you have a second to fix the conflicts and merge this? :)

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.

9 participants