Generate "symbolic" footprints with Isla?

[zsisco]

Hi, I'm really interested in the work you all have done with Isla. I was wondering if it's possible to generate "symbolic" instruction footprints with Isla?

That is, given some instruction like add x, y, z, where x, y, and z are arbitrary registers, it might generate a footprint such as the following based on the definition in the Sail code:

(declare-const v0 (_ BitVec 64))
(read-reg |y| nil v0)
(declare-const v1 (_ BitVec 64))
(read-reg |z| nil v1)
(define-const v2 (bvadd v0 v1))
(write-reg |x| nil v2))

I can't quite grok the code in footprint.rs to gather what I would need to do to add such a feature, but if you have any idea if doing such a thing is possible in Isla and where to look, I'd appreciate it! Thanks!

[bacam]

We're interested in this ourselves to reuse traces more during verification work. There is already support for working with a partially symbolic instruction and it works reasonably well for symbolic immediate operands. For example, on AArch64 --partial -i '1 0 0 100010 0 imm:12 00000 00000' adds the symbolic value imm to x0. It still needs a little code to link the name to the SMT variable that appears in the trace.

For registers our current models case split on the register used, causing some path explosion. I have experimented a little with allowing accesses to the register file to be indexed by a symbolic value with reasonable results except that it generates some complex SMT output in the trace to allow for aliasing. For example, if you read two registers x and y the solver needs to know that if x = y then you get the same value. I haven't yet updated and committed this patch, but I could do it fairly quickly if you're interested.

[zsisco]

Thanks for the response! Yes, I would be interested in that.

I didn't know about the --partial option; thanks for bringing that to my attention.

[uv-xiao]

Hi @bacam,

Could you provide some details or examples about how isla-footprint supports symbolic traces currently? I'm also interested in this feature. Thanks a lot!

[uv-xiao]

I tried target/release/isla-footprint -A snapshots/riscv64. ir -C configs/riscv64.toml --partial -i '000000000000 r0:5 000 00000 0010011' -s for instruction addi x0, r0, 0 where r0 is symbolic, and the isla-footprint produces replications of the following trace:

