Skip to content

Aslp generating control flow branches#188

Open
katrinafyi wants to merge 20 commits into
mainfrom
aslp-branches-2
Open

Aslp generating control flow branches#188
katrinafyi wants to merge 20 commits into
mainfrom
aslp-branches-2

Conversation

@katrinafyi

@katrinafyi katrinafyi commented Jun 22, 2026

Copy link
Copy Markdown
Collaborator

ensures a pc increment on all straight-line control-flow paths by construction.

adds a new lib/transforms/aslp/aslp_lexpr.ml file for abstracting the builtin and local variables used by the aslp lifter.

this pr also renames some things, like now using aslp_diamond in place of aslp_state.

let%expect_test "lift: b.eq #1024" =
  let module I = (val Bincaml_ibi.from_generator (Aslp_state.empty_aslp_ids ()))
  in
  let x =
    lift_opcode
      (module I)
      ~address:(Bitvec.zero ~size:64)
      (Bitvec.of_string "0x54002000:bv32")
  in
  print_endline @@ Aslp_state.show_aslp_diamond x;
  [%expect
    {|
    { Aslp_state.blocks = "block_0"
      -> { Aslp_state.assume = None; stmts = []; succs = ["block_1"; "block_2"];
           has_pc_assign = false },
      "block_1"
      -> { Aslp_state.assume = (Some eq($PSTATE_Z, 0x1:bv1));
           stmts = [var BranchTaken:bool := true; $PC:bv64 := 0x400:bv64];
           succs = ["block_3"]; has_pc_assign = true },
      "block_2"
      -> { Aslp_state.assume = (Some boolnot(eq($PSTATE_Z, 0x1:bv1)));
           stmts =
           [($PC:bv64 := bvadd($PC, 0x4:bv32), var BranchTaken:bool := false)];
           succs = ["block_3"]; has_pc_assign = true },
      "block_3"
      -> { Aslp_state.assume = None; stmts = []; succs = []; has_pc_assign = true
           };
      entry = "block_0"; exit = "block_3" }
    |}]

@katrinafyi katrinafyi requested a review from agle as a code owner June 22, 2026 08:46
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.

1 participant