diff --git a/examples b/examples index 339b7c48..bd28c05a 160000 --- a/examples +++ b/examples @@ -1 +1 @@ -Subproject commit 339b7c483383d3c73af612dc5e612a4d4252b599 +Subproject commit bd28c05ab1b06318f4a19c3a65061780f3d59b92 diff --git a/lib/gtirb/gfir_to_bincaml.ml b/lib/gtirb/gfir_to_bincaml.ml index e08a1b56..8b7b2144 100644 --- a/lib/gtirb/gfir_to_bincaml.ml +++ b/lib/gtirb/gfir_to_bincaml.ml @@ -354,5 +354,6 @@ let module_to_ir_prog ir_cfg (m : Module.t) = (fun _ proc prog -> temp_proc_to_ir_proc all_blocks prog proc) procs prog in + let prog = Lang.Spec_modifies.set_modsets prog in let entry_proc = UUIDMap.find entry_proc procs in Lang.Program.set_entry_proc entry_proc.id prog diff --git a/lib/invariants.ml b/lib/invariants.ml index b52d6ea2..a70f6760 100644 --- a/lib/invariants.ml +++ b/lib/invariants.ml @@ -16,6 +16,7 @@ type t = | Params | LambdaLift | MemoryEncoding + | GTIRB_ARM | ReducibleLoops (** All loops are reducible. That is, there are no {i irreducible} loops. *) @@ -23,6 +24,7 @@ type t = let read s = match s with + | "GTIRB_ARM" -> GTIRB_ARM | "SSA" -> SSA | "DSA" -> DSA | "NoPhis" -> NoPhis diff --git a/lib/lang/spec_modifies.ml b/lib/lang/spec_modifies.ml index 9b2b324d..191a84cb 100644 --- a/lib/lang/spec_modifies.ml +++ b/lib/lang/spec_modifies.ml @@ -76,14 +76,17 @@ let set_modsets ?(add_only = false) prog = |> Iter.flat_map Expr.BasilExpr.free_vars_iter |> Iter.filter Var.is_global |> VarSet.of_iter in + let name_compare = fun a b -> String.compare (Var.name a) (Var.name b) in let captures_globs = - List.filter (not % Var.is_constant) + List.sort name_compare + @@ List.filter (not % Var.is_constant) @@ VarSet.elements @@ VarSet.union vs @@ VarSet.union exist_captures @@ VarSet.union read written in let modifies_globs = - VarSet.elements @@ VarSet.union exist_modifies written + List.sort name_compare @@ VarSet.elements + @@ VarSet.union exist_modifies written in let spec : (Var.t, Program.e) Procedure.proc_spec = Procedure.specification p diff --git a/lib/loadir.ml b/lib/loadir.ml index 2957c3ba..a831315d 100644 --- a/lib/loadir.ml +++ b/lib/loadir.ml @@ -1523,7 +1523,7 @@ let concrete_prog_ast_of_channel ?input ?filename c = let lexbuf = Lexing.from_channel ~with_positions:true c in filename |> Option.iter (fun f -> Lexing.set_filename lexbuf f); try ParBasilIR.pModuleT LexBasilIR.token lexbuf - with ParBasilIR.Error -> raise (ILBParseError { input; lexbuf }) + with _ -> raise (ILBParseError { input; lexbuf }) let concrete_prog_ast_of_string ?input ?filename str = let open BasilIR in diff --git a/lib/passes.ml b/lib/passes.ml index e753dd81..87132f93 100644 --- a/lib/passes.ml +++ b/lib/passes.ml @@ -106,6 +106,15 @@ module PassManager = struct invariants = Invariants.presupposes [ SSA ]; } + let aslp_semantics = + { + name = "aslp-semantics"; + apply = Prog Transforms.Aslp.transform_program; + doc = "Add ASLP instsruction semantics after gtirb"; + invariants = + Invariants.presupposes [ GTIRB_ARM ] ~invalidates:[ GTIRB_ARM ]; + } + let cse_elim = { name = "cse-elim"; @@ -442,6 +451,7 @@ module PassManager = struct let passes = [ + aslp_semantics; lift_intrinsics_aarch64; hm_elaborate; chop_unreachable; diff --git a/lib/script.ml b/lib/script.ml index 6c5ed5cb..c4b91ceb 100644 --- a/lib/script.ml +++ b/lib/script.ml @@ -315,6 +315,7 @@ let load_gtirb st fname = let p = match p with | Ok e -> + let e = Program.set_attrib Invariants.(to_attrib [ GTIRB_ARM ]) e in Loader.Loadir.( Some { prog = e; curr_proc = None; params_order = Hashtbl.create 0 }) diff --git a/lib/transforms/aslp/aslp.ml b/lib/transforms/aslp/aslp.ml index f7b7e4d0..f44703cf 100644 --- a/lib/transforms/aslp/aslp.ml +++ b/lib/transforms/aslp/aslp.ml @@ -73,11 +73,23 @@ let stmt_of_aarch64_intrin ?error : let args = Expr.BasilExpr.[ bvconst opcode; bvconst address ] in Stmt.Instr_IntrinCall { attrib; lhs = []; name = Aarch64Eval; args } -(** Returns the Bincaml global variable representing heap memory. *) +(** Returns the Bincaml global variable representing heap memory, declaring it + if it does not exist. *) let aarch64_mem_of_prog prog = Program.get_decl_by_name "$mem" prog |> function - | Some (Variable { binding }) -> binding - | _ -> failwith "aarch64_mem_of_prog: no $mem found" + | Some (Variable { binding }) -> (prog, binding) + | None -> + let mem = + Var.create "$mem" ~scope:Var.GlobalVarShared + Types.(Map (Bitvector 64, Bitvector 8)) + in + + let prog = + let attrib = Attrib.empty and classification = None in + Program.add_decl prog + (Program.Variable { binding = mem; attrib; classification }) + in + (prog, mem) (** {1 Main Bincaml IR transformation functions} *) @@ -170,13 +182,13 @@ let add_aarch64_global_declarations ?(add_all = false) prog = procedures within the given program. Also inserts global variable declarations for the architectural variables, - if not already present. *) + if not already present. Assumes it is running immediately after gtirb. *) let transform_program prog = - let memory = aarch64_mem_of_prog prog in - + let prog, memory = aarch64_mem_of_prog prog in prog |> Program.map_procedures (fun _ -> transform_procedure ~memory) |> add_aarch64_global_declarations + |> Spec_modifies.set_modsets ~add_only:false (** {1 Supplementary transformation} *) diff --git a/lib/transforms/aslp/aslp_state.ml b/lib/transforms/aslp/aslp_state.ml index 89d3c689..9c218cb9 100644 --- a/lib/transforms/aslp/aslp_state.ml +++ b/lib/transforms/aslp/aslp_state.ml @@ -102,7 +102,7 @@ let empty_aslp_ids () = This will ensure that ASLp's local variable and block names do not clash with existing names. *) let aslp_ids_from_generators ~local_ids = - let local_id = ID.fresh ~name:"var" local_ids %> ID.name in + let local_id = ID.fresh ~name:"lv" local_ids %> ID.name in { local_id } (** {1 State manipulation functions} *) diff --git a/lib/transforms/aslp/bincaml_ibi_make.ml b/lib/transforms/aslp/bincaml_ibi_make.ml index 5291cafc..5622b420 100644 --- a/lib/transforms/aslp/bincaml_ibi_make.ml +++ b/lib/transforms/aslp/bincaml_ibi_make.ml @@ -297,25 +297,31 @@ struct = fun _ -> failwith "f_gen_Elem_set" - (** [f_gen_Mem_set size address size acctype value] *) + (** [(f_gen_Mem_set size address size acctype value) : unit] emits an + instruction which stores value to memory. Value must have bit width equal + to size (bytes) in bits. *) let f_gen_Mem_set : bigint -> expr -> expr -> expr -> expr -> unit = fun size addr _ _acctype value -> - let addr = Stmt.Addr { addr; size = Z.to_int size; endian = `Little } + let size = 8 * Z.to_int size in + let addr = Stmt.Addr { addr; size; endian = `Little } and mem = S.bincaml_memory_var () in bincaml_internal_emit (Stmt.Instr_Store { attrib = Attrib.empty; lhs = mem; rhs = mem; value; addr }) - (** [f_gen_Mem_read size address size acctype value] *) + (** [let lhs = f_gen_Mem_read size address size acctype value] emits a read + instruction reading a bitvector [size] (bytes) from the memory variable, + assigning it to variable [lhs]. Returns [lhs] as an expression). *) let f_gen_Mem_read : bigint -> expr -> expr -> expr -> expr = fun size addr _ _acctype -> - let addr = Stmt.Addr { addr; size = Z.to_int size; endian = `Little } + let size = 8 * Z.to_int size in + let addr = Stmt.Addr { addr; size; endian = `Little } and mem = S.bincaml_memory_var () in let name = !bincaml_lifter_state.generator.local_id () in - let rhs = Var.create name (Types.bv (Z.to_int size)) in + let lhs = Var.create name (Types.bv size) in bincaml_internal_emit - (Stmt.Instr_Load { attrib = Attrib.empty; lhs = mem; rhs; addr }); - Expr.BasilExpr.rvar rhs + (Stmt.Instr_Load { attrib = Attrib.empty; lhs; rhs = mem; addr }); + Expr.BasilExpr.rvar lhs let f_AtomicStart : unit -> unit = fun _ -> failwith "f_AtomicStart" let f_AtomicEnd : unit -> unit = fun _ -> failwith "f_AtomicEnd" @@ -375,6 +381,16 @@ struct let f_gen_slt_bits : bigint -> expr -> expr -> expr = fun _ a b -> Expr.BasilExpr.binexp ~op:`BVSLT a b + let make_widths_equal a b = + let width a = + Expr.BasilExpr.type_of a |> Types.bit_width + |> Option.get_exn_or "expected bv argument to operator" + in + let wb = width b and wa = width a in + if wa = wb then b + else if wa > wb then Expr.BasilExpr.zero_extend ~n_prefix_bits:(wa - wb) b + else failwith "expected second shift argument to be equal or smaller" + let f_gen_mul_bits : bigint -> expr -> expr -> expr = fun _ a b -> Expr.BasilExpr.applyintrin ~op:`BVMUL [ a; b ] @@ -382,13 +398,13 @@ struct fun _ _ a b -> Expr.BasilExpr.applyintrin ~op:`BVConcat [ a; b ] let f_gen_lsr_bits : bigint -> bigint -> expr -> expr -> expr = - fun _ _ a b -> Expr.BasilExpr.binexp ~op:`BVLSHR a b + fun _ _ a b -> Expr.BasilExpr.binexp ~op:`BVLSHR a (make_widths_equal a b) let f_gen_lsl_bits : bigint -> bigint -> expr -> expr -> expr = - fun _ _ a b -> Expr.BasilExpr.binexp ~op:`BVSHL a b + fun _ _ a b -> Expr.BasilExpr.binexp ~op:`BVSHL a (make_widths_equal a b) let f_gen_asr_bits : bigint -> bigint -> expr -> expr -> expr = - fun _ _ a b -> Expr.BasilExpr.binexp ~op:`BVASHR a b + fun _ _ a b -> Expr.BasilExpr.binexp ~op:`BVASHR a (make_widths_equal a b) (** [f_gen_replicate_bits operand_width num_replications operand num_replications] *) @@ -408,7 +424,7 @@ struct (** [f_gen_slice x lo wd] *) let f_gen_slice : expr -> bigint -> bigint -> expr = fun x lo_incl wd -> - let hi_excl = Z.(to_int (lo_incl - wd)) and lo_incl = Z.to_int lo_incl in + let hi_excl = Z.(to_int (lo_incl + wd)) and lo_incl = Z.to_int lo_incl in Expr.BasilExpr.extract ~lo_incl ~hi_excl x (* {1 Floating point intrinsics} *) diff --git a/test/cram/basicssa.t b/test/cram/basicssa.t index d61bf608..621697c0 100644 --- a/test/cram/basicssa.t +++ b/test/cram/basicssa.t @@ -52,10 +52,10 @@ Run on basic irreducible loop example var $ZF:bv1; proc @main_1876() -> () { .address = 1876; .name = "main"; .returnBlock = "main_basil_return_1" } - modifies $mem:(bv64->bv8), $stack:(bv64->bv8), $CF:bv1, $NF:bv1, $R0:bv64, - $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1 - captures $mem:(bv64->bv8), $stack:(bv64->bv8), $CF:bv1, $NF:bv1, $R0:bv64, - $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1 + modifies $CF:bv1, $NF:bv1, $R0:bv64, $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, + $VF:bv1, $ZF:bv1, $mem:(bv64->bv8), $stack:(bv64->bv8) + captures $CF:bv1, $NF:bv1, $R0:bv64, $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, + $VF:bv1, $ZF:bv1, $mem:(bv64->bv8), $stack:(bv64->bv8) [ block %main_entry { .address = 1876 } [ @@ -158,10 +158,10 @@ Run on basic irreducible loop example block %main_basil_return_1 [ return; ] ]; proc @puts_1584() -> () { .address = 1584; .name = "puts" } - modifies $mem:(bv64->bv8), $stack:(bv64->bv8), $CF:bv1, $NF:bv1, $R0:bv64, - $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1 - captures $mem:(bv64->bv8), $stack:(bv64->bv8), $CF:bv1, $NF:bv1, $R0:bv64, - $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1 + modifies $CF:bv1, $NF:bv1, $R0:bv64, $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, + $VF:bv1, $ZF:bv1, $mem:(bv64->bv8), $stack:(bv64->bv8) + captures $CF:bv1, $NF:bv1, $R0:bv64, $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, + $VF:bv1, $ZF:bv1, $mem:(bv64->bv8), $stack:(bv64->bv8) ; prog entry @main_1876; diff --git a/test/cram/gtirb.t b/test/cram/gtirb.t index 804c883b..b6df52c2 100644 --- a/test/cram/gtirb.t +++ b/test/cram/gtirb.t @@ -1,15 +1,33 @@ $ cat << EOF | bincaml script - > (load-gtirb "../../examples/gtirb/binsearch_sqrt.gtirb") > (dump-il gtirb-output.il) - > (dump-il) > (load-il gtirb-output.il) > (dump-il "dumped.il") + > (run-transforms aslp-semantics) + > (dump-il "semantics.il") + > (log-level debug) + > (run-transforms type-check check-read-uninitialised-withlocals) + > (load-il "semantics.il") > EOF (load-gtirb ../../examples/gtirb/binsearch_sqrt.gtirb) (dump-il gtirb-output.il) - (dump-il) + (load-il gtirb-output.il) + (dump-il dumped.il) + (run-transforms aslp-semantics) + bincaml: [WARNING] Invariants not satisfied during 'aslp-semantics'. Needs [GTIRB_ARM] but only have []. + (dump-il semantics.il) + (log-level debug) + (run-transforms type-check check-read-uninitialised-withlocals) + bincaml: [DEBUG] Starting type-check + bincaml: [DEBUG] Starting check-read-uninitialised-withlocals + (load-il semantics.il) + $ diff gtirb-output.il dumped.il + + $ cat semantics.il var $PC:bv64; proc @_fini() -> () { } + modifies $PC:bv64, $R29:bv64, $R30:bv64, $SP:bv64, $mem:(bv64->bv8) + captures $PC:bv64, $R29:bv64, $R30:bv64, $SP:bv64, $mem:(bv64->bv8) requires boolor(eq(0x400828:bv64, $PC)) [ @@ -18,9 +36,28 @@ .target = "internal:wK9NYU4TTr+D8gXPiCk+7w"; .type = "Type_Fallthrough" } ] } [ assume eq(0x400828:bv64, $PC); - call @_aarch64_eval(0xd503201f:bv32, 0x400828:bv64) { .asm = "nop " }; - call @_aarch64_eval(0xa9bf7bfd:bv32, 0x40082c:bv64) { .asm = "stp x29, x30, [sp, #-0x10]!" }; - call @_aarch64_eval(0x910003fd:bv32, 0x400830:bv64) { .asm = "mov x29, sp" }; + call @_aarch64_eval(0xd503201f:bv32, 0x400828:bv64) { .asm = "nop "; + .error = "Failure(\"unsupported\")" }; + goto (%block); + ]; + block %block { .asm = "stp x29, x30, [sp, #-0x10]!" } [ + var lv:bv64 := 0x0:bv64; + var lv:bv64 := $SP; + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd($SP, + 0xfffffffffffffff0:bv64) $R29 64; + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd(bvadd($SP, + 0xfffffffffffffff0:bv64), 0x8:bv64) $R30 64; + $SP:bv64 := bvadd(lv:bv64, 0xfffffffffffffff0:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x400830:bv64); + goto (%block_1); + ]; + block %block_1 { .asm = "mov x29, sp" } [ + var lv_1:bv64 := 0x0:bv64; + $R29:bv64 := bvadd($SP, 0x0:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x400834:bv64); + goto (%_fini_code_2); + ]; + block %_fini_code_2 [ assert boolor(eq(0x400834:bv64, $PC)); goto (%_fini_code_1); ]; @@ -29,14 +66,38 @@ .succ = [ { .conditional = "false"; .direct = "false"; .target = "proxy:P8unZs8jR1SVxJeeo8n1sg"; .type = "Type_Return" } ] } [ assume eq(0x400834:bv64, $PC); - call @_aarch64_eval(0xa8c17bfd:bv32, 0x400834:bv64) { .asm = "ldp x29, x30, [sp], #0x10" }; - call @_aarch64_eval(0xd65f03c0:bv32, 0x400838:bv64) { .asm = "ret " }; - assert boolor(); - goto (%ret_1); + goto (%block_2); + ]; + block %block_2 { .asm = "ldp x29, x30, [sp], #0x10" } [ + var lv_2:bv64 := 0x0:bv64; + var lv_2:bv64 := $SP; + var lv_3:bv64 := 0x0:bv64; + var lv_4:bv64 := load le $mem:(bv64->bv8) $SP 64; + var lv_3:bv64 := lv_4:bv64; + var lv_5:bv64 := 0x0:bv64; + var lv_6:bv64 := load le $mem:(bv64->bv8) bvadd($SP, 0x8:bv64) 64; + var lv_5:bv64 := lv_6:bv64; + $R29:bv64 := lv_3:bv64; + $R30:bv64 := lv_5:bv64; + $SP:bv64 := bvadd(lv_2:bv64, 0x10:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x400838:bv64); + goto (%block_3); ]; + block %block_3 { .asm = "ret " } [ + var lv_7:bv64 := 0x0:bv64; + var BTypeNext:bv2 := 0x0:bv2; + var BranchTaken:bool := true; + $PC:bv64 := $R30; + goto (%_fini_code_3); + ]; + block %_fini_code_3 [ assert boolor(); goto (%ret_1); ]; block %ret_1 [ return; ] ]; proc @_init() -> () { } + modifies $PC:bv64, $R0:bv64, $R16:bv64, $R17:bv64, $R29:bv64, $R30:bv64, + $SP:bv64, $mem:(bv64->bv8) + captures $PC:bv64, $R0:bv64, $R16:bv64, $R17:bv64, $R29:bv64, $R30:bv64, + $SP:bv64, $mem:(bv64->bv8) requires boolor(eq(0x400600:bv64, $PC)) [ @@ -44,10 +105,34 @@ .succ = [ { .address = 4196036; .conditional = "false"; .direct = "true"; .target = "stmts:Djx7L34DQzuSXaBFEj/bpQ"; .type = "Type_Call" } ] } [ assume eq(0x400600:bv64, $PC); - call @_aarch64_eval(0xd503201f:bv32, 0x400600:bv64) { .asm = "nop " }; - call @_aarch64_eval(0xa9bf7bfd:bv32, 0x400604:bv64) { .asm = "stp x29, x30, [sp, #-0x10]!" }; - call @_aarch64_eval(0x910003fd:bv32, 0x400608:bv64) { .asm = "mov x29, sp" }; - call @_aarch64_eval(0x9400002e:bv32, 0x40060c:bv64) { .asm = "bl #0xb8" }; + call @_aarch64_eval(0xd503201f:bv32, 0x400600:bv64) { .asm = "nop "; + .error = "Failure(\"unsupported\")" }; + goto (%block); + ]; + block %block { .asm = "stp x29, x30, [sp, #-0x10]!" } [ + var lv:bv64 := 0x0:bv64; + var lv:bv64 := $SP; + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd($SP, + 0xfffffffffffffff0:bv64) $R29 64; + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd(bvadd($SP, + 0xfffffffffffffff0:bv64), 0x8:bv64) $R30 64; + $SP:bv64 := bvadd(lv:bv64, 0xfffffffffffffff0:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x400608:bv64); + goto (%block_1); + ]; + block %block_1 { .asm = "mov x29, sp" } [ + var lv_1:bv64 := 0x0:bv64; + $R29:bv64 := bvadd($SP, 0x0:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x40060c:bv64); + goto (%block_2); + ]; + block %block_2 { .asm = "bl #0xb8" } [ + $R30:bv64 := 0x400610:bv64; + var BranchTaken:bool := true; + $PC:bv64 := 0x4006c4:bv64; + goto (%_init_code_2); + ]; + block %_init_code_2 [ assert boolor(eq(0x4006c4:bv64, $PC)); goto (%_init_ext); ]; @@ -62,14 +147,38 @@ .succ = [ { .conditional = "false"; .direct = "false"; .target = "proxy:P8unZs8jR1SVxJeeo8n1sg"; .type = "Type_Return" } ] } [ assume eq(0x400610:bv64, $PC); - call @_aarch64_eval(0xa8c17bfd:bv32, 0x400610:bv64) { .asm = "ldp x29, x30, [sp], #0x10" }; - call @_aarch64_eval(0xd65f03c0:bv32, 0x400614:bv64) { .asm = "ret " }; - assert boolor(); - goto (%ret_1); + goto (%block_3); ]; + block %block_3 { .asm = "ldp x29, x30, [sp], #0x10" } [ + var lv_2:bv64 := 0x0:bv64; + var lv_2:bv64 := $SP; + var lv_3:bv64 := 0x0:bv64; + var lv_4:bv64 := load le $mem:(bv64->bv8) $SP 64; + var lv_3:bv64 := lv_4:bv64; + var lv_5:bv64 := 0x0:bv64; + var lv_6:bv64 := load le $mem:(bv64->bv8) bvadd($SP, 0x8:bv64) 64; + var lv_5:bv64 := lv_6:bv64; + $R29:bv64 := lv_3:bv64; + $R30:bv64 := lv_5:bv64; + $SP:bv64 := bvadd(lv_2:bv64, 0x10:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x400614:bv64); + goto (%block_4); + ]; + block %block_4 { .asm = "ret " } [ + var lv_7:bv64 := 0x0:bv64; + var BTypeNext:bv2 := 0x0:bv2; + var BranchTaken:bool := true; + $PC:bv64 := $R30; + goto (%_init_code_3); + ]; + block %_init_code_3 [ assert boolor(); goto (%ret_1); ]; block %ret_1 [ return; ] ]; proc @__do_global_dtors_aux() -> () { } + modifies $PC:bv64, $R0:bv64, $R1:bv64, $R16:bv64, $R19:bv64, $R29:bv64, + $R30:bv64, $SP:bv64, $mem:(bv64->bv8) + captures $PC:bv64, $PSTATE_Z:bv1, $R0:bv64, $R1:bv64, $R16:bv64, $R19:bv64, + $R29:bv64, $R30:bv64, $SP:bv64, $mem:(bv64->bv8) requires boolor(eq(0x40074c:bv64, $PC)) [ @@ -81,12 +190,65 @@ { .address = 4196208; .conditional = "true"; .direct = "true"; .target = "internal:SFN4dpBgSO2bPUu0fyDluw"; .type = "Type_Branch" } ] } [ assume eq(0x40074c:bv64, $PC); - call @_aarch64_eval(0xa9be7bfd:bv32, 0x40074c:bv64) { .asm = "stp x29, x30, [sp, #-0x20]!" }; - call @_aarch64_eval(0x910003fd:bv32, 0x400750:bv64) { .asm = "mov x29, sp" }; - call @_aarch64_eval(0xf9000bf3:bv32, 0x400754:bv64) { .asm = "str x19, [sp, #0x10]" }; - call @_aarch64_eval(0x90000113:bv32, 0x400758:bv64) { .asm = "adrp x19, #0x20000" }; - call @_aarch64_eval(0x3940a260:bv32, 0x40075c:bv64) { .asm = "ldrb w0, [x19, #0x28]" }; - call @_aarch64_eval(0x37000080:bv32, 0x400760:bv64) { .asm = "tbnz w0, #0, #0x10" }; + goto (%block); + ]; + block %block { .asm = "stp x29, x30, [sp, #-0x20]!" } [ + var lv:bv64 := 0x0:bv64; + var lv:bv64 := $SP; + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd($SP, + 0xffffffffffffffe0:bv64) $R29 64; + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd(bvadd($SP, + 0xffffffffffffffe0:bv64), 0x8:bv64) $R30 64; + $SP:bv64 := bvadd(lv:bv64, 0xffffffffffffffe0:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x400750:bv64); + goto (%block_1); + ]; + block %block_1 { .asm = "mov x29, sp" } [ + var lv_1:bv64 := 0x0:bv64; + $R29:bv64 := bvadd($SP, 0x0:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x400754:bv64); + goto (%block_2); + ]; + block %block_2 { .asm = "str x19, [sp, #0x10]" } [ + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd($SP, 0x10:bv64) $R19 64; + (var BranchTaken:bool := false, $PC:bv64 := 0x400758:bv64); + goto (%block_3); + ]; + block %block_3 { .asm = "adrp x19, #0x20000" } [ + $R19:bv64 := 0x420000:bv64; + (var BranchTaken:bool := false, $PC:bv64 := 0x40075c:bv64); + goto (%block_4); + ]; + block %block_4 { .asm = "ldrb w0, [x19, #0x28]" } [ + var lv_2:bv64 := 0x0:bv64; + var lv_2:bv64 := $R19; + var lv_3:bv8 := 0x0:bv8; + var lv_4:bv8 := load le $mem:(bv64->bv8) bvadd(lv_2:bv64, 0x28:bv64) 8; + var lv_3:bv8 := lv_4:bv8; + $R0:bv64 := zero_extend(32, zero_extend(24, lv_3:bv8)); + (var BranchTaken:bool := false, $PC:bv64 := 0x400760:bv64); + goto (%block_5); + ]; + block %block_5 { .asm = "tbnz w0, #0, #0x10" } [ goto (%block_7,%block_6); ]; + block %block_6 [ + assume eq(extract(1,0, extract(1,0, bvlshr(extract(32,0, $R0), + zero_extend(20, 0x0:bv12)))), 0x1:bv1); + var BranchTaken:bool := true; + $PC:bv64 := 0x400770:bv64; + goto (%block_8); + ]; + block %block_7 [ + assume boolnot(eq(extract(1,0, extract(1,0, bvlshr(extract(32,0, $R0), + zero_extend(20, 0x0:bv12)))), 0x1:bv1)); + (var BranchTaken:bool := false, $PC:bv64 := 0x400764:bv64); + goto (%block_8); + ]; + block %block_8 [ + $PC:bv64 := if eq(extract(1,0, extract(1,0, bvlshr(extract(32,0, $R0), + zero_extend(20, 0x0:bv12)))), 0x1:bv1) then 0x400770:bv64 else 0x400764:bv64; + goto (%__do_global_dtors_aux_code_4); + ]; + block %__do_global_dtors_aux_code_4 [ assert boolor(eq(0x400764:bv64, $PC), eq(0x400770:bv64, $PC)); goto (%__do_global_dtors_aux_code_3,%__do_global_dtors_aux_code_1); ]; @@ -95,19 +257,54 @@ .succ = [ { .conditional = "false"; .direct = "false"; .target = "proxy:P8unZs8jR1SVxJeeo8n1sg"; .type = "Type_Return" } ] } [ assume eq(0x400770:bv64, $PC); - call @_aarch64_eval(0xf9400bf3:bv32, 0x400770:bv64) { .asm = "ldr x19, [sp, #0x10]" }; - call @_aarch64_eval(0xa8c27bfd:bv32, 0x400774:bv64) { .asm = "ldp x29, x30, [sp], #0x20" }; - call @_aarch64_eval(0xd65f03c0:bv32, 0x400778:bv64) { .asm = "ret " }; - assert boolor(); - goto (%ret_2); + goto (%block_9); ]; + block %block_9 { .asm = "ldr x19, [sp, #0x10]" } [ + var lv_5:bv64 := 0x0:bv64; + var lv_6:bv64 := load le $mem:(bv64->bv8) bvadd($SP, 0x10:bv64) 64; + var lv_5:bv64 := lv_6:bv64; + $R19:bv64 := zero_extend(0, zero_extend(0, lv_5:bv64)); + (var BranchTaken:bool := false, $PC:bv64 := 0x400774:bv64); + goto (%block_10); + ]; + block %block_10 { .asm = "ldp x29, x30, [sp], #0x20" } [ + var lv_7:bv64 := 0x0:bv64; + var lv_7:bv64 := $SP; + var lv_8:bv64 := 0x0:bv64; + var lv_9:bv64 := load le $mem:(bv64->bv8) $SP 64; + var lv_8:bv64 := lv_9:bv64; + var lv_10:bv64 := 0x0:bv64; + var lv_11:bv64 := load le $mem:(bv64->bv8) bvadd($SP, 0x8:bv64) 64; + var lv_10:bv64 := lv_11:bv64; + $R29:bv64 := lv_8:bv64; + $R30:bv64 := lv_10:bv64; + $SP:bv64 := bvadd(lv_7:bv64, 0x20:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x400778:bv64); + goto (%block_11); + ]; + block %block_11 { .asm = "ret " } [ + var lv_12:bv64 := 0x0:bv64; + var BTypeNext:bv2 := 0x0:bv2; + var BranchTaken:bool := true; + $PC:bv64 := $R30; + goto (%__do_global_dtors_aux_code_5); + ]; + block %__do_global_dtors_aux_code_5 [ assert boolor(); goto (%ret_2); ]; block %ret_2 [ return; ]; block %__do_global_dtors_aux_code_3 { .address = 4196196; .gtirb_block = "lwyID0MJQb6vgyjzPFtz8Q"; .succ = [ { .address = 4196064; .conditional = "false"; .direct = "true"; .target = "stmts:GW0MHC+ORUKlCdpgOcZ6zA"; .type = "Type_Call" } ] } [ assume eq(0x400764:bv64, $PC); - call @_aarch64_eval(0x97ffffdf:bv32, 0x400764:bv64) { .asm = "bl #0xffffffffffffff7c" }; + goto (%block_12); + ]; + block %block_12 { .asm = "bl #0xffffffffffffff7c" } [ + $R30:bv64 := 0x400768:bv64; + var BranchTaken:bool := true; + $PC:bv64 := 0x4006e0:bv64; + goto (%__do_global_dtors_aux_code_6); + ]; + block %__do_global_dtors_aux_code_6 [ assert boolor(eq(0x4006e0:bv64, $PC)); goto (%__do_global_dtors_aux_ext); ]; @@ -123,13 +320,28 @@ .target = "internal:SFN4dpBgSO2bPUu0fyDluw"; .type = "Type_Fallthrough" } ] } [ assume eq(0x400768:bv64, $PC); - call @_aarch64_eval(0x52800020:bv32, 0x400768:bv64) { .asm = "mov w0, #1" }; - call @_aarch64_eval(0x3900a260:bv32, 0x40076c:bv64) { .asm = "strb w0, [x19, #0x28]" }; + goto (%block_13); + ]; + block %block_13 { .asm = "mov w0, #1" } [ + $R0:bv64 := 0x1:bv64; + (var BranchTaken:bool := false, $PC:bv64 := 0x40076c:bv64); + goto (%block_14); + ]; + block %block_14 { .asm = "strb w0, [x19, #0x28]" } [ + var lv_13:bv64 := 0x0:bv64; + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd($R19, 0x28:bv64) extract(8,0, $R0) 8; + (var BranchTaken:bool := false, $PC:bv64 := 0x400770:bv64); + goto (%__do_global_dtors_aux_code_7); + ]; + block %__do_global_dtors_aux_code_7 [ assert boolor(eq(0x400770:bv64, $PC)); goto (%__do_global_dtors_aux_code_1); ] ]; proc @register_tm_clones() -> () { } + modifies $PC:bv64, $R0:bv64, $R1:bv64, $R16:bv64, $R2:bv64 + captures $PC:bv64, $R0:bv64, $R1:bv64, $R16:bv64, $R2:bv64, $R30:bv64, + $mem:(bv64->bv8) requires boolor(eq(0x400710:bv64, $PC)) [ @@ -141,15 +353,86 @@ { .address = 4196168; .conditional = "true"; .direct = "true"; .target = "internal:IkNYmV06TxC75h8A4NM3wA"; .type = "Type_Branch" } ] } [ assume eq(0x400710:bv64, $PC); - call @_aarch64_eval(0x90000100:bv32, 0x400710:bv64) { .asm = "adrp x0, #0x20000" }; - call @_aarch64_eval(0x9100a000:bv32, 0x400714:bv64) { .asm = "add x0, x0, #0x28" }; - call @_aarch64_eval(0x90000101:bv32, 0x400718:bv64) { .asm = "adrp x1, #0x20000" }; - call @_aarch64_eval(0x9100a021:bv32, 0x40071c:bv64) { .asm = "add x1, x1, #0x28" }; - call @_aarch64_eval(0xcb000021:bv32, 0x400720:bv64) { .asm = "sub x1, x1, x0" }; - call @_aarch64_eval(0xd37ffc22:bv32, 0x400724:bv64) { .asm = "lsr x2, x1, #0x3f" }; - call @_aarch64_eval(0x8b810c41:bv32, 0x400728:bv64) { .asm = "add x1, x2, x1, asr #3" }; - call @_aarch64_eval(0x9341fc21:bv32, 0x40072c:bv64) { .asm = "asr x1, x1, #1" }; - call @_aarch64_eval(0xb40000c1:bv32, 0x400730:bv64) { .asm = "cbz x1, #0x18" }; + goto (%block); + ]; + block %block { .asm = "adrp x0, #0x20000" } [ + $R0:bv64 := 0x420000:bv64; + (var BranchTaken:bool := false, $PC:bv64 := 0x400714:bv64); + goto (%block_1); + ]; + block %block_1 { .asm = "add x0, x0, #0x28" } [ + var lv:bv64 := 0x0:bv64; + var lv_1:bv64 := 0x0:bv64; + var lv_1:bv64 := $R0; + $R0:bv64 := bvadd(lv_1:bv64, 0x28:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x400718:bv64); + goto (%block_2); + ]; + block %block_2 { .asm = "adrp x1, #0x20000" } [ + $R1:bv64 := 0x420000:bv64; + (var BranchTaken:bool := false, $PC:bv64 := 0x40071c:bv64); + goto (%block_3); + ]; + block %block_3 { .asm = "add x1, x1, #0x28" } [ + var lv_2:bv64 := 0x0:bv64; + var lv_3:bv64 := 0x0:bv64; + var lv_3:bv64 := $R1; + $R1:bv64 := bvadd(lv_3:bv64, 0x28:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x400720:bv64); + goto (%block_4); + ]; + block %block_4 { .asm = "sub x1, x1, x0" } [ + var lv_4:bv64 := 0x0:bv64; + var lv_4:bv64 := $R1; + var lv_5:bv64 := 0x0:bv64; + var lv_5:bv64 := $R0; + $R1:bv64 := bvadd(bvadd(lv_4:bv64, + bvnot(bvshl(lv_5:bv64, zero_extend(52, 0x0:bv12)))), 0x1:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x400724:bv64); + goto (%block_5); + ]; + block %block_5 { .asm = "lsr x2, x1, #0x3f" } [ + var lv_6:bv64 := 0x0:bv64; + var lv_6:bv64 := $R1; + $R2:bv64 := bvor(bvand(0x0:bv64, 0xfffffffffffffffe:bv64), + bvand(bvor(bvand(0x0:bv64, 0x0:bv64), + bvand(bvor(bvlshr(lv_6:bv64, zero_extend(52, 0x3f:bv12)), + bvshl(lv_6:bv64, zero_extend(48, 0x1:bv16))), 0xffffffffffffffff:bv64)), + 0x1:bv64)); + (var BranchTaken:bool := false, $PC:bv64 := 0x400728:bv64); + goto (%block_6); + ]; + block %block_6 { .asm = "add x1, x2, x1, asr #3" } [ + var lv_7:bv64 := 0x0:bv64; + var lv_7:bv64 := $R2; + var lv_8:bv64 := 0x0:bv64; + var lv_8:bv64 := $R1; + $R1:bv64 := bvadd(lv_7:bv64, bvashr(lv_8:bv64, zero_extend(52, 0x3:bv12))); + (var BranchTaken:bool := false, $PC:bv64 := 0x40072c:bv64); + goto (%register_tm_clones_code_4); + ]; + block %register_tm_clones_code_4 [ + call @_aarch64_eval(0x9341fc21:bv32, 0x40072c:bv64) { .asm = "asr x1, x1, #1"; + .error = "Failure(\"f_gen_replicate_bits\")" }; + goto (%block_7); + ]; + block %block_7 { .asm = "cbz x1, #0x18" } [ goto (%block_9,%block_8); ]; + block %block_8 [ + assume eq($R1, 0x0:bv64); + var BranchTaken:bool := true; + $PC:bv64 := 0x400748:bv64; + goto (%block_10); + ]; + block %block_9 [ + assume boolnot(eq($R1, 0x0:bv64)); + (var BranchTaken:bool := false, $PC:bv64 := 0x400734:bv64); + goto (%block_10); + ]; + block %block_10 [ + $PC:bv64 := if eq($R1, 0x0:bv64) then 0x400748:bv64 else 0x400734:bv64; + goto (%register_tm_clones_code_5); + ]; + block %register_tm_clones_code_5 [ assert boolor(eq(0x400734:bv64, $PC), eq(0x400748:bv64, $PC)); goto (%register_tm_clones_code_3,%register_tm_clones_code); ]; @@ -158,10 +441,16 @@ .succ = [ { .conditional = "false"; .direct = "false"; .target = "proxy:P8unZs8jR1SVxJeeo8n1sg"; .type = "Type_Return" } ] } [ assume eq(0x400748:bv64, $PC); - call @_aarch64_eval(0xd65f03c0:bv32, 0x400748:bv64) { .asm = "ret " }; - assert boolor(); - goto (%ret); + goto (%block_11); + ]; + block %block_11 { .asm = "ret " } [ + var lv_10:bv64 := 0x0:bv64; + var BTypeNext:bv2 := 0x0:bv2; + var BranchTaken:bool := true; + $PC:bv64 := $R30; + goto (%register_tm_clones_code_6); ]; + block %register_tm_clones_code_6 [ assert boolor(); goto (%ret); ]; block %ret [ return; ]; block %register_tm_clones_code_3 { .address = 4196148; .gtirb_block = "tXIOhSQ+R1WA/9VL5+6KQQ"; @@ -171,9 +460,40 @@ { .address = 4196168; .conditional = "true"; .direct = "true"; .target = "internal:IkNYmV06TxC75h8A4NM3wA"; .type = "Type_Branch" } ] } [ assume eq(0x400734:bv64, $PC); - call @_aarch64_eval(0xf00000e2:bv32, 0x400734:bv64) { .asm = "adrp x2, #0x1f000" }; - call @_aarch64_eval(0xf947f042:bv32, 0x400738:bv64) { .asm = "ldr x2, [x2, #0xfe0]" }; - call @_aarch64_eval(0xb4000062:bv32, 0x40073c:bv64) { .asm = "cbz x2, #0xc" }; + goto (%block_12); + ]; + block %block_12 { .asm = "adrp x2, #0x1f000" } [ + $R2:bv64 := 0x41f000:bv64; + (var BranchTaken:bool := false, $PC:bv64 := 0x400738:bv64); + goto (%block_13); + ]; + block %block_13 { .asm = "ldr x2, [x2, #0xfe0]" } [ + var lv_11:bv64 := 0x0:bv64; + var lv_11:bv64 := $R2; + var lv_12:bv64 := 0x0:bv64; + var lv_13:bv64 := load le $mem:(bv64->bv8) bvadd(lv_11:bv64, 0xfe0:bv64) 64; + var lv_12:bv64 := lv_13:bv64; + $R2:bv64 := zero_extend(0, zero_extend(0, lv_12:bv64)); + (var BranchTaken:bool := false, $PC:bv64 := 0x40073c:bv64); + goto (%block_14); + ]; + block %block_14 { .asm = "cbz x2, #0xc" } [ goto (%block_16,%block_15); ]; + block %block_15 [ + assume eq($R2, 0x0:bv64); + var BranchTaken:bool := true; + $PC:bv64 := 0x400748:bv64; + goto (%block_17); + ]; + block %block_16 [ + assume boolnot(eq($R2, 0x0:bv64)); + (var BranchTaken:bool := false, $PC:bv64 := 0x400740:bv64); + goto (%block_17); + ]; + block %block_17 [ + $PC:bv64 := if eq($R2, 0x0:bv64) then 0x400748:bv64 else 0x400740:bv64; + goto (%register_tm_clones_code_7); + ]; + block %register_tm_clones_code_7 [ assert boolor(eq(0x400740:bv64, $PC), eq(0x400748:bv64, $PC)); goto (%register_tm_clones_code_1,%register_tm_clones_code); ]; @@ -182,13 +502,30 @@ .succ = [ { .conditional = "false"; .direct = "false"; .target = "proxy:P8unZs8jR1SVxJeeo8n1sg"; .type = "Type_Branch" } ] } [ assume eq(0x400740:bv64, $PC); - call @_aarch64_eval(0xaa0203f0:bv32, 0x400740:bv64) { .asm = "mov x16, x2" }; - call @_aarch64_eval(0xd61f0200:bv32, 0x400744:bv64) { .asm = "br x16" }; - assert boolor(); - unreachable; - ] + goto (%block_18); + ]; + block %block_18 { .asm = "mov x16, x2" } [ + var lv_14:bv64 := 0x0:bv64; + var lv_14:bv64 := 0x0:bv64; + var lv_15:bv64 := 0x0:bv64; + var lv_15:bv64 := $R2; + $R16:bv64 := bvor(lv_14:bv64, bvshl(lv_15:bv64, zero_extend(52, 0x0:bv12))); + (var BranchTaken:bool := false, $PC:bv64 := 0x400744:bv64); + goto (%block_19); + ]; + block %block_19 { .asm = "br x16" } [ + var lv_16:bv64 := 0x0:bv64; + var BTypeNext:bv2 := 0x1:bv2; + var BranchTaken:bool := true; + $PC:bv64 := $R16; + goto (%register_tm_clones_code_8); + ]; + block %register_tm_clones_code_8 [ assert boolor(); unreachable; ] ]; proc @frame_dummy() -> () { } + modifies $PC:bv64, $R0:bv64, $R1:bv64, $R16:bv64, $R2:bv64 + captures $PC:bv64, $R0:bv64, $R1:bv64, $R16:bv64, $R2:bv64, $R30:bv64, + $mem:(bv64->bv8) requires boolor(eq(0x400780:bv64, $PC)) [ @@ -197,7 +534,14 @@ .succ = [ { .address = 4196112; .conditional = "false"; .direct = "true"; .target = "stmts:rIlbG4jGSTydaFqMhxCKWw"; .type = "Type_Branch" } ] } [ assume eq(0x400780:bv64, $PC); - call @_aarch64_eval(0x17ffffe4:bv32, 0x400780:bv64) { .asm = "b #0xffffffffffffff90" }; + goto (%block); + ]; + block %block { .asm = "b #0xffffffffffffff90" } [ + var BranchTaken:bool := true; + $PC:bv64 := 0x400710:bv64; + goto (%frame_dummy_code_1); + ]; + block %frame_dummy_code_1 [ assert boolor(eq(0x400710:bv64, $PC)); goto (%frame_dummy_ext); ]; @@ -209,6 +553,8 @@ ] ]; proc @FUN_400660() -> () { } + modifies $PC:bv64, $R16:bv64, $R17:bv64 + captures $PC:bv64, $R16:bv64, $R17:bv64, $mem:(bv64->bv8) requires boolor(eq(0x400660:bv64, $PC)) [ @@ -217,15 +563,44 @@ .succ = [ { .conditional = "false"; .direct = "false"; .target = "proxy:BsLBdgTFQlOA45HTKKU2gQ"; .type = "Type_Branch" } ] } [ assume eq(0x400660:bv64, $PC); - call @_aarch64_eval(0x90000110:bv32, 0x400660:bv64) { .asm = "adrp x16, #0x20000" }; - call @_aarch64_eval(0xf9400a11:bv32, 0x400664:bv64) { .asm = "ldr x17, [x16, #0x10]" }; - call @_aarch64_eval(0x91004210:bv32, 0x400668:bv64) { .asm = "add x16, x16, #0x10" }; - call @_aarch64_eval(0xd61f0220:bv32, 0x40066c:bv64) { .asm = "br x17" }; - assert boolor(); - unreachable; - ] + goto (%block); + ]; + block %block { .asm = "adrp x16, #0x20000" } [ + $R16:bv64 := 0x420000:bv64; + (var BranchTaken:bool := false, $PC:bv64 := 0x400664:bv64); + goto (%block_1); + ]; + block %block_1 { .asm = "ldr x17, [x16, #0x10]" } [ + var lv:bv64 := 0x0:bv64; + var lv:bv64 := $R16; + var lv_1:bv64 := 0x0:bv64; + var lv_2:bv64 := load le $mem:(bv64->bv8) bvadd(lv:bv64, 0x10:bv64) 64; + var lv_1:bv64 := lv_2:bv64; + $R17:bv64 := zero_extend(0, zero_extend(0, lv_1:bv64)); + (var BranchTaken:bool := false, $PC:bv64 := 0x400668:bv64); + goto (%block_2); + ]; + block %block_2 { .asm = "add x16, x16, #0x10" } [ + var lv_3:bv64 := 0x0:bv64; + var lv_4:bv64 := 0x0:bv64; + var lv_4:bv64 := $R16; + $R16:bv64 := bvadd(lv_4:bv64, 0x10:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x40066c:bv64); + goto (%block_3); + ]; + block %block_3 { .asm = "br x17" } [ + var lv_5:bv64 := 0x0:bv64; + var BTypeNext:bv2 := 0x1:bv2; + var BranchTaken:bool := true; + $PC:bv64 := $R17; + goto (%FUN_400660_code_1); + ]; + block %FUN_400660_code_1 [ assert boolor(); unreachable; ] ]; proc @Sqrt() -> () { } + modifies $PC:bv64, $R0:bv64, $R1:bv64, $SP:bv64, $mem:(bv64->bv8) + captures $PC:bv64, $PSTATE_N:bv1, $PSTATE_V:bv1, $PSTATE_Z:bv1, $R0:bv64, + $R1:bv64, $R30:bv64, $SP:bv64, $mem:(bv64->bv8) requires boolor(eq(0x400784:bv64, $PC)) [ @@ -234,13 +609,52 @@ .succ = [ { .address = 4196328; .conditional = "false"; .direct = "true"; .target = "internal:32fWxY7+R++JNJOFTmT+Sg"; .type = "Type_Branch" } ] } [ assume eq(0x400784:bv64, $PC); - call @_aarch64_eval(0xd100c3ff:bv32, 0x400784:bv64) { .asm = "sub sp, sp, #0x30" }; - call @_aarch64_eval(0xf90007e0:bv32, 0x400788:bv64) { .asm = "str x0, [sp, #8]" }; - call @_aarch64_eval(0xf90017ff:bv32, 0x40078c:bv64) { .asm = "str xzr, [sp, #0x28]" }; - call @_aarch64_eval(0xf94007e0:bv32, 0x400790:bv64) { .asm = "ldr x0, [sp, #8]" }; - call @_aarch64_eval(0x91000400:bv32, 0x400794:bv64) { .asm = "add x0, x0, #1" }; - call @_aarch64_eval(0xf90013e0:bv32, 0x400798:bv64) { .asm = "str x0, [sp, #0x20]" }; - call @_aarch64_eval(0x14000013:bv32, 0x40079c:bv64) { .asm = "b #0x4c" }; + goto (%block); + ]; + block %block { .asm = "sub sp, sp, #0x30" } [ + var lv:bv64 := 0x0:bv64; + var lv:bv64 := $SP; + $SP:bv64 := bvadd(bvadd(lv:bv64, 0xffffffffffffffcf:bv64), 0x1:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x400788:bv64); + goto (%block_1); + ]; + block %block_1 { .asm = "str x0, [sp, #8]" } [ + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd($SP, 0x8:bv64) $R0 64; + (var BranchTaken:bool := false, $PC:bv64 := 0x40078c:bv64); + goto (%block_2); + ]; + block %block_2 { .asm = "str xzr, [sp, #0x28]" } [ + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd($SP, 0x28:bv64) 0x0:bv64 64; + (var BranchTaken:bool := false, $PC:bv64 := 0x400790:bv64); + goto (%block_3); + ]; + block %block_3 { .asm = "ldr x0, [sp, #8]" } [ + var lv_1:bv64 := 0x0:bv64; + var lv_2:bv64 := load le $mem:(bv64->bv8) bvadd($SP, 0x8:bv64) 64; + var lv_1:bv64 := lv_2:bv64; + $R0:bv64 := zero_extend(0, zero_extend(0, lv_1:bv64)); + (var BranchTaken:bool := false, $PC:bv64 := 0x400794:bv64); + goto (%block_4); + ]; + block %block_4 { .asm = "add x0, x0, #1" } [ + var lv_3:bv64 := 0x0:bv64; + var lv_4:bv64 := 0x0:bv64; + var lv_4:bv64 := $R0; + $R0:bv64 := bvadd(lv_4:bv64, 0x1:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x400798:bv64); + goto (%block_5); + ]; + block %block_5 { .asm = "str x0, [sp, #0x20]" } [ + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd($SP, 0x20:bv64) $R0 64; + (var BranchTaken:bool := false, $PC:bv64 := 0x40079c:bv64); + goto (%block_6); + ]; + block %block_6 { .asm = "b #0x4c" } [ + var BranchTaken:bool := true; + $PC:bv64 := 0x4007e8:bv64; + goto (%Sqrt_code_6); + ]; + block %Sqrt_code_6 [ assert boolor(eq(0x4007e8:bv64, $PC)); goto (%Sqrt_code_5); ]; @@ -252,11 +666,56 @@ .target = "internal:lr6o4ptnRiK3TGR1gpiWGg"; .type = "Type_Fallthrough" } ] } [ assume eq(0x4007e8:bv64, $PC); - call @_aarch64_eval(0xf94017e0:bv32, 0x4007e8:bv64) { .asm = "ldr x0, [sp, #0x28]" }; - call @_aarch64_eval(0x91000400:bv32, 0x4007ec:bv64) { .asm = "add x0, x0, #1" }; - call @_aarch64_eval(0xf94013e1:bv32, 0x4007f0:bv64) { .asm = "ldr x1, [sp, #0x20]" }; - call @_aarch64_eval(0xeb00003f:bv32, 0x4007f4:bv64) { .asm = "cmp x1, x0" }; - call @_aarch64_eval(0x54fffd41:bv32, 0x4007f8:bv64) { .asm = "b.ne #0xffffffffffffffa8" }; + goto (%block_7); + ]; + block %block_7 { .asm = "ldr x0, [sp, #0x28]" } [ + var lv_5:bv64 := 0x0:bv64; + var lv_6:bv64 := load le $mem:(bv64->bv8) bvadd($SP, 0x28:bv64) 64; + var lv_5:bv64 := lv_6:bv64; + $R0:bv64 := zero_extend(0, zero_extend(0, lv_5:bv64)); + (var BranchTaken:bool := false, $PC:bv64 := 0x4007ec:bv64); + goto (%block_8); + ]; + block %block_8 { .asm = "add x0, x0, #1" } [ + var lv_7:bv64 := 0x0:bv64; + var lv_8:bv64 := 0x0:bv64; + var lv_8:bv64 := $R0; + $R0:bv64 := bvadd(lv_8:bv64, 0x1:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x4007f0:bv64); + goto (%block_9); + ]; + block %block_9 { .asm = "ldr x1, [sp, #0x20]" } [ + var lv_9:bv64 := 0x0:bv64; + var lv_10:bv64 := load le $mem:(bv64->bv8) bvadd($SP, 0x20:bv64) 64; + var lv_9:bv64 := lv_10:bv64; + $R1:bv64 := zero_extend(0, zero_extend(0, lv_9:bv64)); + (var BranchTaken:bool := false, $PC:bv64 := 0x4007f4:bv64); + goto (%Sqrt_code_7); + ]; + block %Sqrt_code_7 [ + call @_aarch64_eval(0xeb00003f:bv32, 0x4007f4:bv64) { .asm = "cmp x1, x0"; + .error = "Failure(\"f_gen_cvt_bool_bv\")" }; + goto (%block_10); + ]; + block %block_10 { .asm = "b.ne #0xffffffffffffffa8" } [ + goto (%block_12,%block_11); + ]; + block %block_11 [ + assume boolnot(eq($PSTATE_Z, 0x1:bv1)); + var BranchTaken:bool := true; + $PC:bv64 := 0x4007a0:bv64; + goto (%block_13); + ]; + block %block_12 [ + assume boolnot(boolnot(eq($PSTATE_Z, 0x1:bv1))); + (var BranchTaken:bool := false, $PC:bv64 := 0x4007fc:bv64); + goto (%block_13); + ]; + block %block_13 [ + $PC:bv64 := if boolnot(eq($PSTATE_Z, 0x1:bv1)) then 0x4007a0:bv64 else 0x4007fc:bv64; + goto (%Sqrt_code_8); + ]; + block %Sqrt_code_8 [ assert boolor(eq(0x4007a0:bv64, $PC), eq(0x4007fc:bv64, $PC)); goto (%Sqrt_code_4,%Sqrt_code_3); ]; @@ -265,12 +724,31 @@ .succ = [ { .address = 4196384; .conditional = "false"; .direct = "true"; .target = "external:rlVqjjqoR6uHwOYvPCS15g"; .type = "Type_Return" } ] } [ assume eq(0x4007fc:bv64, $PC); - call @_aarch64_eval(0xf94017e0:bv32, 0x4007fc:bv64) { .asm = "ldr x0, [sp, #0x28]" }; - call @_aarch64_eval(0x9100c3ff:bv32, 0x400800:bv64) { .asm = "add sp, sp, #0x30" }; - call @_aarch64_eval(0xd65f03c0:bv32, 0x400804:bv64) { .asm = "ret " }; - assert boolor(eq(0x400820:bv64, $PC)); - goto (%ret_3); + goto (%block_14); + ]; + block %block_14 { .asm = "ldr x0, [sp, #0x28]" } [ + var lv_13:bv64 := 0x0:bv64; + var lv_14:bv64 := load le $mem:(bv64->bv8) bvadd($SP, 0x28:bv64) 64; + var lv_13:bv64 := lv_14:bv64; + $R0:bv64 := zero_extend(0, zero_extend(0, lv_13:bv64)); + (var BranchTaken:bool := false, $PC:bv64 := 0x400800:bv64); + goto (%block_15); + ]; + block %block_15 { .asm = "add sp, sp, #0x30" } [ + var lv_15:bv64 := 0x0:bv64; + var lv_15:bv64 := $SP; + $SP:bv64 := bvadd(lv_15:bv64, 0x30:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x400804:bv64); + goto (%block_16); ]; + block %block_16 { .asm = "ret " } [ + var lv_16:bv64 := 0x0:bv64; + var BTypeNext:bv2 := 0x0:bv2; + var BranchTaken:bool := true; + $PC:bv64 := $R30; + goto (%Sqrt_code_9); + ]; + block %Sqrt_code_9 [ assert boolor(eq(0x400820:bv64, $PC)); goto (%ret_3); ]; block %ret_3 [ return; ]; block %Sqrt_code_4 { .address = 4196256; .gtirb_block = "rCSSdLZcRB2TKAu9h+WCqg"; @@ -280,19 +758,119 @@ { .address = 4196320; .conditional = "true"; .direct = "true"; .target = "internal:HVqN0/3+RWiLPKsHRvUqeg"; .type = "Type_Branch" } ] } [ assume eq(0x4007a0:bv64, $PC); - call @_aarch64_eval(0xf94017e1:bv32, 0x4007a0:bv64) { .asm = "ldr x1, [sp, #0x28]" }; - call @_aarch64_eval(0xf94013e0:bv32, 0x4007a4:bv64) { .asm = "ldr x0, [sp, #0x20]" }; - call @_aarch64_eval(0x8b000020:bv32, 0x4007a8:bv64) { .asm = "add x0, x1, x0" }; - call @_aarch64_eval(0xd37ffc01:bv32, 0x4007ac:bv64) { .asm = "lsr x1, x0, #0x3f" }; - call @_aarch64_eval(0x8b000020:bv32, 0x4007b0:bv64) { .asm = "add x0, x1, x0" }; - call @_aarch64_eval(0x9341fc00:bv32, 0x4007b4:bv64) { .asm = "asr x0, x0, #1" }; - call @_aarch64_eval(0xb9001fe0:bv32, 0x4007b8:bv64) { .asm = "str w0, [sp, #0x1c]" }; - call @_aarch64_eval(0xb9401fe0:bv32, 0x4007bc:bv64) { .asm = "ldr w0, [sp, #0x1c]" }; - call @_aarch64_eval(0x1b007c00:bv32, 0x4007c0:bv64) { .asm = "mul w0, w0, w0" }; - call @_aarch64_eval(0x93407c00:bv32, 0x4007c4:bv64) { .asm = "sxtw x0, w0" }; - call @_aarch64_eval(0xf94007e1:bv32, 0x4007c8:bv64) { .asm = "ldr x1, [sp, #8]" }; - call @_aarch64_eval(0xeb00003f:bv32, 0x4007cc:bv64) { .asm = "cmp x1, x0" }; - call @_aarch64_eval(0x5400008b:bv32, 0x4007d0:bv64) { .asm = "b.lt #0x10" }; + goto (%block_17); + ]; + block %block_17 { .asm = "ldr x1, [sp, #0x28]" } [ + var lv_17:bv64 := 0x0:bv64; + var lv_18:bv64 := load le $mem:(bv64->bv8) bvadd($SP, 0x28:bv64) 64; + var lv_17:bv64 := lv_18:bv64; + $R1:bv64 := zero_extend(0, zero_extend(0, lv_17:bv64)); + (var BranchTaken:bool := false, $PC:bv64 := 0x4007a4:bv64); + goto (%block_18); + ]; + block %block_18 { .asm = "ldr x0, [sp, #0x20]" } [ + var lv_19:bv64 := 0x0:bv64; + var lv_20:bv64 := load le $mem:(bv64->bv8) bvadd($SP, 0x20:bv64) 64; + var lv_19:bv64 := lv_20:bv64; + $R0:bv64 := zero_extend(0, zero_extend(0, lv_19:bv64)); + (var BranchTaken:bool := false, $PC:bv64 := 0x4007a8:bv64); + goto (%block_19); + ]; + block %block_19 { .asm = "add x0, x1, x0" } [ + var lv_21:bv64 := 0x0:bv64; + var lv_21:bv64 := $R1; + var lv_22:bv64 := 0x0:bv64; + var lv_22:bv64 := $R0; + $R0:bv64 := bvadd(lv_21:bv64, bvshl(lv_22:bv64, zero_extend(52, 0x0:bv12))); + (var BranchTaken:bool := false, $PC:bv64 := 0x4007ac:bv64); + goto (%block_20); + ]; + block %block_20 { .asm = "lsr x1, x0, #0x3f" } [ + var lv_23:bv64 := 0x0:bv64; + var lv_23:bv64 := $R0; + $R1:bv64 := bvor(bvand(0x0:bv64, 0xfffffffffffffffe:bv64), + bvand(bvor(bvand(0x0:bv64, 0x0:bv64), + bvand(bvor(bvlshr(lv_23:bv64, zero_extend(52, 0x3f:bv12)), + bvshl(lv_23:bv64, zero_extend(48, 0x1:bv16))), 0xffffffffffffffff:bv64)), + 0x1:bv64)); + (var BranchTaken:bool := false, $PC:bv64 := 0x4007b0:bv64); + goto (%block_21); + ]; + block %block_21 { .asm = "add x0, x1, x0" } [ + var lv_24:bv64 := 0x0:bv64; + var lv_24:bv64 := $R1; + var lv_25:bv64 := 0x0:bv64; + var lv_25:bv64 := $R0; + $R0:bv64 := bvadd(lv_24:bv64, bvshl(lv_25:bv64, zero_extend(52, 0x0:bv12))); + (var BranchTaken:bool := false, $PC:bv64 := 0x4007b4:bv64); + goto (%Sqrt_code_10); + ]; + block %Sqrt_code_10 [ + call @_aarch64_eval(0x9341fc00:bv32, 0x4007b4:bv64) { .asm = "asr x0, x0, #1"; + .error = "Failure(\"f_gen_replicate_bits\")" }; + goto (%block_22); + ]; + block %block_22 { .asm = "str w0, [sp, #0x1c]" } [ + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd($SP, 0x1c:bv64) extract(32,0, $R0) 32; + (var BranchTaken:bool := false, $PC:bv64 := 0x4007bc:bv64); + goto (%block_23); + ]; + block %block_23 { .asm = "ldr w0, [sp, #0x1c]" } [ + var lv_27:bv32 := 0x0:bv32; + var lv_28:bv32 := load le $mem:(bv64->bv8) bvadd($SP, 0x1c:bv64) 32; + var lv_27:bv32 := lv_28:bv32; + $R0:bv64 := zero_extend(32, zero_extend(0, lv_27:bv32)); + (var BranchTaken:bool := false, $PC:bv64 := 0x4007c0:bv64); + goto (%block_24); + ]; + block %block_24 { .asm = "mul w0, w0, w0" } [ + var lv_29:bv32 := 0x0:bv32; + var lv_29:bv32 := extract(32,0, $R0); + var lv_30:bv32 := 0x0:bv32; + var lv_30:bv32 := extract(32,0, $R0); + var lv_31:bv32 := 0x0:bv32; + var lv_31:bv32 := 0x0:bv32; + $R0:bv64 := zero_extend(32, + bvadd(lv_31:bv32, + extract(32,0, bvmul(extract(32,0, lv_29:bv32), extract(32,0, lv_30:bv32))))); + (var BranchTaken:bool := false, $PC:bv64 := 0x4007c4:bv64); + goto (%Sqrt_code_11); + ]; + block %Sqrt_code_11 [ + call @_aarch64_eval(0x93407c00:bv32, 0x4007c4:bv64) { .asm = "sxtw x0, w0"; + .error = "Failure(\"f_gen_replicate_bits\")" }; + goto (%block_25); + ]; + block %block_25 { .asm = "ldr x1, [sp, #8]" } [ + var lv_33:bv64 := 0x0:bv64; + var lv_34:bv64 := load le $mem:(bv64->bv8) bvadd($SP, 0x8:bv64) 64; + var lv_33:bv64 := lv_34:bv64; + $R1:bv64 := zero_extend(0, zero_extend(0, lv_33:bv64)); + (var BranchTaken:bool := false, $PC:bv64 := 0x4007cc:bv64); + goto (%Sqrt_code_12); + ]; + block %Sqrt_code_12 [ + call @_aarch64_eval(0xeb00003f:bv32, 0x4007cc:bv64) { .asm = "cmp x1, x0"; + .error = "Failure(\"f_gen_cvt_bool_bv\")" }; + goto (%block_26); + ]; + block %block_26 { .asm = "b.lt #0x10" } [ goto (%block_28,%block_27); ]; + block %block_27 [ + assume boolnot(eq($PSTATE_N, $PSTATE_V)); + var BranchTaken:bool := true; + $PC:bv64 := 0x4007e0:bv64; + goto (%block_29); + ]; + block %block_28 [ + assume boolnot(boolnot(eq($PSTATE_N, $PSTATE_V))); + (var BranchTaken:bool := false, $PC:bv64 := 0x4007d4:bv64); + goto (%block_29); + ]; + block %block_29 [ + $PC:bv64 := if boolnot(eq($PSTATE_N, $PSTATE_V)) then 0x4007e0:bv64 else 0x4007d4:bv64; + goto (%Sqrt_code_13); + ]; + block %Sqrt_code_13 [ assert boolor(eq(0x4007d4:bv64, $PC), eq(0x4007e0:bv64, $PC)); goto (%Sqrt_code_2,%Sqrt_code); ]; @@ -301,8 +879,22 @@ .target = "internal:32fWxY7+R++JNJOFTmT+Sg"; .type = "Type_Fallthrough" } ] } [ assume eq(0x4007e0:bv64, $PC); - call @_aarch64_eval(0xb9801fe0:bv32, 0x4007e0:bv64) { .asm = "ldrsw x0, [sp, #0x1c]" }; - call @_aarch64_eval(0xf90013e0:bv32, 0x4007e4:bv64) { .asm = "str x0, [sp, #0x20]" }; + goto (%block_30); + ]; + block %block_30 { .asm = "ldrsw x0, [sp, #0x1c]" } [ + var lv_37:bv32 := 0x0:bv32; + var lv_38:bv32 := load le $mem:(bv64->bv8) bvadd($SP, 0x1c:bv64) 32; + var lv_37:bv32 := lv_38:bv32; + $R0:bv64 := zero_extend(0, sign_extend(32, lv_37:bv32)); + (var BranchTaken:bool := false, $PC:bv64 := 0x4007e4:bv64); + goto (%block_31); + ]; + block %block_31 { .asm = "str x0, [sp, #0x20]" } [ + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd($SP, 0x20:bv64) $R0 64; + (var BranchTaken:bool := false, $PC:bv64 := 0x4007e8:bv64); + goto (%Sqrt_code_14); + ]; + block %Sqrt_code_14 [ assert boolor(eq(0x4007e8:bv64, $PC)); goto (%Sqrt_code_5); ]; @@ -311,14 +903,36 @@ .succ = [ { .address = 4196328; .conditional = "false"; .direct = "true"; .target = "internal:32fWxY7+R++JNJOFTmT+Sg"; .type = "Type_Branch" } ] } [ assume eq(0x4007d4:bv64, $PC); - call @_aarch64_eval(0xb9801fe0:bv32, 0x4007d4:bv64) { .asm = "ldrsw x0, [sp, #0x1c]" }; - call @_aarch64_eval(0xf90017e0:bv32, 0x4007d8:bv64) { .asm = "str x0, [sp, #0x28]" }; - call @_aarch64_eval(0x14000003:bv32, 0x4007dc:bv64) { .asm = "b #0xc" }; + goto (%block_32); + ]; + block %block_32 { .asm = "ldrsw x0, [sp, #0x1c]" } [ + var lv_39:bv32 := 0x0:bv32; + var lv_40:bv32 := load le $mem:(bv64->bv8) bvadd($SP, 0x1c:bv64) 32; + var lv_39:bv32 := lv_40:bv32; + $R0:bv64 := zero_extend(0, sign_extend(32, lv_39:bv32)); + (var BranchTaken:bool := false, $PC:bv64 := 0x4007d8:bv64); + goto (%block_33); + ]; + block %block_33 { .asm = "str x0, [sp, #0x28]" } [ + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd($SP, 0x28:bv64) $R0 64; + (var BranchTaken:bool := false, $PC:bv64 := 0x4007dc:bv64); + goto (%block_34); + ]; + block %block_34 { .asm = "b #0xc" } [ + var BranchTaken:bool := true; + $PC:bv64 := 0x4007e8:bv64; + goto (%Sqrt_code_15); + ]; + block %Sqrt_code_15 [ assert boolor(eq(0x4007e8:bv64, $PC)); goto (%Sqrt_code_5); ] ]; proc @_start() -> () { } + modifies $PC:bv64, $R0:bv64, $R1:bv64, $R16:bv64, $R17:bv64, $R2:bv64, $R29:bv64, + $R3:bv64, $R30:bv64, $R4:bv64, $R5:bv64, $R6:bv64 + captures $PC:bv64, $R0:bv64, $R1:bv64, $R16:bv64, $R17:bv64, $R2:bv64, $R29:bv64, + $R3:bv64, $R30:bv64, $R4:bv64, $R5:bv64, $R6:bv64, $SP:bv64, $mem:(bv64->bv8) requires boolor(eq(0x400680:bv64, $PC)) [ @@ -327,18 +941,79 @@ .succ = [ { .address = 4195904; .conditional = "false"; .direct = "true"; .target = "stmts:YmNxI7RsS/6TZy3HTKzvWg"; .type = "Type_Call" } ] } [ assume eq(0x400680:bv64, $PC); - call @_aarch64_eval(0xd503201f:bv32, 0x400680:bv64) { .asm = "nop " }; - call @_aarch64_eval(0xd280001d:bv32, 0x400684:bv64) { .asm = "mov x29, #0" }; - call @_aarch64_eval(0xd280001e:bv32, 0x400688:bv64) { .asm = "mov x30, #0" }; - call @_aarch64_eval(0xaa0003e5:bv32, 0x40068c:bv64) { .asm = "mov x5, x0" }; - call @_aarch64_eval(0xf94003e1:bv32, 0x400690:bv64) { .asm = "ldr x1, [sp]" }; - call @_aarch64_eval(0x910023e2:bv32, 0x400694:bv64) { .asm = "add x2, sp, #8" }; - call @_aarch64_eval(0x910003e6:bv32, 0x400698:bv64) { .asm = "mov x6, sp" }; - call @_aarch64_eval(0x90000000:bv32, 0x40069c:bv64) { .asm = "adrp x0, #0" }; - call @_aarch64_eval(0x911ad000:bv32, 0x4006a0:bv64) { .asm = "add x0, x0, #0x6b4" }; - call @_aarch64_eval(0xd2800003:bv32, 0x4006a4:bv64) { .asm = "mov x3, #0" }; - call @_aarch64_eval(0xd2800004:bv32, 0x4006a8:bv64) { .asm = "mov x4, #0" }; - call @_aarch64_eval(0x97ffffe5:bv32, 0x4006ac:bv64) { .asm = "bl #0xffffffffffffff94" }; + call @_aarch64_eval(0xd503201f:bv32, 0x400680:bv64) { .asm = "nop "; + .error = "Failure(\"unsupported\")" }; + goto (%block); + ]; + block %block { .asm = "mov x29, #0" } [ + $R29:bv64 := 0x0:bv64; + (var BranchTaken:bool := false, $PC:bv64 := 0x400688:bv64); + goto (%block_1); + ]; + block %block_1 { .asm = "mov x30, #0" } [ + $R30:bv64 := 0x0:bv64; + (var BranchTaken:bool := false, $PC:bv64 := 0x40068c:bv64); + goto (%block_2); + ]; + block %block_2 { .asm = "mov x5, x0" } [ + var lv:bv64 := 0x0:bv64; + var lv:bv64 := 0x0:bv64; + var lv_1:bv64 := 0x0:bv64; + var lv_1:bv64 := $R0; + $R5:bv64 := bvor(lv:bv64, bvshl(lv_1:bv64, zero_extend(52, 0x0:bv12))); + (var BranchTaken:bool := false, $PC:bv64 := 0x400690:bv64); + goto (%block_3); + ]; + block %block_3 { .asm = "ldr x1, [sp]" } [ + var lv_2:bv64 := 0x0:bv64; + var lv_3:bv64 := load le $mem:(bv64->bv8) bvadd($SP, 0x0:bv64) 64; + var lv_2:bv64 := lv_3:bv64; + $R1:bv64 := zero_extend(0, zero_extend(0, lv_2:bv64)); + (var BranchTaken:bool := false, $PC:bv64 := 0x400694:bv64); + goto (%block_4); + ]; + block %block_4 { .asm = "add x2, sp, #8" } [ + var lv_4:bv64 := 0x0:bv64; + $R2:bv64 := bvadd($SP, 0x8:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x400698:bv64); + goto (%block_5); + ]; + block %block_5 { .asm = "mov x6, sp" } [ + var lv_5:bv64 := 0x0:bv64; + $R6:bv64 := bvadd($SP, 0x0:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x40069c:bv64); + goto (%block_6); + ]; + block %block_6 { .asm = "adrp x0, #0" } [ + $R0:bv64 := 0x400000:bv64; + (var BranchTaken:bool := false, $PC:bv64 := 0x4006a0:bv64); + goto (%block_7); + ]; + block %block_7 { .asm = "add x0, x0, #0x6b4" } [ + var lv_6:bv64 := 0x0:bv64; + var lv_7:bv64 := 0x0:bv64; + var lv_7:bv64 := $R0; + $R0:bv64 := bvadd(lv_7:bv64, 0x6b4:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x4006a4:bv64); + goto (%block_8); + ]; + block %block_8 { .asm = "mov x3, #0" } [ + $R3:bv64 := 0x0:bv64; + (var BranchTaken:bool := false, $PC:bv64 := 0x4006a8:bv64); + goto (%block_9); + ]; + block %block_9 { .asm = "mov x4, #0" } [ + $R4:bv64 := 0x0:bv64; + (var BranchTaken:bool := false, $PC:bv64 := 0x4006ac:bv64); + goto (%block_10); + ]; + block %block_10 { .asm = "bl #0xffffffffffffff94" } [ + $R30:bv64 := 0x4006b0:bv64; + var BranchTaken:bool := true; + $PC:bv64 := 0x400640:bv64; + goto (%_start_code_3); + ]; + block %_start_code_3 [ assert boolor(eq(0x400640:bv64, $PC)); goto (%_start_ext); ]; @@ -353,7 +1028,15 @@ .succ = [ { .address = 4195936; .conditional = "false"; .direct = "true"; .target = "stmts:iedVtPHmSjuLgqSxHgXOuw"; .type = "Type_Call" } ] } [ assume eq(0x4006b0:bv64, $PC); - call @_aarch64_eval(0x97ffffec:bv32, 0x4006b0:bv64) { .asm = "bl #0xffffffffffffffb0" }; + goto (%block_11); + ]; + block %block_11 { .asm = "bl #0xffffffffffffffb0" } [ + $R30:bv64 := 0x4006b4:bv64; + var BranchTaken:bool := true; + $PC:bv64 := 0x400660:bv64; + goto (%_start_code_4); + ]; + block %_start_code_4 [ assert boolor(eq(0x400660:bv64, $PC)); goto (%_start_ext_2); ]; @@ -365,6 +1048,8 @@ ] ]; proc @_dl_relocate_static_pie() -> () { } + modifies $PC:bv64 + captures $PC:bv64, $R30:bv64 requires boolor(eq(0x4006c0:bv64, $PC)) [ @@ -373,13 +1058,21 @@ .succ = [ { .conditional = "false"; .direct = "false"; .target = "proxy:P8unZs8jR1SVxJeeo8n1sg"; .type = "Type_Return" } ] } [ assume eq(0x4006c0:bv64, $PC); - call @_aarch64_eval(0xd65f03c0:bv32, 0x4006c0:bv64) { .asm = "ret " }; - assert boolor(); - goto (%ret); + goto (%block); + ]; + block %block { .asm = "ret " } [ + var lv:bv64 := 0x0:bv64; + var BTypeNext:bv2 := 0x0:bv2; + var BranchTaken:bool := true; + $PC:bv64 := $R30; + goto (%_dl_relocate_static_pie_code_1); ]; + block %_dl_relocate_static_pie_code_1 [ assert boolor(); goto (%ret); ]; block %ret [ return; ] ]; proc @call_weak_fn() -> () { } + modifies $PC:bv64, $R0:bv64, $R16:bv64, $R17:bv64 + captures $PC:bv64, $R0:bv64, $R16:bv64, $R17:bv64, $R30:bv64, $mem:(bv64->bv8) requires boolor(eq(0x4006c4:bv64, $PC)) [ @@ -391,9 +1084,40 @@ .target = "internal:fxMAJl44TWOTA8IHVD8V7Q"; .type = "Type_Fallthrough" } ] } [ assume eq(0x4006c4:bv64, $PC); - call @_aarch64_eval(0xf00000e0:bv32, 0x4006c4:bv64) { .asm = "adrp x0, #0x1f000" }; - call @_aarch64_eval(0xf947ec00:bv32, 0x4006c8:bv64) { .asm = "ldr x0, [x0, #0xfd8]" }; - call @_aarch64_eval(0xb4000040:bv32, 0x4006cc:bv64) { .asm = "cbz x0, #8" }; + goto (%block); + ]; + block %block { .asm = "adrp x0, #0x1f000" } [ + $R0:bv64 := 0x41f000:bv64; + (var BranchTaken:bool := false, $PC:bv64 := 0x4006c8:bv64); + goto (%block_1); + ]; + block %block_1 { .asm = "ldr x0, [x0, #0xfd8]" } [ + var lv:bv64 := 0x0:bv64; + var lv:bv64 := $R0; + var lv_1:bv64 := 0x0:bv64; + var lv_2:bv64 := load le $mem:(bv64->bv8) bvadd(lv:bv64, 0xfd8:bv64) 64; + var lv_1:bv64 := lv_2:bv64; + $R0:bv64 := zero_extend(0, zero_extend(0, lv_1:bv64)); + (var BranchTaken:bool := false, $PC:bv64 := 0x4006cc:bv64); + goto (%block_2); + ]; + block %block_2 { .asm = "cbz x0, #8" } [ goto (%block_4,%block_3); ]; + block %block_3 [ + assume eq($R0, 0x0:bv64); + var BranchTaken:bool := true; + $PC:bv64 := 0x4006d4:bv64; + goto (%block_5); + ]; + block %block_4 [ + assume boolnot(eq($R0, 0x0:bv64)); + (var BranchTaken:bool := false, $PC:bv64 := 0x4006d0:bv64); + goto (%block_5); + ]; + block %block_5 [ + $PC:bv64 := if eq($R0, 0x0:bv64) then 0x4006d4:bv64 else 0x4006d0:bv64; + goto (%call_weak_fn_code_3); + ]; + block %call_weak_fn_code_3 [ assert boolor(eq(0x4006d4:bv64, $PC), eq(0x4006d0:bv64, $PC)); goto (%call_weak_fn_code_2,%call_weak_fn_code_1); ]; @@ -402,7 +1126,14 @@ .succ = [ { .address = 4195920; .conditional = "false"; .direct = "true"; .target = "stmts:i2bc6yURTw+Pq2nxe63pQA"; .type = "Type_Branch" } ] } [ assume eq(0x4006d0:bv64, $PC); - call @_aarch64_eval(0x17ffffe0:bv32, 0x4006d0:bv64) { .asm = "b #0xffffffffffffff80" }; + goto (%block_6); + ]; + block %block_6 { .asm = "b #0xffffffffffffff80" } [ + var BranchTaken:bool := true; + $PC:bv64 := 0x400650:bv64; + goto (%call_weak_fn_code_4); + ]; + block %call_weak_fn_code_4 [ assert boolor(eq(0x400650:bv64, $PC)); goto (%call_weak_fn_ext_1); ]; @@ -417,13 +1148,26 @@ .succ = [ { .address = 4195856; .conditional = "false"; .direct = "true"; .target = "external:xdU61Ad4R3aE/hVJ17n5eQ"; .type = "Type_Return" } ] } [ assume eq(0x4006d4:bv64, $PC); - call @_aarch64_eval(0xd65f03c0:bv32, 0x4006d4:bv64) { .asm = "ret " }; + goto (%block_7); + ]; + block %block_7 { .asm = "ret " } [ + var lv_3:bv64 := 0x0:bv64; + var BTypeNext:bv2 := 0x0:bv2; + var BranchTaken:bool := true; + $PC:bv64 := $R30; + goto (%call_weak_fn_code_5); + ]; + block %call_weak_fn_code_5 [ assert boolor(eq(0x400610:bv64, $PC)); goto (%ret_3); ]; block %ret_3 [ return; ] ]; proc @main() -> () { } + modifies $PC:bv64, $R0:bv64, $R1:bv64, $R29:bv64, $R30:bv64, $SP:bv64, + $mem:(bv64->bv8) + captures $PC:bv64, $PSTATE_N:bv1, $PSTATE_V:bv1, $PSTATE_Z:bv1, $R0:bv64, + $R1:bv64, $R29:bv64, $R30:bv64, $SP:bv64, $mem:(bv64->bv8) requires boolor(eq(0x400808:bv64, $PC)) [ @@ -431,12 +1175,50 @@ .succ = [ { .address = 4196228; .conditional = "false"; .direct = "true"; .target = "stmts:OuTzy8qRTci75taVjGinFQ"; .type = "Type_Call" } ] } [ assume eq(0x400808:bv64, $PC); - call @_aarch64_eval(0xa9be7bfd:bv32, 0x400808:bv64) { .asm = "stp x29, x30, [sp, #-0x20]!" }; - call @_aarch64_eval(0x910003fd:bv32, 0x40080c:bv64) { .asm = "mov x29, sp" }; - call @_aarch64_eval(0xb9001fe0:bv32, 0x400810:bv64) { .asm = "str w0, [sp, #0x1c]" }; - call @_aarch64_eval(0xf9000be1:bv32, 0x400814:bv64) { .asm = "str x1, [sp, #0x10]" }; - call @_aarch64_eval(0xb9801fe0:bv32, 0x400818:bv64) { .asm = "ldrsw x0, [sp, #0x1c]" }; - call @_aarch64_eval(0x97ffffda:bv32, 0x40081c:bv64) { .asm = "bl #0xffffffffffffff68" }; + goto (%block); + ]; + block %block { .asm = "stp x29, x30, [sp, #-0x20]!" } [ + var lv:bv64 := 0x0:bv64; + var lv:bv64 := $SP; + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd($SP, + 0xffffffffffffffe0:bv64) $R29 64; + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd(bvadd($SP, + 0xffffffffffffffe0:bv64), 0x8:bv64) $R30 64; + $SP:bv64 := bvadd(lv:bv64, 0xffffffffffffffe0:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x40080c:bv64); + goto (%block_1); + ]; + block %block_1 { .asm = "mov x29, sp" } [ + var lv_1:bv64 := 0x0:bv64; + $R29:bv64 := bvadd($SP, 0x0:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x400810:bv64); + goto (%block_2); + ]; + block %block_2 { .asm = "str w0, [sp, #0x1c]" } [ + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd($SP, 0x1c:bv64) extract(32,0, $R0) 32; + (var BranchTaken:bool := false, $PC:bv64 := 0x400814:bv64); + goto (%block_3); + ]; + block %block_3 { .asm = "str x1, [sp, #0x10]" } [ + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd($SP, 0x10:bv64) $R1 64; + (var BranchTaken:bool := false, $PC:bv64 := 0x400818:bv64); + goto (%block_4); + ]; + block %block_4 { .asm = "ldrsw x0, [sp, #0x1c]" } [ + var lv_2:bv32 := 0x0:bv32; + var lv_3:bv32 := load le $mem:(bv64->bv8) bvadd($SP, 0x1c:bv64) 32; + var lv_2:bv32 := lv_3:bv32; + $R0:bv64 := zero_extend(0, sign_extend(32, lv_2:bv32)); + (var BranchTaken:bool := false, $PC:bv64 := 0x40081c:bv64); + goto (%block_5); + ]; + block %block_5 { .asm = "bl #0xffffffffffffff68" } [ + $R30:bv64 := 0x400820:bv64; + var BranchTaken:bool := true; + $PC:bv64 := 0x400784:bv64; + goto (%main_code_2); + ]; + block %main_code_2 [ assert boolor(eq(0x400784:bv64, $PC)); goto (%main_ext); ]; @@ -451,14 +1233,36 @@ .succ = [ { .conditional = "false"; .direct = "false"; .target = "proxy:P8unZs8jR1SVxJeeo8n1sg"; .type = "Type_Return" } ] } [ assume eq(0x400820:bv64, $PC); - call @_aarch64_eval(0xa8c27bfd:bv32, 0x400820:bv64) { .asm = "ldp x29, x30, [sp], #0x20" }; - call @_aarch64_eval(0xd65f03c0:bv32, 0x400824:bv64) { .asm = "ret " }; - assert boolor(); - goto (%ret_1); + goto (%block_6); + ]; + block %block_6 { .asm = "ldp x29, x30, [sp], #0x20" } [ + var lv_4:bv64 := 0x0:bv64; + var lv_4:bv64 := $SP; + var lv_5:bv64 := 0x0:bv64; + var lv_6:bv64 := load le $mem:(bv64->bv8) $SP 64; + var lv_5:bv64 := lv_6:bv64; + var lv_7:bv64 := 0x0:bv64; + var lv_8:bv64 := load le $mem:(bv64->bv8) bvadd($SP, 0x8:bv64) 64; + var lv_7:bv64 := lv_8:bv64; + $R29:bv64 := lv_5:bv64; + $R30:bv64 := lv_7:bv64; + $SP:bv64 := bvadd(lv_4:bv64, 0x20:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x400824:bv64); + goto (%block_7); ]; + block %block_7 { .asm = "ret " } [ + var lv_9:bv64 := 0x0:bv64; + var BTypeNext:bv2 := 0x0:bv2; + var BranchTaken:bool := true; + $PC:bv64 := $R30; + goto (%main_code_3); + ]; + block %main_code_3 [ assert boolor(); goto (%ret_1); ]; block %ret_1 [ return; ] ]; proc @.L_400650() -> () { } + modifies $PC:bv64, $R16:bv64, $R17:bv64 + captures $PC:bv64, $R16:bv64, $R17:bv64, $mem:(bv64->bv8) requires boolor(eq(0x400650:bv64, $PC)) [ @@ -467,15 +1271,43 @@ .succ = [ { .conditional = "false"; .direct = "false"; .target = "proxy:QQLF2yhHRgKOi0ouqIEdXw"; .type = "Type_Branch" } ] } [ assume eq(0x400650:bv64, $PC); - call @_aarch64_eval(0x90000110:bv32, 0x400650:bv64) { .asm = "adrp x16, #0x20000" }; - call @_aarch64_eval(0xf9400611:bv32, 0x400654:bv64) { .asm = "ldr x17, [x16, #8]" }; - call @_aarch64_eval(0x91002210:bv32, 0x400658:bv64) { .asm = "add x16, x16, #8" }; - call @_aarch64_eval(0xd61f0220:bv32, 0x40065c:bv64) { .asm = "br x17" }; - assert boolor(); - unreachable; - ] + goto (%block); + ]; + block %block { .asm = "adrp x16, #0x20000" } [ + $R16:bv64 := 0x420000:bv64; + (var BranchTaken:bool := false, $PC:bv64 := 0x400654:bv64); + goto (%block_1); + ]; + block %block_1 { .asm = "ldr x17, [x16, #8]" } [ + var lv:bv64 := 0x0:bv64; + var lv:bv64 := $R16; + var lv_1:bv64 := 0x0:bv64; + var lv_2:bv64 := load le $mem:(bv64->bv8) bvadd(lv:bv64, 0x8:bv64) 64; + var lv_1:bv64 := lv_2:bv64; + $R17:bv64 := zero_extend(0, zero_extend(0, lv_1:bv64)); + (var BranchTaken:bool := false, $PC:bv64 := 0x400658:bv64); + goto (%block_2); + ]; + block %block_2 { .asm = "add x16, x16, #8" } [ + var lv_3:bv64 := 0x0:bv64; + var lv_4:bv64 := 0x0:bv64; + var lv_4:bv64 := $R16; + $R16:bv64 := bvadd(lv_4:bv64, 0x8:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x40065c:bv64); + goto (%block_3); + ]; + block %block_3 { .asm = "br x17" } [ + var lv_5:bv64 := 0x0:bv64; + var BTypeNext:bv2 := 0x1:bv2; + var BranchTaken:bool := true; + $PC:bv64 := $R17; + goto (%L_400650_code_1); + ]; + block %L_400650_code_1 [ assert boolor(); unreachable; ] ]; proc @FUN_400640() -> () { } + modifies $PC:bv64, $R16:bv64, $R17:bv64 + captures $PC:bv64, $R16:bv64, $R17:bv64, $mem:(bv64->bv8) requires boolor(eq(0x400640:bv64, $PC)) [ @@ -484,15 +1316,44 @@ .succ = [ { .conditional = "false"; .direct = "false"; .target = "proxy:3AqniX2CT+OA1g1jJcUzbQ"; .type = "Type_Branch" } ] } [ assume eq(0x400640:bv64, $PC); - call @_aarch64_eval(0x90000110:bv32, 0x400640:bv64) { .asm = "adrp x16, #0x20000" }; - call @_aarch64_eval(0xf9400211:bv32, 0x400644:bv64) { .asm = "ldr x17, [x16]" }; - call @_aarch64_eval(0x91000210:bv32, 0x400648:bv64) { .asm = "add x16, x16, #0" }; - call @_aarch64_eval(0xd61f0220:bv32, 0x40064c:bv64) { .asm = "br x17" }; - assert boolor(); - unreachable; - ] + goto (%block); + ]; + block %block { .asm = "adrp x16, #0x20000" } [ + $R16:bv64 := 0x420000:bv64; + (var BranchTaken:bool := false, $PC:bv64 := 0x400644:bv64); + goto (%block_1); + ]; + block %block_1 { .asm = "ldr x17, [x16]" } [ + var lv:bv64 := 0x0:bv64; + var lv:bv64 := $R16; + var lv_1:bv64 := 0x0:bv64; + var lv_2:bv64 := load le $mem:(bv64->bv8) bvadd(lv:bv64, 0x0:bv64) 64; + var lv_1:bv64 := lv_2:bv64; + $R17:bv64 := zero_extend(0, zero_extend(0, lv_1:bv64)); + (var BranchTaken:bool := false, $PC:bv64 := 0x400648:bv64); + goto (%block_2); + ]; + block %block_2 { .asm = "add x16, x16, #0" } [ + var lv_3:bv64 := 0x0:bv64; + var lv_4:bv64 := 0x0:bv64; + var lv_4:bv64 := $R16; + $R16:bv64 := bvadd(lv_4:bv64, 0x0:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x40064c:bv64); + goto (%block_3); + ]; + block %block_3 { .asm = "br x17" } [ + var lv_5:bv64 := 0x0:bv64; + var BTypeNext:bv2 := 0x1:bv2; + var BranchTaken:bool := true; + $PC:bv64 := $R17; + goto (%FUN_400640_code_1); + ]; + block %FUN_400640_code_1 [ assert boolor(); unreachable; ] ]; proc @deregister_tm_clones() -> () { } + modifies $PC:bv64, $R0:bv64, $R1:bv64, $R16:bv64 + captures $PC:bv64, $PSTATE_Z:bv1, $R0:bv64, $R1:bv64, $R16:bv64, $R30:bv64, + $mem:(bv64->bv8) requires boolor(eq(0x4006e0:bv64, $PC)) [ @@ -504,12 +1365,56 @@ .target = "internal:GghTYm6bT12tNFmqu0nIjA"; .type = "Type_Fallthrough" } ] } [ assume eq(0x4006e0:bv64, $PC); - call @_aarch64_eval(0x90000100:bv32, 0x4006e0:bv64) { .asm = "adrp x0, #0x20000" }; - call @_aarch64_eval(0x9100a000:bv32, 0x4006e4:bv64) { .asm = "add x0, x0, #0x28" }; - call @_aarch64_eval(0x90000101:bv32, 0x4006e8:bv64) { .asm = "adrp x1, #0x20000" }; - call @_aarch64_eval(0x9100a021:bv32, 0x4006ec:bv64) { .asm = "add x1, x1, #0x28" }; - call @_aarch64_eval(0xeb00003f:bv32, 0x4006f0:bv64) { .asm = "cmp x1, x0" }; - call @_aarch64_eval(0x540000c0:bv32, 0x4006f4:bv64) { .asm = "b.eq #0x18" }; + goto (%block); + ]; + block %block { .asm = "adrp x0, #0x20000" } [ + $R0:bv64 := 0x420000:bv64; + (var BranchTaken:bool := false, $PC:bv64 := 0x4006e4:bv64); + goto (%block_1); + ]; + block %block_1 { .asm = "add x0, x0, #0x28" } [ + var lv:bv64 := 0x0:bv64; + var lv_1:bv64 := 0x0:bv64; + var lv_1:bv64 := $R0; + $R0:bv64 := bvadd(lv_1:bv64, 0x28:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x4006e8:bv64); + goto (%block_2); + ]; + block %block_2 { .asm = "adrp x1, #0x20000" } [ + $R1:bv64 := 0x420000:bv64; + (var BranchTaken:bool := false, $PC:bv64 := 0x4006ec:bv64); + goto (%block_3); + ]; + block %block_3 { .asm = "add x1, x1, #0x28" } [ + var lv_2:bv64 := 0x0:bv64; + var lv_3:bv64 := 0x0:bv64; + var lv_3:bv64 := $R1; + $R1:bv64 := bvadd(lv_3:bv64, 0x28:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x4006f0:bv64); + goto (%deregister_tm_clones_code_4); + ]; + block %deregister_tm_clones_code_4 [ + call @_aarch64_eval(0xeb00003f:bv32, 0x4006f0:bv64) { .asm = "cmp x1, x0"; + .error = "Failure(\"f_gen_cvt_bool_bv\")" }; + goto (%block_4); + ]; + block %block_4 { .asm = "b.eq #0x18" } [ goto (%block_6,%block_5); ]; + block %block_5 [ + assume eq($PSTATE_Z, 0x1:bv1); + var BranchTaken:bool := true; + $PC:bv64 := 0x40070c:bv64; + goto (%block_7); + ]; + block %block_6 [ + assume boolnot(eq($PSTATE_Z, 0x1:bv1)); + (var BranchTaken:bool := false, $PC:bv64 := 0x4006f8:bv64); + goto (%block_7); + ]; + block %block_7 [ + $PC:bv64 := if eq($PSTATE_Z, 0x1:bv1) then 0x40070c:bv64 else 0x4006f8:bv64; + goto (%deregister_tm_clones_code_5); + ]; + block %deregister_tm_clones_code_5 [ assert boolor(eq(0x40070c:bv64, $PC), eq(0x4006f8:bv64, $PC)); goto (%deregister_tm_clones_code_3,%deregister_tm_clones_code_1); ]; @@ -521,9 +1426,40 @@ .target = "internal:NfWWPq4PTwyv0VapVhBGag"; .type = "Type_Fallthrough" } ] } [ assume eq(0x4006f8:bv64, $PC); - call @_aarch64_eval(0xf00000e1:bv32, 0x4006f8:bv64) { .asm = "adrp x1, #0x1f000" }; - call @_aarch64_eval(0xf947e821:bv32, 0x4006fc:bv64) { .asm = "ldr x1, [x1, #0xfd0]" }; - call @_aarch64_eval(0xb4000061:bv32, 0x400700:bv64) { .asm = "cbz x1, #0xc" }; + goto (%block_8); + ]; + block %block_8 { .asm = "adrp x1, #0x1f000" } [ + $R1:bv64 := 0x41f000:bv64; + (var BranchTaken:bool := false, $PC:bv64 := 0x4006fc:bv64); + goto (%block_9); + ]; + block %block_9 { .asm = "ldr x1, [x1, #0xfd0]" } [ + var lv_6:bv64 := 0x0:bv64; + var lv_6:bv64 := $R1; + var lv_7:bv64 := 0x0:bv64; + var lv_8:bv64 := load le $mem:(bv64->bv8) bvadd(lv_6:bv64, 0xfd0:bv64) 64; + var lv_7:bv64 := lv_8:bv64; + $R1:bv64 := zero_extend(0, zero_extend(0, lv_7:bv64)); + (var BranchTaken:bool := false, $PC:bv64 := 0x400700:bv64); + goto (%block_10); + ]; + block %block_10 { .asm = "cbz x1, #0xc" } [ goto (%block_12,%block_11); ]; + block %block_11 [ + assume eq($R1, 0x0:bv64); + var BranchTaken:bool := true; + $PC:bv64 := 0x40070c:bv64; + goto (%block_13); + ]; + block %block_12 [ + assume boolnot(eq($R1, 0x0:bv64)); + (var BranchTaken:bool := false, $PC:bv64 := 0x400704:bv64); + goto (%block_13); + ]; + block %block_13 [ + $PC:bv64 := if eq($R1, 0x0:bv64) then 0x40070c:bv64 else 0x400704:bv64; + goto (%deregister_tm_clones_code_6); + ]; + block %deregister_tm_clones_code_6 [ assert boolor(eq(0x40070c:bv64, $PC), eq(0x400704:bv64, $PC)); goto (%deregister_tm_clones_code_3,%deregister_tm_clones_code_2); ]; @@ -532,23 +1468,48 @@ .succ = [ { .conditional = "false"; .direct = "false"; .target = "proxy:P8unZs8jR1SVxJeeo8n1sg"; .type = "Type_Branch" } ] } [ assume eq(0x400704:bv64, $PC); - call @_aarch64_eval(0xaa0103f0:bv32, 0x400704:bv64) { .asm = "mov x16, x1" }; - call @_aarch64_eval(0xd61f0200:bv32, 0x400708:bv64) { .asm = "br x16" }; - assert boolor(); - unreachable; + goto (%block_14); ]; + block %block_14 { .asm = "mov x16, x1" } [ + var lv_9:bv64 := 0x0:bv64; + var lv_9:bv64 := 0x0:bv64; + var lv_10:bv64 := 0x0:bv64; + var lv_10:bv64 := $R1; + $R16:bv64 := bvor(lv_9:bv64, bvshl(lv_10:bv64, zero_extend(52, 0x0:bv12))); + (var BranchTaken:bool := false, $PC:bv64 := 0x400708:bv64); + goto (%block_15); + ]; + block %block_15 { .asm = "br x16" } [ + var lv_11:bv64 := 0x0:bv64; + var BTypeNext:bv2 := 0x1:bv2; + var BranchTaken:bool := true; + $PC:bv64 := $R16; + goto (%deregister_tm_clones_code_7); + ]; + block %deregister_tm_clones_code_7 [ assert boolor(); unreachable; ]; block %deregister_tm_clones_code_3 { .address = 4196108; .gtirb_block = "cdQ2GS2+QhaOa7OUvPWMRQ"; .succ = [ { .address = 4196200; .conditional = "false"; .direct = "true"; .target = "external:TxTRm4kpQiq/Xgistx+xbQ"; .type = "Type_Return" } ] } [ assume eq(0x40070c:bv64, $PC); - call @_aarch64_eval(0xd65f03c0:bv32, 0x40070c:bv64) { .asm = "ret " }; + goto (%block_16); + ]; + block %block_16 { .asm = "ret " } [ + var lv_12:bv64 := 0x0:bv64; + var BTypeNext:bv2 := 0x0:bv2; + var BranchTaken:bool := true; + $PC:bv64 := $R30; + goto (%deregister_tm_clones_code_8); + ]; + block %deregister_tm_clones_code_8 [ assert boolor(eq(0x400768:bv64, $PC)); goto (%ret_5); ]; block %ret_5 [ return; ] ]; proc @FUN_400620() -> () { } + modifies $PC:bv64, $R16:bv64, $R17:bv64, $SP:bv64, $mem:(bv64->bv8) + captures $PC:bv64, $R16:bv64, $R17:bv64, $R30:bv64, $SP:bv64, $mem:(bv64->bv8) requires boolor(eq(0x400620:bv64, $PC)) [ @@ -557,46 +1518,67 @@ .succ = [ { .conditional = "false"; .direct = "false"; .target = "proxy:P8unZs8jR1SVxJeeo8n1sg"; .type = "Type_Branch" } ] } [ assume eq(0x400620:bv64, $PC); - call @_aarch64_eval(0xa9bf7bf0:bv32, 0x400620:bv64) { .asm = "stp x16, x30, [sp, #-0x10]!" }; - call @_aarch64_eval(0xf00000f0:bv32, 0x400624:bv64) { .asm = "adrp x16, #0x1f000" }; - call @_aarch64_eval(0xf947fe11:bv32, 0x400628:bv64) { .asm = "ldr x17, [x16, #0xff8]" }; - call @_aarch64_eval(0x913fe210:bv32, 0x40062c:bv64) { .asm = "add x16, x16, #0xff8" }; - call @_aarch64_eval(0xd61f0220:bv32, 0x400630:bv64) { .asm = "br x17" }; - assert boolor(); - unreachable; - ] + goto (%block); + ]; + block %block { .asm = "stp x16, x30, [sp, #-0x10]!" } [ + var lv:bv64 := 0x0:bv64; + var lv:bv64 := $SP; + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd($SP, + 0xfffffffffffffff0:bv64) $R16 64; + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd(bvadd($SP, + 0xfffffffffffffff0:bv64), 0x8:bv64) $R30 64; + $SP:bv64 := bvadd(lv:bv64, 0xfffffffffffffff0:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x400624:bv64); + goto (%block_1); + ]; + block %block_1 { .asm = "adrp x16, #0x1f000" } [ + $R16:bv64 := 0x41f000:bv64; + (var BranchTaken:bool := false, $PC:bv64 := 0x400628:bv64); + goto (%block_2); + ]; + block %block_2 { .asm = "ldr x17, [x16, #0xff8]" } [ + var lv_1:bv64 := 0x0:bv64; + var lv_1:bv64 := $R16; + var lv_2:bv64 := 0x0:bv64; + var lv_3:bv64 := load le $mem:(bv64->bv8) bvadd(lv_1:bv64, 0xff8:bv64) 64; + var lv_2:bv64 := lv_3:bv64; + $R17:bv64 := zero_extend(0, zero_extend(0, lv_2:bv64)); + (var BranchTaken:bool := false, $PC:bv64 := 0x40062c:bv64); + goto (%block_3); + ]; + block %block_3 { .asm = "add x16, x16, #0xff8" } [ + var lv_4:bv64 := 0x0:bv64; + var lv_5:bv64 := 0x0:bv64; + var lv_5:bv64 := $R16; + $R16:bv64 := bvadd(lv_5:bv64, 0xff8:bv64); + (var BranchTaken:bool := false, $PC:bv64 := 0x400630:bv64); + goto (%block_4); + ]; + block %block_4 { .asm = "br x17" } [ + var lv_6:bv64 := 0x0:bv64; + var BTypeNext:bv2 := 0x1:bv2; + var BranchTaken:bool := true; + $PC:bv64 := $R17; + goto (%FUN_400620_code_1); + ]; + block %FUN_400620_code_1 [ assert boolor(); unreachable; ] ]; - prog entry @_start;(load-il gtirb-output.il) - (dump-il dumped.il) - $ diff gtirb-output.il dumped.il - 2a3 - > captures $PC:bv64 - 29a31 - > captures $PC:bv64 - 62a65 - > captures $PC:bv64 - 122a126 - > captures $PC:bv64 - 181a186 - > captures $PC:bv64 - 201a207 - > captures $PC:bv64 - 218a225 - > captures $PC:bv64 - 311a319 - > captures $PC:bv64 - 357a366 - > captures $PC:bv64 - 372a382 - > captures $PC:bv64 - 416a427 - > captures $PC:bv64 - 451a463 - > captures $PC:bv64 - 468a481 - > captures $PC:bv64 - 485a499 - > captures $PC:bv64 - 541a556 - > captures $PC:bv64 - [1] + var observable $mem:(bv64->bv8); + var $SP:bv64; + var $R0:bv64; + var $R1:bv64; + var $R2:bv64; + var $R3:bv64; + var $R4:bv64; + var $R5:bv64; + var $R6:bv64; + var $R16:bv64; + var $R17:bv64; + var $R19:bv64; + var $R29:bv64; + var $R30:bv64; + var $PSTATE_N:bv1; + var $PSTATE_Z:bv1; + var $PSTATE_V:bv1; + prog entry @_start; + diff --git a/test/cram/malloc_free.t b/test/cram/malloc_free.t index e89c58a2..0608b7c2 100644 --- a/test/cram/malloc_free.t +++ b/test/cram/malloc_free.t @@ -132,7 +132,7 @@ procedure p$main_2276(R0_in: bv64, R16_in: bv64, R17_in: bv64, R1_in: bv64, R29_in: bv64, R30_in: bv64, R31_in: bv64, _PC_in: bv64) returns (R0_out: bv64, R17_out: bv64, R1_out: bv64, R29_out: bv64, R30_out: bv64); - modifies $mem_encoding, $mem, $stack; + modifies $mem, $mem_encoding, $stack; ensures {:msg "Memory Error: Memory Leak"} (forall i: bv64 :: @@ -216,13 +216,13 @@ return; } procedure p$malloc(R0_in: bv64) returns (R0_out: bv64); - modifies $mem_encoding, $mem, $stack; + modifies $mem, $mem_encoding, $stack; ensures $me_can_allocate(old($mem_encoding), R0_out, R0_in); ensures ($me_addr_offset($mem_encoding, R0_out) == 0bv64); ensures ($me_alloc_base($mem_encoding, $me_addr_alloc($mem_encoding, R0_out)) == R0_out); ensures $me_allocate(old($mem_encoding), $mem_encoding, R0_out, R0_in); procedure p$#free(R0_in: bv64); - modifies $mem_encoding, $mem, $stack; + modifies $mem, $mem_encoding, $stack; ensures {:msg "Memory Error: Invalid Free"} ($mem_encoding == $me_alloc_live_update( old($mem_encoding), $me_addr_alloc(old($mem_encoding), R0_in), @@ -369,7 +369,7 @@ procedure p$main_2276(R0_in: bv64, R16_in: bv64, R17_in: bv64, R1_in: bv64, R29_in: bv64, R30_in: bv64, R31_in: bv64, _PC_in: bv64) returns (R0_out: bv64, R17_out: bv64, R1_out: bv64, R29_out: bv64, R30_out: bv64); - modifies $mem_encoding, $mem, $stack; + modifies $mem, $mem_encoding, $stack; ensures {:msg "Memory Error: Memory Leak"} (forall i: bv64 :: @@ -453,13 +453,13 @@ return; } procedure p$malloc(R0_in: bv64) returns (R0_out: bv64); - modifies $mem_encoding, $mem, $stack; + modifies $mem, $mem_encoding, $stack; ensures $me_can_allocate(old($mem_encoding), R0_out, R0_in); ensures ($me_addr_offset($mem_encoding, R0_out) == 0bv64); ensures ($me_alloc_base($mem_encoding, $me_addr_alloc($mem_encoding, R0_out)) == R0_out); ensures $me_allocate(old($mem_encoding), $mem_encoding, R0_out, R0_in); procedure p$#free(R0_in: bv64); - modifies $mem_encoding, $mem, $stack; + modifies $mem, $mem_encoding, $stack; ensures {:msg "Memory Error: Invalid Free"} ($mem_encoding == $me_alloc_live_update( old($mem_encoding), $me_addr_alloc(old($mem_encoding), R0_in), diff --git a/test/cram/sva.t b/test/cram/sva.t index 1a7167f1..b4be47cb 100644 --- a/test/cram/sva.t +++ b/test/cram/sva.t @@ -2,4 +2,4 @@ (load-il ../../examples/irreducible_loop_1.il) (run-transforms ssa sva) (CF_in->(Par(@puts_1584_{ Var.V.name = "CF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), NF_in->(Par(@puts_1584_{ Var.V.name = "NF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_in->(Par(@puts_1584_{ Var.V.name = "R0_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_in->(Par(@puts_1584_{ Var.V.name = "R1_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_in->(Par(@puts_1584_{ Var.V.name = "R29_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_in->(Par(@puts_1584_{ Var.V.name = "R30_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_in->(Stack(@puts_1584)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), VF_in->(Par(@puts_1584_{ Var.V.name = "VF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), ZF_in->(Par(@puts_1584_{ Var.V.name = "ZF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), _->⊥) - (CF_in->(Par(@main_1876_{ Var.V.name = "CF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), NF_in->(Par(@main_1876_{ Var.V.name = "NF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_in->(Par(@main_1876_{ Var.V.name = "R0_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_in->(Par(@main_1876_{ Var.V.name = "R1_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_in->(Par(@main_1876_{ Var.V.name = "R29_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_in->(Par(@main_1876_{ Var.V.name = "R30_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_in->(Stack(@main_1876)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), VF_in->(Par(@main_1876_{ Var.V.name = "VF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), ZF_in->(Par(@main_1876_{ Var.V.name = "ZF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), CF_out->(Ret(@puts_1584_{ Var.V.name = "CF_8"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), NF_out->(Ret(@puts_1584_{ Var.V.name = "NF_8"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_out->(Constant->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_out->(Ret(@puts_1584_{ Var.V.name = "R1_7"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_out->(Loaded(load21_1)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_out->(Loaded(load22_1)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_out->(Ret(@puts_1584_{ Var.V.name = "R31_7"; typ = bv64; scope = Var.LocalVar })->⟦0x20:bv64, 0x20:bv64⟧, _->⊥), VF_out->(Ret(@puts_1584_{ Var.V.name = "VF_8"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), ZF_out->(Ret(@puts_1584_{ Var.V.name = "ZF_12"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), CF_1->(Par(@main_1876_{ Var.V.name = "CF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), NF_1->(Par(@main_1876_{ Var.V.name = "NF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_1->(Par(@main_1876_{ Var.V.name = "R0_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_1->(Par(@main_1876_{ Var.V.name = "R1_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_1->(Par(@main_1876_{ Var.V.name = "R29_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_1->(Par(@main_1876_{ Var.V.name = "R30_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_1->(Stack(@main_1876)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), VF_1->(Par(@main_1876_{ Var.V.name = "VF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), ZF_1->(Par(@main_1876_{ Var.V.name = "ZF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), #4_1->(Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, _->⊥), R31_2->(Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, _->⊥), R29_2->(Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, _->⊥), R0_2->(Constant->⟦0x20000:bv64, 0x20000:bv64⟧, _->⊥), R0_3->(Constant->⟦0x2003c:bv64, 0x2003c:bv64⟧, _->⊥), R0_4->(Constant->⟦0x20000:bv64, 0x20000:bv64⟧, _->⊥), R0_5->(Constant->⟦0x20040:bv64, 0x20040:bv64⟧, _->⊥), load18_1->(Loaded(load18_1)->⟦0x0:bv32, 0x0:bv32⟧, _->⊥), R0_6->(Loaded(load18_1)->⊤, _->⊥), R0_7->(Loaded(load18_1)->⊤, _->⊥), #5_1->(Loaded(load18_1)->⊤, _->⊥), VF_2->(Loaded(load18_1)->⊤, _->⊥), CF_2->(Loaded(load18_1)->⊤, _->⊥), ZF_2->(Loaded(load18_1)->⊤, _->⊥), NF_2->(Loaded(load18_1)->⊤, _->⊥), ZF_3->(Loaded(load18_1)->⊤, _->⊥), ZF_4->(Loaded(load18_1)->⊤, _->⊥), ZF_5->(Ret(@puts_1584_{ Var.V.name = "ZF_10"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, Loaded(load18_1)->⊤, _->⊥), VF_3->(Ret(@puts_1584_{ Var.V.name = "VF_7"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, Loaded(load18_1)->⊤, _->⊥), R31_3->(Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, Ret(@puts_1584_{ Var.V.name = "R31_6"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_3->(Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, Ret(@puts_1584_{ Var.V.name = "R29_6"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_2->(Loaded(load19_1)->⊤, Par(@main_1876_{ Var.V.name = "R1_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), NF_3->(Ret(@puts_1584_{ Var.V.name = "NF_7"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, Loaded(load18_1)->⊤, _->⊥), CF_3->(Ret(@puts_1584_{ Var.V.name = "CF_7"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, Loaded(load18_1)->⊤, _->⊥), R0_8->(Constant->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R0_9->(Constant->⟦0x820:bv64, 0x820:bv64⟧, _->⊥), R30_2->(Constant->⟦0x7d0:bv64, 0x7d0:bv64⟧, _->⊥), CF_4->(Ret(@puts_1584_{ Var.V.name = "CF_4"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), NF_4->(Ret(@puts_1584_{ Var.V.name = "NF_4"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_10->(Ret(@puts_1584_{ Var.V.name = "R0_10"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_3->(Ret(@puts_1584_{ Var.V.name = "R1_3"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_4->(Ret(@puts_1584_{ Var.V.name = "R29_4"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_3->(Ret(@puts_1584_{ Var.V.name = "R30_3"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_4->(Ret(@puts_1584_{ Var.V.name = "R31_4"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), VF_4->(Ret(@puts_1584_{ Var.V.name = "VF_4"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), ZF_6->(Ret(@puts_1584_{ Var.V.name = "ZF_6"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_11->(Constant->⟦0x20000:bv64, 0x20000:bv64⟧, _->⊥), R0_12->(Constant->⟦0x2003c:bv64, 0x2003c:bv64⟧, _->⊥), load20_1->(Loaded(load20_1)->⟦0x0:bv32, 0x0:bv32⟧, _->⊥), R0_13->(Loaded(load20_1)->⊤, _->⊥), #6_1->(Loaded(load20_1)->⊤, _->⊥), VF_5->(Loaded(load20_1)->⊤, _->⊥), CF_5->(Loaded(load20_1)->⊤, _->⊥), ZF_7->(Loaded(load20_1)->⊤, _->⊥), NF_5->(Loaded(load20_1)->⊤, _->⊥), ZF_8->(Loaded(load20_1)->⊤, _->⊥), ZF_9->(Loaded(load20_1)->⊤, Loaded(load18_1)->⊤, _->⊥), VF_6->(Loaded(load20_1)->⊤, Loaded(load18_1)->⊤, _->⊥), R31_5->(Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, Ret(@puts_1584_{ Var.V.name = "R31_4"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_5->(Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, Ret(@puts_1584_{ Var.V.name = "R29_4"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_4->(Par(@main_1876_{ Var.V.name = "R1_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, Ret(@puts_1584_{ Var.V.name = "R1_3"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), NF_6->(Loaded(load20_1)->⊤, Loaded(load18_1)->⊤, _->⊥), CF_6->(Loaded(load20_1)->⊤, Loaded(load18_1)->⊤, _->⊥), R0_14->(Constant->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R0_15->(Constant->⟦0x820:bv64, 0x820:bv64⟧, _->⊥), R30_4->(Constant->⟦0x7a0:bv64, 0x7a0:bv64⟧, _->⊥), CF_7->(Ret(@puts_1584_{ Var.V.name = "CF_7"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), NF_7->(Ret(@puts_1584_{ Var.V.name = "NF_7"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_16->(Ret(@puts_1584_{ Var.V.name = "R0_16"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_5->(Ret(@puts_1584_{ Var.V.name = "R1_5"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_6->(Ret(@puts_1584_{ Var.V.name = "R29_6"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_5->(Ret(@puts_1584_{ Var.V.name = "R30_5"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_6->(Ret(@puts_1584_{ Var.V.name = "R31_6"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), VF_7->(Ret(@puts_1584_{ Var.V.name = "VF_7"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), ZF_10->(Ret(@puts_1584_{ Var.V.name = "ZF_10"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_17->(Constant->⟦0x20000:bv64, 0x20000:bv64⟧, _->⊥), R0_18->(Constant->⟦0x2003c:bv64, 0x2003c:bv64⟧, _->⊥), load19_1->(Loaded(load19_1)->⟦0x0:bv32, 0x0:bv32⟧, _->⊥), R0_19->(Loaded(load19_1)->⊤, _->⊥), R1_6->(Loaded(load19_1)->⊤, _->⊥), R0_20->(Constant->⟦0x20000:bv64, 0x20000:bv64⟧, _->⊥), R0_21->(Constant->⟦0x2003c:bv64, 0x2003c:bv64⟧, _->⊥), ZF_11->(Loaded(load20_1)->⊤, _->⊥), R0_22->(Constant->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R0_23->(Constant->⟦0x828:bv64, 0x828:bv64⟧, _->⊥), R30_6->(Constant->⟦0x7f4:bv64, 0x7f4:bv64⟧, _->⊥), CF_8->(Ret(@puts_1584_{ Var.V.name = "CF_8"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), NF_8->(Ret(@puts_1584_{ Var.V.name = "NF_8"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_24->(Ret(@puts_1584_{ Var.V.name = "R0_24"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_7->(Ret(@puts_1584_{ Var.V.name = "R1_7"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_7->(Ret(@puts_1584_{ Var.V.name = "R29_7"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_7->(Ret(@puts_1584_{ Var.V.name = "R30_7"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_7->(Ret(@puts_1584_{ Var.V.name = "R31_7"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), VF_8->(Ret(@puts_1584_{ Var.V.name = "VF_8"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), ZF_12->(Ret(@puts_1584_{ Var.V.name = "ZF_12"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_25->(Constant->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), load21_1->(Loaded(load21_1)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_8->(Loaded(load21_1)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), load22_1->(Loaded(load22_1)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_8->(Loaded(load22_1)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_8->(Ret(@puts_1584_{ Var.V.name = "R31_7"; typ = bv64; scope = Var.LocalVar })->⟦0x20:bv64, 0x20:bv64⟧, _->⊥), _->⊥) + (CF_in->(Par(@main_1876_{ Var.V.name = "CF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), NF_in->(Par(@main_1876_{ Var.V.name = "NF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_in->(Par(@main_1876_{ Var.V.name = "R0_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_in->(Par(@main_1876_{ Var.V.name = "R1_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_in->(Par(@main_1876_{ Var.V.name = "R29_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_in->(Par(@main_1876_{ Var.V.name = "R30_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_in->(Stack(@main_1876)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), VF_in->(Par(@main_1876_{ Var.V.name = "VF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), ZF_in->(Par(@main_1876_{ Var.V.name = "ZF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), CF_out->(Ret(@puts_1584_{ Var.V.name = "CF_8"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), NF_out->(Ret(@puts_1584_{ Var.V.name = "NF_8"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_out->(Constant->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_out->(Ret(@puts_1584_{ Var.V.name = "R1_7"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_out->(Loaded(load21_1)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_out->(Loaded(load22_1)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_out->(Ret(@puts_1584_{ Var.V.name = "R31_7"; typ = bv64; scope = Var.LocalVar })->⟦0x20:bv64, 0x20:bv64⟧, _->⊥), VF_out->(Ret(@puts_1584_{ Var.V.name = "VF_8"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), ZF_out->(Ret(@puts_1584_{ Var.V.name = "ZF_12"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), CF_1->(Par(@main_1876_{ Var.V.name = "CF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), NF_1->(Par(@main_1876_{ Var.V.name = "NF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_1->(Par(@main_1876_{ Var.V.name = "R0_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_1->(Par(@main_1876_{ Var.V.name = "R1_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_1->(Par(@main_1876_{ Var.V.name = "R29_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_1->(Par(@main_1876_{ Var.V.name = "R30_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_1->(Stack(@main_1876)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), VF_1->(Par(@main_1876_{ Var.V.name = "VF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), ZF_1->(Par(@main_1876_{ Var.V.name = "ZF_in"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), #4_1->(Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, _->⊥), R31_2->(Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, _->⊥), R29_2->(Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, _->⊥), R0_2->(Constant->⟦0x20000:bv64, 0x20000:bv64⟧, _->⊥), R0_3->(Constant->⟦0x2003c:bv64, 0x2003c:bv64⟧, _->⊥), R0_4->(Constant->⟦0x20000:bv64, 0x20000:bv64⟧, _->⊥), R0_5->(Constant->⟦0x20040:bv64, 0x20040:bv64⟧, _->⊥), load18_1->(Loaded(load18_1)->⟦0x0:bv32, 0x0:bv32⟧, _->⊥), R0_6->(Loaded(load18_1)->⊤, _->⊥), R0_7->(Loaded(load18_1)->⊤, _->⊥), #5_1->(Loaded(load18_1)->⊤, _->⊥), VF_2->(Loaded(load18_1)->⊤, _->⊥), CF_2->(Loaded(load18_1)->⊤, _->⊥), ZF_2->(Loaded(load18_1)->⊤, _->⊥), NF_2->(Loaded(load18_1)->⊤, _->⊥), ZF_3->(Loaded(load18_1)->⊤, _->⊥), ZF_4->(Loaded(load18_1)->⊤, _->⊥), ZF_5->(Ret(@puts_1584_{ Var.V.name = "ZF_10"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, Loaded(load18_1)->⊤, _->⊥), VF_3->(Ret(@puts_1584_{ Var.V.name = "VF_7"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, Loaded(load18_1)->⊤, _->⊥), R31_3->(Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, Ret(@puts_1584_{ Var.V.name = "R31_6"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_3->(Ret(@puts_1584_{ Var.V.name = "R29_6"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, _->⊥), R1_2->(Loaded(load19_1)->⊤, Par(@main_1876_{ Var.V.name = "R1_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), NF_3->(Ret(@puts_1584_{ Var.V.name = "NF_7"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, Loaded(load18_1)->⊤, _->⊥), CF_3->(Ret(@puts_1584_{ Var.V.name = "CF_7"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, Loaded(load18_1)->⊤, _->⊥), R0_8->(Constant->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R0_9->(Constant->⟦0x820:bv64, 0x820:bv64⟧, _->⊥), R30_2->(Constant->⟦0x7d0:bv64, 0x7d0:bv64⟧, _->⊥), CF_4->(Ret(@puts_1584_{ Var.V.name = "CF_4"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), NF_4->(Ret(@puts_1584_{ Var.V.name = "NF_4"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_10->(Ret(@puts_1584_{ Var.V.name = "R0_10"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_3->(Ret(@puts_1584_{ Var.V.name = "R1_3"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_4->(Ret(@puts_1584_{ Var.V.name = "R29_4"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_3->(Ret(@puts_1584_{ Var.V.name = "R30_3"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_4->(Ret(@puts_1584_{ Var.V.name = "R31_4"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), VF_4->(Ret(@puts_1584_{ Var.V.name = "VF_4"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), ZF_6->(Ret(@puts_1584_{ Var.V.name = "ZF_6"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_11->(Constant->⟦0x20000:bv64, 0x20000:bv64⟧, _->⊥), R0_12->(Constant->⟦0x2003c:bv64, 0x2003c:bv64⟧, _->⊥), load20_1->(Loaded(load20_1)->⟦0x0:bv32, 0x0:bv32⟧, _->⊥), R0_13->(Loaded(load20_1)->⊤, _->⊥), #6_1->(Loaded(load20_1)->⊤, _->⊥), VF_5->(Loaded(load20_1)->⊤, _->⊥), CF_5->(Loaded(load20_1)->⊤, _->⊥), ZF_7->(Loaded(load20_1)->⊤, _->⊥), NF_5->(Loaded(load20_1)->⊤, _->⊥), ZF_8->(Loaded(load20_1)->⊤, _->⊥), ZF_9->(Loaded(load18_1)->⊤, Loaded(load20_1)->⊤, _->⊥), VF_6->(Loaded(load18_1)->⊤, Loaded(load20_1)->⊤, _->⊥), R31_5->(Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, Ret(@puts_1584_{ Var.V.name = "R31_4"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_5->(Ret(@puts_1584_{ Var.V.name = "R29_4"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, Stack(@main_1876)->⟦0xffffffffffffffe0:bv64, 0xffffffffffffffe0:bv64⟧, _->⊥), R1_4->(Ret(@puts_1584_{ Var.V.name = "R1_3"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, Par(@main_1876_{ Var.V.name = "R1_in"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), NF_6->(Loaded(load18_1)->⊤, Loaded(load20_1)->⊤, _->⊥), CF_6->(Loaded(load18_1)->⊤, Loaded(load20_1)->⊤, _->⊥), R0_14->(Constant->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R0_15->(Constant->⟦0x820:bv64, 0x820:bv64⟧, _->⊥), R30_4->(Constant->⟦0x7a0:bv64, 0x7a0:bv64⟧, _->⊥), CF_7->(Ret(@puts_1584_{ Var.V.name = "CF_7"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), NF_7->(Ret(@puts_1584_{ Var.V.name = "NF_7"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_16->(Ret(@puts_1584_{ Var.V.name = "R0_16"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_5->(Ret(@puts_1584_{ Var.V.name = "R1_5"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_6->(Ret(@puts_1584_{ Var.V.name = "R29_6"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_5->(Ret(@puts_1584_{ Var.V.name = "R30_5"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_6->(Ret(@puts_1584_{ Var.V.name = "R31_6"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), VF_7->(Ret(@puts_1584_{ Var.V.name = "VF_7"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), ZF_10->(Ret(@puts_1584_{ Var.V.name = "ZF_10"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_17->(Constant->⟦0x20000:bv64, 0x20000:bv64⟧, _->⊥), R0_18->(Constant->⟦0x2003c:bv64, 0x2003c:bv64⟧, _->⊥), load19_1->(Loaded(load19_1)->⟦0x0:bv32, 0x0:bv32⟧, _->⊥), R0_19->(Loaded(load19_1)->⊤, _->⊥), R1_6->(Loaded(load19_1)->⊤, _->⊥), R0_20->(Constant->⟦0x20000:bv64, 0x20000:bv64⟧, _->⊥), R0_21->(Constant->⟦0x2003c:bv64, 0x2003c:bv64⟧, _->⊥), ZF_11->(Loaded(load20_1)->⊤, _->⊥), R0_22->(Constant->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R0_23->(Constant->⟦0x828:bv64, 0x828:bv64⟧, _->⊥), R30_6->(Constant->⟦0x7f4:bv64, 0x7f4:bv64⟧, _->⊥), CF_8->(Ret(@puts_1584_{ Var.V.name = "CF_8"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), NF_8->(Ret(@puts_1584_{ Var.V.name = "NF_8"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_24->(Ret(@puts_1584_{ Var.V.name = "R0_24"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R1_7->(Ret(@puts_1584_{ Var.V.name = "R1_7"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_7->(Ret(@puts_1584_{ Var.V.name = "R29_7"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_7->(Ret(@puts_1584_{ Var.V.name = "R30_7"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_7->(Ret(@puts_1584_{ Var.V.name = "R31_7"; typ = bv64; scope = Var.LocalVar })->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), VF_8->(Ret(@puts_1584_{ Var.V.name = "VF_8"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), ZF_12->(Ret(@puts_1584_{ Var.V.name = "ZF_12"; typ = bv1; scope = Var.LocalVar })->⟦0x0:bv1, 0x0:bv1⟧, _->⊥), R0_25->(Constant->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), load21_1->(Loaded(load21_1)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_8->(Loaded(load21_1)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), load22_1->(Loaded(load22_1)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_8->(Loaded(load22_1)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R31_8->(Ret(@puts_1584_{ Var.V.name = "R31_7"; typ = bv64; scope = Var.LocalVar })->⟦0x20:bv64, 0x20:bv64⟧, _->⊥), _->⊥) diff --git a/test/transforms/test_aslp.ml b/test/transforms/test_aslp.ml index f73da071..12645eca 100644 --- a/test/transforms/test_aslp.ml +++ b/test/transforms/test_aslp.ml @@ -28,7 +28,7 @@ let%expect_test "lift: add x1, x2, x3, lsl #4" = stmts = [var var_0:bv64 := 0x0:bv64; var var_0:bv64 := $R2; var var_1:bv64 := 0x0:bv64; var var_1:bv64 := $R3; - $R1:bv64 := bvadd(var_0:bv64, bvshl(var_1:bv64, 0x4:bv12)); + $R1:bv64 := bvadd(var_0:bv64, bvshl(var_1:bv64, zero_extend(52, 0x4:bv12))); (var BranchTaken:bool := false, $PC:bv64 := 0x2004:bv64)]; pc_assign = (Some 0x2004:bv64) }) |}] @@ -108,7 +108,7 @@ let%expect_test "lift: b #16" = stmts = [var var_0:bv64 := 0x0:bv64; var var_0:bv64 := $R2; var var_1:bv64 := 0x0:bv64; var var_1:bv64 := $R3; - $R1:bv64 := bvadd(var_0:bv64, bvshl(var_1:bv64, 0x4:bv12)); + $R1:bv64 := bvadd(var_0:bv64, bvshl(var_1:bv64, zero_extend(52, 0x4:bv12))); (var BranchTaken:bool := false, $PC:bv64 := 0x2004:bv64)]; pc_assign = (Some 0x2004:bv64) }) |}] @@ -154,7 +154,9 @@ proc @main() -> () { } var observable $mem:(bv64->bv8); var $PC:bv64; proc @main() -> () { } - captures $PC:bv64 + modifies $PC:bv64, $R0:bv64, $R29:bv64, $R30:bv64, $SP:bv64, $mem:(bv64->bv8) + captures $PC:bv64, $R0:bv64, $R1:bv64, $R29:bv64, $R30:bv64, $SP:bv64, + $mem:(bv64->bv8) requires boolor(eq(0x400808:bv64, $PC)) [ @@ -165,37 +167,37 @@ proc @main() -> () { } goto (%block); ]; block %block { .asm = "stp x29, x30, [sp, #-0x20]!" } [ - var var:bv64 := 0x0:bv64; - var var:bv64 := $SP; + var lv:bv64 := 0x0:bv64; + var lv:bv64 := $SP; $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd($SP, - 0xffffffffffffffe0:bv64) $R29 8; + 0xffffffffffffffe0:bv64) $R29 64; $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd(bvadd($SP, - 0xffffffffffffffe0:bv64), 0x8:bv64) $R30 8; - $SP:bv64 := bvadd(var:bv64, 0xffffffffffffffe0:bv64); + 0xffffffffffffffe0:bv64), 0x8:bv64) $R30 64; + $SP:bv64 := bvadd(lv:bv64, 0xffffffffffffffe0:bv64); (var BranchTaken:bool := false, $PC:bv64 := 0x40080c:bv64); goto (%block_1); ]; block %block_1 { .asm = "mov x29, sp" } [ - var var_1:bv64 := 0x0:bv64; + var lv_1:bv64 := 0x0:bv64; $R29:bv64 := bvadd($SP, 0x0:bv64); (var BranchTaken:bool := false, $PC:bv64 := 0x400810:bv64); goto (%block_2); ]; block %block_2 { .asm = "str w0, [sp, #0x1c]" } [ - $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd($SP, 0x1c:bv64) extract(-32,0, $R0) 4; + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd($SP, 0x1c:bv64) extract(32,0, $R0) 32; (var BranchTaken:bool := false, $PC:bv64 := 0x400814:bv64); goto (%block_3); ]; block %block_3 { .asm = "str x1, [sp, #0x10]" } [ - $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd($SP, 0x10:bv64) $R1 8; + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) bvadd($SP, 0x10:bv64) $R1 64; (var BranchTaken:bool := false, $PC:bv64 := 0x400818:bv64); goto (%block_4); ]; block %block_4 { .asm = "ldrsw x0, [sp, #0x1c]" } [ - var var_2:bv32 := 0x0:bv32; - $mem:(bv64->bv8) := load le var_3:bv4 bvadd($SP, 0x1c:bv64) 4; - var var_2:bv32 := var_3:bv4; - $R0:bv64 := zero_extend(0, sign_extend(32, var_2:bv32)); + var lv_2:bv32 := 0x0:bv32; + var lv_3:bv32 := load le $mem:(bv64->bv8) bvadd($SP, 0x1c:bv64) 32; + var lv_2:bv32 := lv_3:bv32; + $R0:bv64 := zero_extend(0, sign_extend(32, lv_2:bv32)); (var BranchTaken:bool := false, $PC:bv64 := 0x40081c:bv64); goto (%block_5); ]; @@ -257,7 +259,8 @@ proc @Sqrt() -> () { } var observable $mem:(bv64->bv8); var $PC:bv64; proc @Sqrt() -> () { } - captures $PC:bv64 + modifies $PC:bv64 + captures $PC:bv64, $PSTATE_N:bv1, $PSTATE_V:bv1 [ block %Sqrt_code_4 { .address = 4196316 } [ @@ -329,6 +332,7 @@ proc @main() -> () { } var observable $mem:(bv64->bv8); var $PC:bv64; proc @main() -> () { } + modifies $PC:bv64 captures $PC:bv64 requires boolor(eq(0x400808:bv64, $PC)) @@ -342,8 +346,8 @@ proc @main() -> () { } goto (%block); ]; block %block { .asm = "mov xzr, xzr" } [ - var var:bv64 := 0x0:bv64; - var var_1:bv64 := 0x0:bv64; + var lv:bv64 := 0x0:bv64; + var lv_1:bv64 := 0x0:bv64; (var BranchTaken:bool := false, $PC:bv64 := 0x400810:bv64); goto (%ret_1); ];