Highest live bit analysis and transform - #220
Open
NambatCat wants to merge 49 commits into
Open
Conversation
added 17 commits
July 9, 2026 13:04
…all) & (Assign og_v := tmp) instructions
… analysis and the highest_live_bit transform files.
NambatCat
marked this pull request as ready for review
July 21, 2026 22:25
katrinafyi
removed their request for review
July 22, 2026 01:27
…o-extend. Made preliminary fix for evaluating call parameters during analysis
This implements the Aslp frontend. It's a bit big.
- all arm variables are added all of the time.
- PC assignments are forwarded into an assign at the merge point, immediately before the nondeterministic goto. is this enough or should we put it right into the assume of the successors?
- todo update bincaml-test with new .address attribute
See tests at bottom half of test/transforms/test_aslp.ml.
Here is an example for `b.lt #0x10`. You can see the propagated PC ITE assignment in the block_3.
```ocaml
proc @sqrt() -> () { }
captures $PC:bv64
[
block %Sqrt_code_4 { .address = 4196316 } [
assume eq(0x4007dc:bv64, $PC);
goto (%block);
];
block %block { .asm = "b.lt #0x10" } [
guard true;
goto (%block_2,%block_1);
];
block %block_1 [
guard boolnot(eq($PSTATE_N, $PSTATE_V));
var BranchTaken:bool := true;
$PC:bv64 := 0x4007ec:bv64;
goto (%block_3);
];
block %block_2 [
guard boolnot(boolnot(eq($PSTATE_N, $PSTATE_V)));
(var BranchTaken:bool := false, $PC:bv64 := 0x4007e0:bv64);
goto (%block_3);
];
block %block_3 [
guard true;
$PC:bv64 := if boolnot(eq($PSTATE_N, $PSTATE_V)) then 0x4007ec:bv64 else 0x4007e0:bv64;
assert boolor(eq(0x4007fc:bv64, $PC), eq(0x4007e0:bv64, $PC));
goto (%Sqrt_code_3,%Sqrt_code);
];
block %Sqrt_code [ assume eq(0x4007e0:bv64, $PC); goto (%ret); ];
block %Sqrt_code_3 [ assume eq(0x4007fc:bv64, $PC); goto (%ret); ];
block %ret [ return; ]
];
```
Closes #194
Closes #198
Closes #199
Just some maintenance of the flake to keep the package and devshell working and up to date. It was missing the examples submodule which was causing me some headache getting it to pass checks! * Nix maintenance * undoing a debugging change * Documented why containers.nix is necessary
To be honest, it is debatable whether this is easier to read than the old code. I think it is slightly, because you don't need do so much bookkeeping of directions. It also makes the tree structure more explicit and adds a scan function. * use scan and duplicate on CCKTrees * touch up move * avoid polymorphic variant casting
headline changes: - gtirb loader now attaches address to every intrinsic, and the transform looks for this. the transform now works one statement at a time. - to help this, i've added some helper methods in Procedure for block control flow. i want advice on whether they look good. - also added a "micro-pass" to compute stmt address from block .address to avoid needing address on every statement in tests, which would've been tedious. this has to be run manually if it's wanted other new features: - exceptions while lifting now just lead to a `.error` attribute on the intrinsic, rather than crashing. transforming continues with the next valid opcode. this can be seen in a test case. other output changes: - a final combined PC assignment is now emitted to the last block in the ASLp output (previously, it was just recorded internally but not used). let me know if this is enough for future guard cleanup, or whether it needs to be forwarded even more. - guard trues are omitted. - PC ITEs which are the same on both side are simplified to avoid the ITE. - only used ARM global variables are generated. however: - transforming one statement at a time leads to overall `n^2` in the number of intrinsics, because we make new block stmt vectors after each intermediate intrinsic and it's cloned each time. i don't know how to improve this without introducing a new temporary block stmt list representation or something similarly hacky. edit: I have an idea now. next pr.
* SVA? * flip test order because of hashing nonsense * funny option monad * fixes changes * Don't throw on invalid params * ds cells * gen constraints * mappable exprs * Start making ds graph * yap * test thing * untested unfinished node list * shift * collapse * wrapped intervals -> top * remove warning * other warning * doc comments * unify pointees * Make nodes * Untested graphviz code * It works?! * fixes * create cells with correct intervals * distinct load bases * fix infinite loop * Node record * flags * interproc ids * node uf * interval to cell finding * incomplete bu phase * Copy nodes * Maybe working bu phase maybe??? no sccs though * Slightly nicer dot printing * Remove call preserve vars * Copy per call instead of per param * Assign symbolic bases to copied nodes * AAAAAAAAaa i have NO idea if this works ?????????????????? * Remove debug stuff * some proptests (incomplete) * fix a terrible bug HOW WAS THAT THERE (proptests are NOT sufficient) * oops reenable bu * Don't clear stack flag if node is merged already * BU phase preserve unified pointees * Partial formal impl of dsgraph * formal unification pass * formal copy * aslkjgdhsdkjfhsadlkjghdslkfdg * A little bit of cleaning to make testing possible or something * Some tests (i want to go home) * Formal old-to-new mapping * IT'S ALL BROKEN * Fix joining intervals oops * Check cell widths (everything explodes) * Fix joining * fix unify * copy works? * a * Fix stuff * patch messed up mutability * fix bu stuff idk * Probably wrong recursion implementation * Fix unifying within-node recursive cells * fix big bu but it still looks broken * cleanup stuff * remove sig * Proptest nodes instead of singular cells * remove broken test, and add note * remove old slow redundant test * TD phase! it's really bad * Don't copy nodes across calls if callee cell doesn't exist * merge main i think? * Permit non unique formal outs * fix tests after merge * Document the transform * SVA global ranges * find_cell * correct pass requirements * flag docs * named argument constraint map * clarify sb comment * node_id instead of id * remove pointfree inlines * Map.update * Move everything into separate files * Remove unnecessary rec labels * Get rid of more recursion oops * deriving show on stm commands * Move sva iteration logic outside the dsgraph * uniq callees --------- Co-authored-by: JTrenerry <105094182+JTrenerry@users.noreply.github.com> Co-authored-by: am <a.michael1@uq.edu.au>
Implements the acyclic cfa reduction transform from some old snippet of nicks thesis. Basically just flattens an acyclic, deterministic procedure in a single block. Cheats a bit because we already have an SSA transform so we can skip some of the algorithm, yay! * Rebased * undoing a debugging change * CFA Reduction Skeleton * Reduction is working * Clean up the graph to prevent errors * Test case * formatting * cram promotion * Cleaned up a comment :) * simplify removed * filter out guards * cleanup * Some more documenting * formatter... * rebased
* Use CCVector in CFA reduction to avoid quadratic Follow-up to https://www.github.com/agle/bincaml/pull/214#pullrequestreview-4750940364 I know I said it didn't urgently need fixing, but it's just such low hanging fruit and it avoids the future frustration - however small. In the transform, we use `modify_block` after `fresh_block` to avoid casting the vector into a list and then back to a vector. * bring back fold_blocks_topo_fwd but use CCVector as accumulator a bit less imperative.
… to remove unnecessary extracts.
…ond pass to remove unnecessary extracts." This reverts commit cb55273.
This reverts commit 6769dda.
This reverts commit d962a62.
This reverts commit db3a69b.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Highest Live Bit analysis and transform.
This project contains a process for transforming a program that contains
mbit variables where the highnbits are not live tom-nbit variableslib/analysis/highest_live_bit_simple.ml
This file uses the IDESSI solver to perform an interprocedural analysis for the least significant live bit of a variable. It only examines the inner-most expression of a nested expression that operates directly on a variable, and determines the highest live bit of said variable.
lib/transforms/highest_live_bit.ml
This file performs a transform on a program using the information from highest_live_bit_simple. First, it changes the size of a variable, then either wraps an extend or an extract around it, depending on where in a statement it is located. It then maps over the expressions of a statement and removes redundant extracts and extends. Further details can be found in the docstrings of the file.
var R0_1:bv64 := zero_extend(32, bvadd(1:bv32, extract(32, 0, R0_2:bv64)));var v:bv32 := extract(32, 0, R0_1:bv64);->
var R0_1:bv32 := extract(32, 0, zero_extend(32, bvadd(1:bv32, extract(32, 0, zero_extend(32, R0_2:bv32)))));var v:bv32 := extract(32, 0, zero_extend(32, R0_1:bv32));->
var R0_1:bv32 := bvadd(1:bv32, R0_2:bv32);var v:bv32 := R0_1:bv32;lib/analysis/highest_live_bit_complex.ml
This file contains a more complicated analysis that attempts to examine the least significant live bit of a variable across an entire expression, which may be very large. However, it does not work for all edge cases, and is deprecated. It is left in on the chance that the more complex analysis on entire nested expressions will be visited in the future.
lib/analysis/dune
The simple and complex ml files were added to the dune builder, so that they can compile with
dune buildTODO:
KNOWN ISSUES:
b:bv64 ; ... := call (in=b:bv64); ... extract(32, 0, b:bv64)will output 31 for b instead of 63Contributers:
Namson Phan