Question: how isla bind the arch level's registers and IR variables

[msuadOf]

How isla bind the arch level's registers (eg. mstatus in RV & VBAR_EL2 in ARM) and IR variables(eg. zz40:%i in xxx.ir)?

[bacam]

The bindings are similar to Sail - registers have declarations, with optional initialisers. By default Isla will run initialisers, but this can be turned off with a command line option, and the values can also be overridden by command line options. For example, mstatus is initialised like this.

However, some registers are initialised by model-specific code. VBAR_EL2 is an example, and is initialised by (e.g.) the isla_footprint function in arm-v9.4-a/src/isla_main.sail in the sail-arm repository.

[msuadOf]

As far as I dig into isla, I find it more interesting to use it for symbolic.

I have some new questions now.

• How can I get the symbolic vars solved? for examle, transfer a Val with some sym inside into a concrete Val like Val::I64
• How can I deal with enum? it seems some problem with enum when I transfer enum from solver. And is something wrong with the way I use it?

Anyway, thank you for your help!

[bacam]

You can see some example code in our test generator at https://github.com/rems-project/isla-testgen/blob/master/src/extract_state.rs#L107. Note that sometimes the solver doesn't return anything - this means that the value is unconstrained and you could pick any concrete value you like. That code doesn't handle enums, though.

I can't quite remember the correct way to handle enums at the moment, but I think you need to look them up in the type_info part of the shared state.

[msuadOf]

Enum really trubles me.

Here is the code. The reason why the enum cannot get the correct member is the value func_decl and *member is set in a wrong way, for example, a deault value(I meant to get member=3,but get member=0).

Can you tell me is it worked in some old version? Or, fix it? Even more, If you did not plan to fix it, tell me how to fix it, I will try to do that.

I have found the comment here, maybe the problem is related to it.

[msuadOf]

I found the lib https://crates.io/crates/z3 it provides z3-solver and z3-sys. z3-sys is already used in isla, but z3-solver not. Why not use that to provide enum support?

[bacam]

I don't understand what the failure that you're seeing is. I tried writing a little test to ensure that we can get non-zero member values back from the solver, and it appears to work:

    #[test]
    fn more_enums() {
        let mut cfg = Config::new();
        cfg.set_param_value("model", "true");
        let ctx = Context::new(cfg);
        let mut solver = Solver::<B64>::new(&ctx);
        let e = solver.get_enum(Name::from_u32(0), 3);
        let v = solver.declare_const(Ty::Enum(e), SourceLoc::unknown());
        solver.assert(Exp::Neq(Box::new(Exp::Var(v)), Box::new(Exp::Enum(EnumMember { enum_id: EnumId::from_name(Name::from_u32(0)), member: 0 }))));
        assert!(solver.check_sat(SourceLoc::unknown()) == Sat);
        let mut model = Model::new(&solver);
        let model_exp = model.get_var(v).unwrap().unwrap_exp();
        match model_exp {
            Exp::Enum(m) => {
                assert_eq!(m.enum_id.to_name(), Name::from_u32(0));
                assert!(m.member != 0);
            }
            _ => panic!("Model did not return a constant"),
        }
    }

Do you have an example that fails that I could look at?

[Alasdair]

I found the lib https://crates.io/crates/z3 it provides z3-solver and z3-sys. z3-sys is already used in isla, but z3-solver not. Why not use that to provide enum support?

z3-sys is the low level API the directly mirrors the z3 C API.

The way enumerations work is a little bit tricky, because we construct (Z3) enumeration types in the Isla solver type on the fly as they are used by the Sail source, so each trace ends up only containing the enumeration types it uses. It might have been better to pre-initialise all the enumeration types from the model, but the representation went through a few refactors, where initially there were generic N-element types created that were used for all enums of the same size.

[msuadOf]

I don't understand what the failure that you're seeing is. I tried writing a little test to ensure that we can get non-zero member values back from the solver, and it appears to work:

    #[test]
    fn more_enums() {
        let mut cfg = Config::new();
        cfg.set_param_value("model", "true");
        let ctx = Context::new(cfg);
        let mut solver = Solver::<B64>::new(&ctx);
        let e = solver.get_enum(Name::from_u32(0), 3);
        let v = solver.declare_const(Ty::Enum(e), SourceLoc::unknown());
        solver.assert(Exp::Neq(Box::new(Exp::Var(v)), Box::new(Exp::Enum(EnumMember { enum_id: EnumId::from_name(Name::from_u32(0)), member: 0 }))));
        assert!(solver.check_sat(SourceLoc::unknown()) == Sat);
        let mut model = Model::new(&solver);
        let model_exp = model.get_var(v).unwrap().unwrap_exp();
        match model_exp {
            Exp::Enum(m) => {
                assert_eq!(m.enum_id.to_name(), Name::from_u32(0));
                assert!(m.member != 0);
            }
            _ => panic!("Model did not return a constant"),
        }
    }