(trace
  (declare-const v0 (_ BitVec 5)) ; 0:0 - 0:0
  (assume-reg |misa| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |mstatus| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |mcountinhibit| nil (_ struct (|bits| #x00000000)))
  (assume-reg |satp| nil #x0000000000000000)
  (define-enum |Privilege| 3 (|User| |Supervisor| |Machine|)) ; 0:0 - 0:0
  (define-enum |Architecture| 3 (|RV32| |RV64| |RV128|)) ; 0:0 - 0:0
  (define-enum |PmpAddrMatchType| 4 (|OFF| |TOR| |NA4| |NAPOT|)) ; 0:0 - 0:0
  (cycle)
  (declare-const v74 (_ BitVec 64)) ; model/main.sail 107:15 - 107:21
  (read-reg |PC| nil v74)
  (define-const v75 (bvadd v74 #x0000000000000004)) ; 0:0 - 0:0
  (write-reg |nextPC| nil v75)
  (define-enum |iop| 6 (|RISCV_ADDI| |RISCV_SLTI| |RISCV_SLTIU| |RISCV_XORI| |RISCV_ORI| |RISCV_ANDI|)) ; 0:0 - 0:0
  (define-const v84 ((_ extract 63 0) ((_ zero_extend 123) v0))) ; model/riscv_regs.sail 209:46 - 209:57
  (define-const v87 (not (= ((_ sign_extend 64) v84) #x00000000000000000000000000000000))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 0 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v87) ; 0:0 - 0:0
  (define-const v90 (not (= ((_ sign_extend 64) v84) #x00000000000000000000000000000001))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 1 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v90) ; 0:0 - 0:0
  (define-const v93 (not (= ((_ sign_extend 64) v84) #x00000000000000000000000000000002))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 2 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v93) ; 0:0 - 0:0
  (define-const v96 (not (= ((_ sign_extend 64) v84) #x00000000000000000000000000000003))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 3 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v96) ; 0:0 - 0:0
  (define-const v99 (not (= ((_ sign_extend 64) v84) #x00000000000000000000000000000004))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 4 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v99) ; 0:0 - 0:0
  (define-const v102 (not (= ((_ sign_extend 64) v84) #x00000000000000000000000000000005))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 5 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v102) ; 0:0 - 0:0
  (define-const v105 (not (= ((_ sign_extend 64) v84) #x00000000000000000000000000000006))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 6 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v105) ; 0:0 - 0:0
  (define-const v108 (not (= ((_ sign_extend 64) v84) #x00000000000000000000000000000007))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 7 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v108) ; 0:0 - 0:0
  (define-const v111 (not (= ((_ sign_extend 64) v84) #x00000000000000000000000000000008))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 8 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v111) ; 0:0 - 0:0
  (define-const v114 (not (= ((_ sign_extend 64) v84) #x00000000000000000000000000000009))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 9 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v114) ; 0:0 - 0:0
  (define-const v117 (not (= ((_ sign_extend 64) v84) #x0000000000000000000000000000000a))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 10 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v117) ; 0:0 - 0:0
  (define-const v120 (not (= ((_ sign_extend 64) v84) #x0000000000000000000000000000000b))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 11 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v120) ; 0:0 - 0:0
  (define-const v123 (not (= ((_ sign_extend 64) v84) #x0000000000000000000000000000000c))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 12 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v123) ; 0:0 - 0:0
  (define-const v126 (not (= ((_ sign_extend 64) v84) #x0000000000000000000000000000000d))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 13 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v126) ; 0:0 - 0:0
  (define-const v129 (not (= ((_ sign_extend 64) v84) #x0000000000000000000000000000000e))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 14 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v129) ; 0:0 - 0:0
  (define-const v132 (not (= ((_ sign_extend 64) v84) #x0000000000000000000000000000000f))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 15 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v132) ; 0:0 - 0:0
  (define-const v135 (not (= ((_ sign_extend 64) v84) #x00000000000000000000000000000010))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 16 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v135) ; 0:0 - 0:0
  (define-const v138 (not (= ((_ sign_extend 64) v84) #x00000000000000000000000000000011))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 17 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v138) ; 0:0 - 0:0
  (define-const v141 (not (= ((_ sign_extend 64) v84) #x00000000000000000000000000000012))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 18 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v141) ; 0:0 - 0:0
  (define-const v144 (not (= ((_ sign_extend 64) v84) #x00000000000000000000000000000013))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 19 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v144) ; 0:0 - 0:0
  (define-const v147 (not (= ((_ sign_extend 64) v84) #x00000000000000000000000000000014))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 20 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v147) ; 0:0 - 0:0
  (define-const v150 (not (= ((_ sign_extend 64) v84) #x00000000000000000000000000000015))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 21 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v150) ; 0:0 - 0:0
  (define-const v153 (not (= ((_ sign_extend 64) v84) #x00000000000000000000000000000016))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 22 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v153) ; 0:0 - 0:0
  (define-const v156 (not (= ((_ sign_extend 64) v84) #x00000000000000000000000000000017))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 23 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v156) ; 0:0 - 0:0
  (define-const v159 (not (= ((_ sign_extend 64) v84) #x00000000000000000000000000000018))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 24 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v159) ; 0:0 - 0:0
  (define-const v162 (not (= ((_ sign_extend 64) v84) #x00000000000000000000000000000019))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 25 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v162) ; 0:0 - 0:0
  (define-const v165 (not (= ((_ sign_extend 64) v84) #x0000000000000000000000000000001a))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 26 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v165) ; 0:0 - 0:0
  (define-const v168 (not (= ((_ sign_extend 64) v84) #x0000000000000000000000000000001b))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 27 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v168) ; 0:0 - 0:0
  (define-const v171 (not (= ((_ sign_extend 64) v84) #x0000000000000000000000000000001c))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 28 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v171) ; 0:0 - 0:0
  (define-const v174 (not (= ((_ sign_extend 64) v84) #x0000000000000000000000000000001d))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 29 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v174) ; 0:0 - 0:0
  (define-const v177 (not (= ((_ sign_extend 64) v84) #x0000000000000000000000000000001e))) ; model/riscv_regs.sail 114:4 - 148:5
  (branch 30 "model/riscv_regs.sail 114:4 - 148:5")
  (assert v177) ; 0:0 - 0:0
  (assert (not (not (= ((_ sign_extend 64) v84) #x0000000000000000000000000000001f)))) ; 0:0 - 0:0
  (declare-const v181 (_ BitVec 64)) ; model/riscv_regs.sail 146:12 - 146:15
  (read-reg |x31| nil v181)
  (define-enum |Retired| 2 (|RETIRE_SUCCESS| |RETIRE_FAIL|)) ; 0:0 - 0:0
  (read-reg |nextPC| nil v75)
  (write-reg |PC| nil v75))

The trace seems to try every possible value of r0 through define-const; branch; asserts rather than leaving it symbolic as I expected. Is there any method to keep the register index symbolic in the produced trace?

Thanks again!

[Alasdair]

Getting the symbolic registers working might require a bit of tweaking to the specs. I think the way the RISC-V model is written might be forcing the case-splitting on the register numbers.

This is a fairly straightforward change though, so I'll look at it when I am back later this week.

[Alasdair]

One thing you could try is --abstract rX and --abstract wX, which would include events for calling the reading and writing functions for the GPRs in the trace, rather than the concrete read-reg events.

[uv-xiao]

Hi @Alasdair ,

One thing you could try is --abstract rX and --abstract wX, which would include events for calling the reading and writing functions for the GPRs in the trace, rather than the concrete read-reg events.

I tried with target/release/isla-footprint -A snapshots/riscv64.ir -C configs/riscv64.toml --partial -i '000000000000 r0:5 000 00000 0010011' -s --abstract rX --abstract wX, which produced:

(trace
  (declare-const v0 (_ BitVec 5)) ; 0:0 - 0:0
  (assume-reg |misa| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |mstatus| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |mcountinhibit| nil (_ struct (|bits| #x00000000)))
  (assume-reg |satp| nil #x0000000000000000)
  (define-enum |Privilege| 3 (|User| |Supervisor| |Machine|)) ; 0:0 - 0:0
  (define-enum |Architecture| 3 (|RV32| |RV64| |RV128|)) ; 0:0 - 0:0
  (define-enum |PmpAddrMatchType| 4 (|OFF| |TOR| |NA4| |NAPOT|)) ; 0:0 - 0:0
  (cycle)
  (declare-const v74 (_ BitVec 64)) ; model/main.sail 107:15 - 107:21
  (read-reg |PC| nil v74)
  (define-const v75 (bvadd v74 #x0000000000000004)) ; 0:0 - 0:0
  (write-reg |nextPC| nil v75)
  (define-enum |iop| 6 (|RISCV_ADDI| |RISCV_SLTI| |RISCV_SLTIU| |RISCV_XORI| |RISCV_ORI| |RISCV_ANDI|)) ; 0:0 - 0:0
  (define-const v84 ((_ extract 63 0) ((_ zero_extend 123) v0))) ; model/riscv_regs.sail 209:46 - 209:57
  (declare-const v85 (_ BitVec 64)) ; model/riscv_regs.sail 209:43 - 209:58
  (abstract-call |rX| v85 v84)
  (define-const v86 (bvadd v85 #x0000000000000000)) ; model/riscv_insts_base.sail 238:19 - 238:35
  (abstract-call |wX| (_ unit) (_ bv0 64) v86)
  (define-enum |Retired| 2 (|RETIRE_SUCCESS| |RETIRE_FAIL|)) ; 0:0 - 0:0
  (read-reg |nextPC| nil v75)
  (write-reg |PC| nil v75))

which looks much more friendly, and I guess the declared_const v85 stands for the symbolic r0. Is that possible to generate such mapping relations for symbolic variables?

Getting the symbolic registers working might require a bit of tweaking to the specs. I think the way the RISC-V model is written might be forcing the case-splitting on the register numbers.

This is a fairly straightforward change though, so I'll look at it when I am back later this week.

Thanks for your attention! BTW, are there any open tutorials or documents that help to use the isla-lib? The Rust API documentation is available, but some simple examples might be very helpful for understanding. I found it hard to modify the src/footprint.rs by myself.