Do you have an example that fails that I could look at?

OK, to be honesty, I found it maybe a different reason.

I tried to symbol execute the ir function zexecute of rv32d.ir/rv64d.ir. I want to get the solved ISA state required by the execution path in the end of every execution path.

But I just run the symbolic engine using start_single and solve the symbolic value at the 'Collector' function. So it result in the problem.

For this, in second path,mstatus will be assigned and overwrite the symbolic value. So I meant to get the value zcur_privilege =Privilege::zMachine(EnumMember.member:3),but actually I get the zUser(member:0).

I just want to get the registers before execution which the path executed need. How can I achive that?

here is some registers printed and the events.

  zmepc = <arbitrary: BitVec(32)>
  zmvendorid = 0x0
  zelp = 0x0
  zsenvcfg = {bits: #x00000000} | Struct({Name("zbits"): Bits(B129 { tag: false, bits: 0, len: 32 })})
  zmhartid = 0x0
  znextPC = <arbitrary: BitVec(32)>
  zmconfigptr = 0x0
  zmstatus = {bits: #x0000000000001880} | Struct({Name("zbits"): Bits(B129 { tag: false, bits: 6272, len: 64 })})
  zmimpid = 0x0
  zmarchid = 0x0
  zcur_privilege = Privilege::zUser(EnumMember.member:0) | Enum(EnumMember { enum_id: EnumId { id: Name("zPrivilege") }, member: 0 })
  zhtif_tohost_base = None<b>(()) | Ctor(Name("zNonezIbzK"), Unit)
  zpc_reset_address = 0x0
  zmseccfg = {bits: #x0000000000000000} | Struct({Name("zbits"): Bits(B129 { tag: false, bits: 0, len: 64 })})
  zmisa = {bits: #x40000000} | Struct({Name("zbits"): Bits(B129 { tag: false, bits: 1073741824, len: 32 })})
  zmenvcfg = {bits: #x0000000000000000} | Struct({Name("zbits"): Bits(B129 { tag: false, bits: 0, len: 64 })})
  zhart_state = HART_ACTIVE(()) | Ctor(Name("zHART_ACTIVE"), Unit)
  z__monomorphizze_writes = false
  zPC = <arbitrary: BitVec(32)>

 [event] Function { name: Name("zexecute"), call: false }
 [event] Function { name: Name("zset_next_pc"), call: false }
 [event] Function { name: Name("zredirect_callback"), call: false }
 [event] Function { name: Name("zredirect_callback"), call: true }
 [event] WriteReg(Name("znextPC"), [], Symbolic(Sym { id: 126 }))
 [event] Branch { address: Symbolic(Sym { id: 126 }) }
 [event] Function { name: Name("zset_next_pc"), call: true }
 [event] Function { name: Name("zexception_handler"), call: false }
 [event] Function { name: Name("zprepare_xret_target"), call: false }
 [event] Function { name: Name("zget_xepc"), call: false }
 [event] Function { name: Name("zalign_pc"), call: false }
 [event] Smt(DefineConst(Sym { id: 126 }, Bvor(Bvand(Var(Sym { id: 125 }), Bvnot(Bits64(B64 { len: 32, bits: 3 }))), ZeroExtend(30, Bits64(B64 { len: 2, bits: 0 })))), DefAttrs { attrs: 0 }, SourceLoc { file: -1, line1: 0, char1: 0, line2: 0, char2: 0 })
 [event] Function { name: Name("zzzeros"), call: false }
 [event] Function { name: Name("zzzeros"), call: true }
 [event] Function { name: Name("zcurrentlyEnabled"), call: false }
 [event] Function { name: Name("znot"), call: false }
 [event] Function { name: Name("znot"), call: true }
 [event] Function { name: Name("zhartSupports"), call: false }
 [event] Function { name: Name("zhartSupports"), call: false }
 [event] Function { name: Name("zhartSupports"), call: true }
 [event] Function { name: Name("zhartSupports"), call: false }
 [event] Function { name: Name("zhartSupports"), call: true }
 [event] Function { name: Name("zhartSupports"), call: false }
 [event] Function { name: Name("zhartSupports"), call: true }
 [event] Function { name: Name("zhartSupports"), call: true }
 [event] Function { name: Name("zcurrentlyEnabled"), call: false }
 [event] Function { name: Name("z_get_Misa_C"), call: false }
 [event] Function { name: Name("z_get_Misa_C"), call: true }
 [event] ReadReg(Name("zmisa"), [], Struct({Name("zbits"): Bits(B129 { tag: false, bits: 1073741824, len: 32 })}))
 [event] Function { name: Name("zhartSupports"), call: false }
 [event] Function { name: Name("zhartSupports"), call: false }
 [event] Function { name: Name("zhartSupports"), call: true }
 [event] Function { name: Name("zhartSupports"), call: false }
 [event] Function { name: Name("zhartSupports"), call: true }
 [event] Function { name: Name("zhartSupports"), call: false }
 [event] Function { name: Name("zhartSupports"), call: true }
 [event] Function { name: Name("zhartSupports"), call: true }
 [event] Function { name: Name("zcurrentlyEnabled"), call: true }
 [event] Function { name: Name("zhartSupports"), call: false }
 [event] Function { name: Name("zhartSupports"), call: true }
 [event] Function { name: Name("zcurrentlyEnabled"), call: true }
 [event] Function { name: Name("zalign_pc"), call: true }
 [event] ReadReg(Name("zmepc"), [], Symbolic(Sym { id: 125 }))
 [event] Smt(DeclareConst(Sym { id: 125 }, BitVec(32)), DefAttrs { attrs: 0 }, SourceLoc { file: 40, line1: 43, char1: 25, line2: 43, char2: 39 })
 [event] Function { name: Name("zget_xepc"), call: true }
 [event] Function { name: Name("zprepare_xret_target"), call: true }
 [event] Function { name: Name("zget_config_print_exception"), call: false }
 [event] Function { name: Name("zget_config_print_exception"), call: true }
 [event] Function { name: Name("zlong_csr_write_callback"), call: false }
 [event] Function { name: Name("zcsr_name_write_callback"), call: false }
 [event] Function { name: Name("zcsr_full_write_callback"), call: false }
 [event] Smt(DeclareConst(Sym { id: 124 }, BitVec(32)), DefAttrs { attrs: 0 }, SourceLoc { file: 31, line1: 35, char1: 33, line2: 35, char2: 34 })
 [event] Smt(DeclareConst(Sym { id: 123 }, BitVec(12)), DefAttrs { attrs: 0 }, SourceLoc { file: 31, line1: 35, char1: 33, line2: 35, char2: 34 })
 [event] Function { name: Name("zcsr_full_write_callback"), call: true }
 [event] Function { name: Name("zcsr_name_map_backwards"), call: false }
 [event] Function { name: Name("zcsr_name_map_backwards"), call: true }
 [event] Function { name: Name("zcsr_name_write_callback"), call: true }
 [event] Function { name: Name("zcsr_name_write_callback"), call: false }
 [event] Function { name: Name("zcsr_full_write_callback"), call: false }
 [event] Smt(DeclareConst(Sym { id: 122 }, BitVec(32)), DefAttrs { attrs: 0 }, SourceLoc { file: 31, line1: 35, char1: 33, line2: 35, char2: 34 })
 [event] Smt(DeclareConst(Sym { id: 121 }, BitVec(12)), DefAttrs { attrs: 0 }, SourceLoc { file: 31, line1: 35, char1: 33, line2: 35, char2: 34 })
 [event] Function { name: Name("zcsr_full_write_callback"), call: true }
 [event] Function { name: Name("zcsr_name_map_backwards"), call: false }
 [event] Function { name: Name("zcsr_name_map_backwards"), call: true }
 [event] Function { name: Name("zcsr_name_write_callback"), call: true }
 [event] Function { name: Name("zlong_csr_write_callback"), call: true }
 [event] ReadReg(Name("zmstatus"), [Field(Name("zbits"))], Struct({Name("zbits"): Bits(B129 { tag: false, bits: 6272, len: 64 })}))
 [event] Function { name: Name("zzzicfilp_restore_elp_on_xret"), call: false }
 [event] WriteReg(Name("zelp"), [], Bits(B129 { tag: false, bits: 0, len: 1 }))
 [event] Function { name: Name("zlanding_pad_bits_backwards"), call: false }
 [event] Function { name: Name("zlanding_pad_bits_backwards"), call: true }
 [event] Function { name: Name("zget_xLPE"), call: false }
 [event] Function { name: Name("zbool_bits_backwards"), call: false }
 [event] Function { name: Name("zbool_bits_backwards"), call: true }
 [event] Function { name: Name("z_get_MEnvcfg_LPE"), call: false }
 [event] Function { name: Name("z_get_MEnvcfg_LPE"), call: true }
 [event] ReadReg(Name("zmenvcfg"), [], Struct({Name("zbits"): Bits(B129 { tag: false, bits: 0, len: 64 })}))
 [event] Function { name: Name("zcurrentlyEnabled"), call: false }
 [event] Function { name: Name("z_get_Misa_S"), call: false }
 [event] Function { name: Name("z_get_Misa_S"), call: true }
 [event] ReadReg(Name("zmisa"), [], Struct({Name("zbits"): Bits(B129 { tag: false, bits: 1073741824, len: 32 })}))
 [event] Function { name: Name("zhartSupports"), call: false }
 [event] Function { name: Name("zhartSupports"), call: true }
 [event] Function { name: Name("zcurrentlyEnabled"), call: true }
 [event] Function { name: Name("zget_xLPE"), call: true }
 [event] WriteReg(Name("zmstatus"), [], Struct({Name("zbits"): Bits(B129 { tag: false, bits: 6272, len: 64 })}))
 [event] ReadReg(Name("zmstatus"), [], Struct({Name("zbits"): Bits(B129 { tag: false, bits: 6272, len: 64 })}))
 [event] Function { name: Name("zlanding_pad_bits_backwards"), call: false }
 [event] Function { name: Name("zlanding_pad_bits_backwards"), call: true }
 [event] Smt(DefineEnum(Name("zlanding_pad_expectation"), 2), DefAttrs { attrs: 0 }, SourceLoc { file: -1, line1: 0, char1: 0, line2: 0, char2: 0 })
 [event] ReadReg(Name("zmstatus"), [Field(Name("zbits"))], Struct({Name("zbits"): Bits(B129 { tag: false, bits: 6272, len: 64 })}))
 [event] Function { name: Name("z_get_Mstatus_MPELP"), call: false }
 [event] Function { name: Name("z_get_Mstatus_MPELP"), call: true }
 [event] ReadReg(Name("zmstatus"), [], Struct({Name("zbits"): Bits(B129 { tag: false, bits: 6272, len: 64 })}))
 [event] Function { name: Name("zzzicfilp_restore_elp_on_xret"), call: true }
 [event] ReadReg(Name("zcur_privilege"), [], Enum(EnumMember { enum_id: EnumId { id: Name("zPrivilege") }, member: 0 }))
 [event] Smt(DefineEnum(Name("zxRET_type"), 2), DefAttrs { attrs: 0 }, SourceLoc { file: -1, line1: 0, char1: 0, line2: 0, char2: 0 })
 [event] Function { name: Name("zhartSupports"), call: false }
 [event] Function { name: Name("zhartSupports"), call: true }
 [event] WriteReg(Name("zmstatus"), [], Struct({Name("zbits"): Bits(B129 { tag: false, bits: 6272, len: 64 })}))
 [event] ReadReg(Name("zmstatus"), [], Struct({Name("zbits"): Bits(B129 { tag: false, bits: 6272, len: 64 })}))
 [event] ReadReg(Name("zmstatus"), [Field(Name("zbits"))], Struct({Name("zbits"): Bits(B129 { tag: false, bits: 6272, len: 64 })}))
 [event] Function { name: Name("zneq_anythingzIEPrivilegez5zK"), call: false }
 [event] Function { name: Name("zneq_anythingzIEPrivilegez5zK"), call: true }
 [event] ReadReg(Name("zcur_privilege"), [], Enum(EnumMember { enum_id: EnumId { id: Name("zPrivilege") }, member: 0 }))
 [event] WriteReg(Name("zmstatus"), [], Struct({Name("zbits"): Bits(B129 { tag: false, bits: 6272, len: 64 })}))
 [event] ReadReg(Name("zmstatus"), [], Struct({Name("zbits"): Bits(B129 { tag: false, bits: 128, len: 64 })}))
 [event] Function { name: Name("zprivLevel_to_bits"), call: false }
 [event] Function { name: Name("zprivLevel_bits_backwards"), call: false }
 [event] Function { name: Name("zprivLevel_bits_backwards"), call: true }
 [event] Function { name: Name("zprivLevel_to_bits"), call: true }
 [event] Function { name: Name("zcurrentlyEnabled"), call: false }
 [event] Function { name: Name("z_get_Misa_U"), call: false }
 [event] Function { name: Name("z_get_Misa_U"), call: true }
 [event] ReadReg(Name("zmisa"), [], Struct({Name("zbits"): Bits(B129 { tag: false, bits: 1073741824, len: 32 })}))
 [event] Function { name: Name("zhartSupports"), call: false }
 [event] Function { name: Name("zhartSupports"), call: true }
 [event] Function { name: Name("zcurrentlyEnabled"), call: true }
 [event] Smt(DefineEnum(Name("zextension"), 104), DefAttrs { attrs: 0 }, SourceLoc { file: -1, line1: 0, char1: 0, line2: 0, char2: 0 })
 [event] ReadReg(Name("zmstatus"), [Field(Name("zbits"))], Struct({Name("zbits"): Bits(B129 { tag: false, bits: 128, len: 64 })}))
 [event] WriteReg(Name("zcur_privilege"), [], Enum(EnumMember { enum_id: EnumId { id: Name("zPrivilege") }, member: 0 }))
 [event] Function { name: Name("zprivLevel_bits_forwards"), call: false }
 [event] Function { name: Name("zprivLevel_bits_forwards"), call: true }
 [event] Function { name: Name("z_get_Mstatus_MPP"), call: false }
 [event] Function { name: Name("z_get_Mstatus_MPP"), call: true }
 [event] ReadReg(Name("zmstatus"), [], Struct({Name("zbits"): Bits(B129 { tag: false, bits: 128, len: 64 })}))
 [event] WriteReg(Name("zmstatus"), [], Struct({Name("zbits"): Bits(B129 { tag: false, bits: 128, len: 64 })}))
 [event] ReadReg(Name("zmstatus"), [], Struct({Name("zbits"): Bits(B129 { tag: false, bits: 0, len: 64 })}))
 [event] ReadReg(Name("zmstatus"), [Field(Name("zbits"))], Struct({Name("zbits"): Bits(B129 { tag: false, bits: 0, len: 64 })}))
 [event] WriteReg(Name("zmstatus"), [], Struct({Name("zbits"): Bits(B129 { tag: false, bits: 0, len: 64 })}))
 [event] ReadReg(Name("zmstatus"), [], Struct({Name("zbits"): Bits(B129 { tag: false, bits: 0, len: 64 })}))
 [event] Function { name: Name("z_get_Mstatus_MPIE"), call: false }
 [event] Function { name: Name("z_get_Mstatus_MPIE"), call: true }
 [event] ReadReg(Name("zmstatus"), [], Struct({Name("zbits"): Bits(B129 { tag: false, bits: 0, len: 64 })}))
 [event] ReadReg(Name("zmstatus"), [Field(Name("zbits"))], Struct({Name("zbits"): Bits(B129 { tag: false, bits: 0, len: 64 })}))
 [event] ReadReg(Name("zcur_privilege"), [], Symbolic(Sym { id: 6 }))
 [event] Function { name: Name("zexception_handler"), call: true }
 [event] ReadReg(Name("zPC"), [], Symbolic(Sym { id: 9 }))
 [event] Smt(DeclareConst(Sym { id: 9 }, BitVec(32)), DefAttrs { attrs: 0 }, SourceLoc { file: 68, line1: 567, char1: 16, line2: 567, char2: 64 })
 [event] ReadReg(Name("zcur_privilege"), [], Symbolic(Sym { id: 6 }))
 [event] Function { name: Name("znot"), call: false }
 [event] Function { name: Name("znot"), call: true }
 [event] Function { name: Name("zext_check_xret_priv"), call: false }
 [event] Function { name: Name("zext_check_xret_priv"), call: true }
 [event] Smt(Assert(Not(Var(Sym { id: 8 }))), DefAttrs { attrs: 0 }, SourceLoc { file: -1, line1: 0, char1: 0, line2: 0, char2: 0 })
 [event] Fork(0, (not (= k!5 k!6)) = false, expr=(not (= k!5 k!6)), branch=1)
 [event] Function { name: Name("zneq_anythingzIEPrivilegez5zK"), call: false }
 [event] Smt(DefineConst(Sym { id: 8 }, Not(Var(Sym { id: 7 }))), DefAttrs { attrs: 0 }, SourceLoc { file: 3, line1: 61, char1: 30, line2: 61, char2: 57 })
 [event] Smt(DefineConst(Sym { id: 7 }, Eq(Enum(EnumMember { enum_id: EnumId { id: Name("zPrivilege") }, member: 4 }), Var(Sym { id: 6 }))), DefAttrs { attrs: 0 }, SourceLoc { file: 3, line1: 61, char1: 39, line2: 61, char2: 56 })
 [event] Function { name: Name("zneq_anythingzIEPrivilegez5zK"), call: true }
 [event] ReadReg(Name("zcur_privilege"), [], Symbolic(Sym { id: 6 }))
 [event] Smt(DeclareConst(Sym { id: 6 }, Enum(EnumId { id: Name("zPrivilege") })), DefAttrs { attrs: 0 }, SourceLoc { file: 68, line1: 562, char1: 7, line2: 562, char2: 31 })
 [event] Smt(DefineEnum(Name("zPrivilege"), 5), DefAttrs { attrs: 0 }, SourceLoc { file: -1, line1: 0, char1: 0, line2: 0, char2: 0 })

[bacam]

If I'm reading the trace correctly (it appears to be backwards), then mstatus[MPP] is zero at the assignment of cur_privilege, which corresponds to User. So you do seem to be getting the correct value.

[msuadOf]

If I'm reading the trace correctly (it appears to be backwards), then mstatus[MPP] is zero at the assignment of cur_privilege, which corresponds to User. So you do seem to be getting the correct value.如果我正确解读了跟踪信息（看起来顺序反了），那么在 cur_privilege 赋值时， mstatus[MPP] 的值为零，这对应于 User 。所以你似乎确实得到了正确的值。

I forget to describe something. I construct a partial symbolic argument of the Ctor function like the way below. And the log above is the output of MRET.

    let ctor_name = shared_state.symtab.lookup(instruction_name);

    let instruction_union = shared_state.type_info.unions.get(&shared_state.symtab.lookup("zinstruction"));

    let Some(union_members) = instruction_union else {
        panic!("run_symbolic_execute: error 'zinstruction'");
    };

    let Some((_, ctor_ty)) = union_members.iter().find(|(n, _ty)| *n == ctor_name) else {
        return None;
    };

    let mut cfg = Config::new();
    cfg.set_param_value("model", "true");
    let ctx = Context::new(cfg);
    let mut solver = Solver::new(&ctx);

    let fun_args = vec![Val::<B>::Ctor(
        ctor_name,
        Box::new(symbolic(ctor_ty, shared_state, &mut solver, SourceLoc::unknown()).unwrap()),
    )];

But I want to get the value Machine because it is the condition that the 'else' branch('else branch' is sail file's shown below)should satisfy. It means if the register cur_privilege is Machine before actual concrete excution, it will go into the else branch and return RETIRE_SUCCESS.

For event, the WriteReg of cur_privilege after the Fork override the symbolic value(the value I want to get) and should be removed.

[msuadOf]

My idea to solve this problem is to get the expression of Fork and replace intermediate variables by some WriteReg and ReadReg event. Another idea is to get the value of what the Sym_id maps to.

Am I thinking correctly? Is my idea convenient to implement? I don't know is there some code I can use or some tips to help me solve that.

[bacam]

The approach I used in isla-testgen was to remember the initial value for registers (which in this case would be Symbolic(Sym { id: 6 })) and use the model to fill in the symbolic values. Alternatively, you could find the initial value by looking for the first ReadReg of the register in the trace.

[msuadOf]

The approach I used in isla-testgen was to remember the initial value for registers (which in this case would be Symbolic(Sym { id: 6 })) and use the model to fill in the symbolic values. Alternatively, you could find the initial value by looking for the first ReadReg of the register in the trace.我在 isla-testgen 中使用的方法是记住寄存器的初始值（在本例中为 Symbolic(Sym { id: 6 }) ），并使用模型来填充符号值。或者，您也可以通过在跟踪中查找寄存器的第一个 ReadReg 调用来找到初始值。

Can you give me the code location? I can find them more easily. Thank you for your help!

[bacam]

The code that obtains the initial register values is https://github.com/rems-project/isla-testgen/blob/master/src/extract_state.rs#L389, and uses a map built during setup, https://github.com/rems-project/isla-testgen/blob/master/src/execution.rs#L538.

[msuadOf]

Ok, I have read the code and I have another question. When symbolic execution needs to access registers like 'x1' and 'x2' in riscv, it creates a Fork for each register because of IR, but this is clearly problematic. These general-purpose registers are interchangeable, and we don't actually care about which specific one is used. I want to know how to handle this part.