Skip to content

Instantly share code, notes, and snippets.

@mmcloughlin

mmcloughlin/trace0000.out Secret

Last active January 8, 2024 21:59
Show Gist options
  • Save mmcloughlin/943d338e0126cdbb62f3d205f2b1c289 to your computer and use it in GitHub Desktop.
Save mmcloughlin/943d338e0126cdbb62f3d205f2b1c289 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
trace0000.out
(trace
(declare-const v0 (_ BitVec 64)) ; register_accessors.sail 28:25 - 28:34
(declare-const v1 (_ BitVec 64)) ; register_accessors.sail 28:25 - 28:34
(declare-const v2 (_ BitVec 64)) ; register_accessors.sail 28:25 - 28:34
(declare-const v3 (_ BitVec 64)) ; register_accessors.sail 28:25 - 28:34
(declare-const v4 (_ BitVec 64)) ; register_accessors.sail 28:25 - 28:34
(declare-const v5 (_ BitVec 64)) ; register_accessors.sail 28:25 - 28:34
(declare-const v6 (_ BitVec 64)) ; register_accessors.sail 28:25 - 28:34
(read-reg |msrs| nil (_ vec v0 v1 v2 v3 v4 v5 v6))
(define-const v9 (bvor (bvand v0 #xfffffffffffff000) ((_ zero_extend 52) (bvor (bvand ((_ extract 11 0) v0) #xbff) #x400)))) ; 0:0 - 0:0
(write-reg |msrs| nil (_ vec v9 v1 v2 v3 v4 v5 v6))
(declare-const v10 (_ BitVec 16)) ; main.sail 12:66 - 12:85
(declare-const v11 (_ BitVec 16)) ; main.sail 12:66 - 12:85
(declare-const v12 (_ BitVec 16)) ; main.sail 12:66 - 12:85
(declare-const v13 (_ BitVec 16)) ; main.sail 12:66 - 12:85
(declare-const v14 (_ BitVec 16)) ; main.sail 12:66 - 12:85
(declare-const v15 (_ BitVec 16)) ; main.sail 12:66 - 12:85
(read-reg |seg_hidden_attrs| nil (_ vec v10 v11 v12 v13 v14 v15))
(define-const v16 (bvor (bvand v11 #xfdff) #x0200)) ; 0:0 - 0:0
(write-reg |seg_hidden_attrs| nil (_ vec v10 v16 v12 v13 v14 v15))
(declare-const v24 (_ BitVec 64)) ; 0:0 - 0:0
(declare-const v33 (_ BitVec 64)) ; 0:0 - 0:0
(declare-const v34 (_ BitVec 64)) ; 0:0 - 0:0
(declare-const v35 (Array (_ BitVec 64) (_ BitVec 8))) ; 0:0 - 0:0
(assert (= v34 #x0000000000401000)) ; 0:0 - 0:0
(declare-const v36 (_ BitVec 24)) ; 0:0 - 0:0
(assert (and (and (bvule #x0000000000401000 v34) (bvult (bvadd ((_ zero_extend 65) v34) ((_ zero_extend 65) #x0000000000000003)) ((_ zero_extend 65) #x0000000000411000))) (= v36 (concat (select v35 (bvadd v34 #x0000000000000002)) (concat (select v35 (bvadd v34 #x0000000000000001)) (select v35 v34)))))) ; 0:0 - 0:0
(read-mem v36 (_ unit) v34 3)
(declare-const v37 (_ BitVec 24)) ; 0:0 - 0:0
(assert (= v37 #xea014c)) ; 0:0 - 0:0
(assert (= v37 v36)) ; 0:0 - 0:0
(read-reg |ms_reg| nil false)
(read-reg |fault_reg| nil false)
(read-reg |msrs| nil (_ vec v9 v1 v2 v3 v4 v5 v6))
(read-reg |seg_hidden_attrs| nil (_ vec v10 v16 v12 v13 v14 v15))
(assert (= ((_ extract 10 10) ((_ extract 11 0) v9)) #b1)) ; 0:0 - 0:0
(assert (= ((_ extract 9 9) v16) #b1)) ; 0:0 - 0:0
(define-enum |proc_mode| 5 (|Mode_64bit| |Mode_Compatibility| |Mode_Protected| |Mode_Real| |Mode_SMM|)) ; 0:0 - 0:0
(read-reg |rip| nil v34)
(define-const v49 ((_ extract 47 0) v34)) ; 0:0 - 0:0
(define-const v50 ((_ sign_extend 16) v49)) ; step.sail 92:94 - 92:125
(define-const v53 ((_ sign_extend 64) ((_ extract 63 0) ((_ sign_extend 64) v50)))) ; ./segmentation.sail 262:20 - 262:57
(assert (not (not (ite (not (bvsle #xffffffffffffffffffff800000000000 v53)) false (bvslt v53 #x00000000000000000000800000000000))))) ; 0:0 - 0:0
(define-const v59 ((_ sign_extend 64) v50)) ; prelude.sail 682:36 - 682:48
(assert (not (not (ite (not (bvsle #xffffffffffffffffffff800000000000 v59)) false (bvslt v59 #x00000000000000000000800000000000))))) ; 0:0 - 0:0
(read-reg |app_view| nil true)
(define-const v68 ((_ zero_extend 12) ((_ sign_extend 4) (bvadd ((_ extract 47 0) v50) #x000000000000)))) ; /home/mbmcloug/.opam/4.10.0/share/sail/lib/vector.sail 141:76 - 141:100
(define-enum |read_kind| 13 (|Read_plain| |Read_reserve| |Read_acquire| |Read_exclusive| |Read_exclusive_acquire| |Read_stream| |Read_ifetch| |Read_RISCV_acquire| |Read_RISCV_strong_acquire| |Read_RISCV_reserved| |Read_RISCV_reserved_acquire| |Read_RISCV_reserved_strong_acquire| |Read_X86_locked|)) ; 0:0 - 0:0
(declare-const v83 (_ BitVec 8)) ; 0:0 - 0:0
(assert (and (and (bvule #x0000000000401000 v68) (bvult (bvadd ((_ zero_extend 65) v68) ((_ zero_extend 65) #x0000000000000001)) ((_ zero_extend 65) #x0000000000411000))) (= v83 (select v35 v68)))) ; 0:0 - 0:0
(read-mem v83 |Read_plain| v68 1)
(define-const v85 (bvor #x00 v83)) ; 0:0 - 0:0
(define-const v89 ((_ sign_extend 64) ((_ extract 63 0) ((_ zero_extend 120) v85)))) ; ././././prefix_modrm_sib_decoding.sail 8:4 - 8:838
(assert (not (not (= ((_ sign_extend 64) (ite (= v89 #x00000000000000000000000000000000) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000001) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000002) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000003) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000004) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000005) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000006) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000007) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000008) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000009) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000000a) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000000b) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000000c) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000000d) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000000e) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000000f) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000010) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000011) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000012) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000013) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000014) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000015) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000016) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000017) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000018) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000019) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000001a) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000001b) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000001c) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000001d) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000001e) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000001f) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000020) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000021) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000022) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000023) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000024) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000025) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000026) #x0000000000000002 (ite (= v89 #x00000000000000000000000000000027) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000028) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000029) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000002a) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000002b) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000002c) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000002d) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000002e) #x0000000000000002 (ite (= v89 #x0000000000000000000000000000002f) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000030) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000031) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000032) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000033) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000034) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000035) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000036) #x0000000000000002 (ite (= v89 #x00000000000000000000000000000037) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000038) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000039) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000003a) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000003b) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000003c) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000003d) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000003e) #x0000000000000002 (ite (= v89 #x0000000000000000000000000000003f) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000040) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000041) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000042) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000043) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000044) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000045) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000046) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000047) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000048) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000049) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000004a) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000004b) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000004c) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000004d) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000004e) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000004f) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000050) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000051) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000052) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000053) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000054) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000055) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000056) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000057) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000058) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000059) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000005a) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000005b) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000005c) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000005d) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000005e) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000005f) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000060) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000061) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000062) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000063) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000064) #x0000000000000002 (ite (= v89 #x00000000000000000000000000000065) #x0000000000000002 (ite (= v89 #x00000000000000000000000000000066) #x0000000000000003 (ite (= v89 #x00000000000000000000000000000067) #x0000000000000004 (ite (= v89 #x00000000000000000000000000000068) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000069) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000006a) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000006b) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000006c) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000006d) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000006e) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000006f) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000070) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000071) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000072) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000073) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000074) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000075) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000076) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000077) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000078) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000079) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000007a) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000007b) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000007c) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000007d) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000007e) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000007f) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000080) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000081) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000082) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000083) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000084) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000085) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000086) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000087) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000088) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000089) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000008a) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000008b) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000008c) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000008d) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000008e) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000008f) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000090) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000091) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000092) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000093) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000094) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000095) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000096) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000097) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000098) #x0000000000000000 (ite (= v89 #x00000000000000000000000000000099) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000009a) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000009b) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000009c) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000009d) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000009e) #x0000000000000000 (ite (= v89 #x0000000000000000000000000000009f) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000a0) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000a1) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000a2) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000a3) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000a4) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000a5) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000a6) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000a7) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000a8) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000a9) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000aa) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000ab) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000ac) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000ad) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000ae) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000af) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000b0) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000b1) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000b2) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000b3) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000b4) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000b5) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000b6) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000b7) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000b8) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000b9) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000ba) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000bb) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000bc) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000bd) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000be) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000bf) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000c0) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000c1) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000c2) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000c3) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000c4) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000c5) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000c6) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000c7) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000c8) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000c9) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000ca) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000cb) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000cc) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000cd) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000ce) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000cf) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000d0) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000d1) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000d2) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000d3) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000d4) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000d5) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000d6) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000d7) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000d8) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000d9) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000da) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000db) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000dc) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000dd) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000de) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000df) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000e0) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000e1) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000e2) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000e3) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000e4) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000e5) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000e6) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000e7) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000e8) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000e9) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000ea) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000eb) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000ec) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000ed) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000ee) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000ef) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000f0) #x0000000000000001 (ite (= v89 #x000000000000000000000000000000f1) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000f2) #x0000000000000001 (ite (= v89 #x000000000000000000000000000000f3) #x0000000000000001 (ite (= v89 #x000000000000000000000000000000f4) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000f5) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000f6) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000f7) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000f8) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000f9) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000fa) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000fb) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000fc) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000fd) #x0000000000000000 (ite (= v89 #x000000000000000000000000000000fe) #x0000000000000000 #x0000000000000000)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) #x00000000000000000000000000000000)))) ; 0:0 - 0:0
(assert (= ((_ extract 3 0) (bvashr ((_ sign_extend 64) ((_ extract 63 0) ((_ zero_extend 120) v85))) #x00000000000000000000000000000004)) #x4)) ; 0:0 - 0:0
(define-const v106 ((_ extract 48 0) ((_ sign_extend 64) (bvadd ((_ extract 63 0) ((_ sign_extend 64) ((_ extract 63 0) ((_ sign_extend 80) v49)))) #x0000000000000001)))) ; 0:0 - 0:0
(define-const v109 ((_ sign_extend 64) ((_ extract 63 0) ((_ sign_extend 79) v106)))) ; ././././decoding_and_spec_utils.sail 80:11 - 80:55
(assert (ite (not (bvsle #xffffffffffffffffffff800000000000 v109)) false (bvslt v109 #x00000000000000000000800000000000))) ; 0:0 - 0:0
(define-const v115 ((_ sign_extend 16) ((_ extract 47 0) v106))) ; step.sail 92:94 - 92:125
(define-const v118 ((_ sign_extend 64) ((_ extract 63 0) ((_ sign_extend 64) v115)))) ; ./segmentation.sail 262:20 - 262:57
(assert (not (not (ite (not (bvsle #xffffffffffffffffffff800000000000 v118)) false (bvslt v118 #x00000000000000000000800000000000))))) ; 0:0 - 0:0
(define-const v124 ((_ sign_extend 64) v115)) ; prelude.sail 682:36 - 682:48
(assert (not (not (ite (not (bvsle #xffffffffffffffffffff800000000000 v124)) false (bvslt v124 #x00000000000000000000800000000000))))) ; 0:0 - 0:0
(define-const v133 ((_ zero_extend 12) ((_ sign_extend 4) (bvadd ((_ extract 47 0) v115) #x000000000000)))) ; /home/mbmcloug/.opam/4.10.0/share/sail/lib/vector.sail 141:76 - 141:100
(declare-const v134 (_ BitVec 8)) ; 0:0 - 0:0
(assert (and (and (bvule #x0000000000401000 v133) (bvult (bvadd ((_ zero_extend 65) v133) ((_ zero_extend 65) #x0000000000000001)) ((_ zero_extend 65) #x0000000000411000))) (= v134 (select v35 v133)))) ; 0:0 - 0:0
(read-mem v134 |Read_plain| v133 1)
(define-const v136 (bvor #x00 v134)) ; 0:0 - 0:0
(define-const v140 ((_ sign_extend 64) ((_ extract 63 0) ((_ zero_extend 120) v136)))) ; ././././prefix_modrm_sib_decoding.sail 8:4 - 8:838
(assert (not (not (= ((_ sign_extend 64) (ite (= v140 #x00000000000000000000000000000000) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000001) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000002) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000003) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000004) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000005) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000006) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000007) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000008) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000009) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000000a) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000000b) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000000c) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000000d) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000000e) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000000f) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000010) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000011) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000012) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000013) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000014) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000015) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000016) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000017) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000018) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000019) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000001a) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000001b) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000001c) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000001d) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000001e) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000001f) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000020) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000021) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000022) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000023) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000024) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000025) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000026) #x0000000000000002 (ite (= v140 #x00000000000000000000000000000027) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000028) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000029) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000002a) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000002b) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000002c) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000002d) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000002e) #x0000000000000002 (ite (= v140 #x0000000000000000000000000000002f) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000030) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000031) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000032) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000033) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000034) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000035) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000036) #x0000000000000002 (ite (= v140 #x00000000000000000000000000000037) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000038) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000039) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000003a) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000003b) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000003c) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000003d) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000003e) #x0000000000000002 (ite (= v140 #x0000000000000000000000000000003f) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000040) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000041) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000042) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000043) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000044) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000045) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000046) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000047) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000048) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000049) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000004a) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000004b) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000004c) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000004d) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000004e) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000004f) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000050) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000051) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000052) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000053) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000054) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000055) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000056) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000057) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000058) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000059) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000005a) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000005b) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000005c) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000005d) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000005e) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000005f) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000060) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000061) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000062) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000063) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000064) #x0000000000000002 (ite (= v140 #x00000000000000000000000000000065) #x0000000000000002 (ite (= v140 #x00000000000000000000000000000066) #x0000000000000003 (ite (= v140 #x00000000000000000000000000000067) #x0000000000000004 (ite (= v140 #x00000000000000000000000000000068) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000069) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000006a) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000006b) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000006c) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000006d) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000006e) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000006f) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000070) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000071) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000072) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000073) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000074) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000075) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000076) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000077) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000078) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000079) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000007a) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000007b) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000007c) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000007d) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000007e) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000007f) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000080) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000081) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000082) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000083) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000084) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000085) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000086) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000087) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000088) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000089) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000008a) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000008b) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000008c) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000008d) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000008e) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000008f) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000090) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000091) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000092) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000093) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000094) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000095) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000096) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000097) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000098) #x0000000000000000 (ite (= v140 #x00000000000000000000000000000099) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000009a) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000009b) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000009c) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000009d) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000009e) #x0000000000000000 (ite (= v140 #x0000000000000000000000000000009f) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000a0) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000a1) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000a2) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000a3) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000a4) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000a5) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000a6) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000a7) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000a8) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000a9) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000aa) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000ab) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000ac) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000ad) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000ae) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000af) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000b0) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000b1) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000b2) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000b3) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000b4) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000b5) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000b6) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000b7) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000b8) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000b9) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000ba) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000bb) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000bc) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000bd) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000be) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000bf) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000c0) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000c1) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000c2) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000c3) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000c4) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000c5) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000c6) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000c7) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000c8) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000c9) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000ca) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000cb) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000cc) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000cd) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000ce) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000cf) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000d0) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000d1) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000d2) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000d3) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000d4) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000d5) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000d6) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000d7) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000d8) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000d9) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000da) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000db) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000dc) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000dd) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000de) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000df) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000e0) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000e1) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000e2) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000e3) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000e4) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000e5) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000e6) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000e7) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000e8) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000e9) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000ea) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000eb) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000ec) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000ed) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000ee) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000ef) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000f0) #x0000000000000001 (ite (= v140 #x000000000000000000000000000000f1) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000f2) #x0000000000000001 (ite (= v140 #x000000000000000000000000000000f3) #x0000000000000001 (ite (= v140 #x000000000000000000000000000000f4) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000f5) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000f6) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000f7) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000f8) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000f9) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000fa) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000fb) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000fc) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000fd) #x0000000000000000 (ite (= v140 #x000000000000000000000000000000fe) #x0000000000000000 #x0000000000000000)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) #x00000000000000000000000000000000)))) ; 0:0 - 0:0
(assert (not (= ((_ extract 3 0) (bvashr ((_ sign_extend 64) ((_ extract 63 0) ((_ zero_extend 120) v136))) #x00000000000000000000000000000004)) #x4))) ; 0:0 - 0:0
(define-const v152 (bvor (bvand (bvor #x0000000000000 (bvshl ((_ zero_extend 44) v136) #x000000000002c)) #xffffffffffff0) #x0000000000001)) ; 0:0 - 0:0
(define-const v153 ((_ extract 51 44) v152)) ; 1248:0 - 0:0
(define-const v171 ((_ extract 48 0) ((_ sign_extend 64) (bvadd ((_ extract 63 0) ((_ sign_extend 64) ((_ extract 63 0) ((_ sign_extend 80) v49)))) ((_ extract 63 0) ((_ sign_extend 64) ((_ extract 63 0) ((_ sign_extend 80) ((_ extract 47 0) ((_ sign_extend 64) (bvadd #x0000000000000001 ((_ extract 63 0) ((_ sign_extend 64) ((_ extract 63 0) ((_ zero_extend 124) ((_ extract 3 0) v152)))))))))))))))) ; 0:0 - 0:0
(define-const v174 ((_ sign_extend 64) ((_ extract 63 0) ((_ sign_extend 79) v171)))) ; ././././decoding_and_spec_utils.sail 80:11 - 80:55
(assert (ite (not (bvsle #xffffffffffffffffffff800000000000 v174)) false (bvslt v174 #x00000000000000000000800000000000))) ; 0:0 - 0:0
(define-const v179 ((_ extract 47 0) v171)) ; 0:0 - 0:0
(assert (not (= v153 #xc5))) ; 0:0 - 0:0
(define-const v181 (= v153 #xc4)) ; step.sail 2427:63 - 2427:91
(assert (not v181)) ; 0:0 - 0:0
(assert (not v181)) ; 0:0 - 0:0
(define-const v182 (= v153 #x62)) ; step.sail 2440:37 - 2440:61
(assert (not v182)) ; 0:0 - 0:0
(assert (not v182)) ; 0:0 - 0:0
(define-const v185 ((_ sign_extend 64) ((_ extract 63 0) ((_ zero_extend 120) v153)))) ; ././././prefix_modrm_sib_decoding.sail 75:4 - 75:1777
(define-const v186 (ite (= v185 #x00000000000000000000000000000000) true (ite (= v185 #x00000000000000000000000000000001) true (ite (= v185 #x00000000000000000000000000000002) true (ite (= v185 #x00000000000000000000000000000003) true (ite (= v185 #x00000000000000000000000000000004) false (ite (= v185 #x00000000000000000000000000000005) false (ite (= v185 #x00000000000000000000000000000006) false (ite (= v185 #x00000000000000000000000000000007) false (ite (= v185 #x00000000000000000000000000000008) true (ite (= v185 #x00000000000000000000000000000009) true (ite (= v185 #x0000000000000000000000000000000a) true (ite (= v185 #x0000000000000000000000000000000b) true (ite (= v185 #x0000000000000000000000000000000c) false (ite (= v185 #x0000000000000000000000000000000d) false (ite (= v185 #x0000000000000000000000000000000e) false (ite (= v185 #x0000000000000000000000000000000f) false (ite (= v185 #x00000000000000000000000000000010) true (ite (= v185 #x00000000000000000000000000000011) true (ite (= v185 #x00000000000000000000000000000012) true (ite (= v185 #x00000000000000000000000000000013) true (ite (= v185 #x00000000000000000000000000000014) false (ite (= v185 #x00000000000000000000000000000015) false (ite (= v185 #x00000000000000000000000000000016) false (ite (= v185 #x00000000000000000000000000000017) false (ite (= v185 #x00000000000000000000000000000018) true (ite (= v185 #x00000000000000000000000000000019) true (ite (= v185 #x0000000000000000000000000000001a) true (ite (= v185 #x0000000000000000000000000000001b) true (ite (= v185 #x0000000000000000000000000000001c) false (ite (= v185 #x0000000000000000000000000000001d) false (ite (= v185 #x0000000000000000000000000000001e) false (ite (= v185 #x0000000000000000000000000000001f) false (ite (= v185 #x00000000000000000000000000000020) true (ite (= v185 #x00000000000000000000000000000021) true (ite (= v185 #x00000000000000000000000000000022) true (ite (= v185 #x00000000000000000000000000000023) true (ite (= v185 #x00000000000000000000000000000024) false (ite (= v185 #x00000000000000000000000000000025) false (ite (= v185 #x00000000000000000000000000000026) false (ite (= v185 #x00000000000000000000000000000027) false (ite (= v185 #x00000000000000000000000000000028) true (ite (= v185 #x00000000000000000000000000000029) true (ite (= v185 #x0000000000000000000000000000002a) true (ite (= v185 #x0000000000000000000000000000002b) true (ite (= v185 #x0000000000000000000000000000002c) false (ite (= v185 #x0000000000000000000000000000002d) false (ite (= v185 #x0000000000000000000000000000002e) false (ite (= v185 #x0000000000000000000000000000002f) false (ite (= v185 #x00000000000000000000000000000030) true (ite (= v185 #x00000000000000000000000000000031) true (ite (= v185 #x00000000000000000000000000000032) true (ite (= v185 #x00000000000000000000000000000033) true (ite (= v185 #x00000000000000000000000000000034) false (ite (= v185 #x00000000000000000000000000000035) false (ite (= v185 #x00000000000000000000000000000036) false (ite (= v185 #x00000000000000000000000000000037) false (ite (= v185 #x00000000000000000000000000000038) true (ite (= v185 #x00000000000000000000000000000039) true (ite (= v185 #x0000000000000000000000000000003a) true (ite (= v185 #x0000000000000000000000000000003b) true (ite (= v185 #x0000000000000000000000000000003c) false (ite (= v185 #x0000000000000000000000000000003d) false (ite (= v185 #x0000000000000000000000000000003e) false (ite (= v185 #x0000000000000000000000000000003f) false (ite (= v185 #x00000000000000000000000000000040) false (ite (= v185 #x00000000000000000000000000000041) false (ite (= v185 #x00000000000000000000000000000042) false (ite (= v185 #x00000000000000000000000000000043) false (ite (= v185 #x00000000000000000000000000000044) false (ite (= v185 #x00000000000000000000000000000045) false (ite (= v185 #x00000000000000000000000000000046) false (ite (= v185 #x00000000000000000000000000000047) false (ite (= v185 #x00000000000000000000000000000048) false (ite (= v185 #x00000000000000000000000000000049) false (ite (= v185 #x0000000000000000000000000000004a) false (ite (= v185 #x0000000000000000000000000000004b) false (ite (= v185 #x0000000000000000000000000000004c) false (ite (= v185 #x0000000000000000000000000000004d) false (ite (= v185 #x0000000000000000000000000000004e) false (ite (= v185 #x0000000000000000000000000000004f) false (ite (= v185 #x00000000000000000000000000000050) false (ite (= v185 #x00000000000000000000000000000051) false (ite (= v185 #x00000000000000000000000000000052) false (ite (= v185 #x00000000000000000000000000000053) false (ite (= v185 #x00000000000000000000000000000054) false (ite (= v185 #x00000000000000000000000000000055) false (ite (= v185 #x00000000000000000000000000000056) false (ite (= v185 #x00000000000000000000000000000057) false (ite (= v185 #x00000000000000000000000000000058) false (ite (= v185 #x00000000000000000000000000000059) false (ite (= v185 #x0000000000000000000000000000005a) false (ite (= v185 #x0000000000000000000000000000005b) false (ite (= v185 #x0000000000000000000000000000005c) false (ite (= v185 #x0000000000000000000000000000005d) false (ite (= v185 #x0000000000000000000000000000005e) false (ite (= v185 #x0000000000000000000000000000005f) false (ite (= v185 #x00000000000000000000000000000060) false (ite (= v185 #x00000000000000000000000000000061) false (ite (= v185 #x00000000000000000000000000000062) false (ite (= v185 #x00000000000000000000000000000063) true (ite (= v185 #x00000000000000000000000000000064) false (ite (= v185 #x00000000000000000000000000000065) false (ite (= v185 #x00000000000000000000000000000066) false (ite (= v185 #x00000000000000000000000000000067) false (ite (= v185 #x00000000000000000000000000000068) false (ite (= v185 #x00000000000000000000000000000069) true (ite (= v185 #x0000000000000000000000000000006a) false (ite (= v185 #x0000000000000000000000000000006b) true (ite (= v185 #x0000000000000000000000000000006c) false (ite (= v185 #x0000000000000000000000000000006d) false (ite (= v185 #x0000000000000000000000000000006e) false (ite (= v185 #x0000000000000000000000000000006f) false (ite (= v185 #x00000000000000000000000000000070) false (ite (= v185 #x00000000000000000000000000000071) false (ite (= v185 #x00000000000000000000000000000072) false (ite (= v185 #x00000000000000000000000000000073) false (ite (= v185 #x00000000000000000000000000000074) false (ite (= v185 #x00000000000000000000000000000075) false (ite (= v185 #x00000000000000000000000000000076) false (ite (= v185 #x00000000000000000000000000000077) false (ite (= v185 #x00000000000000000000000000000078) false (ite (= v185 #x00000000000000000000000000000079) false (ite (= v185 #x0000000000000000000000000000007a) false (ite (= v185 #x0000000000000000000000000000007b) false (ite (= v185 #x0000000000000000000000000000007c) false (ite (= v185 #x0000000000000000000000000000007d) false (ite (= v185 #x0000000000000000000000000000007e) false (ite (= v185 #x0000000000000000000000000000007f) false (ite (= v185 #x00000000000000000000000000000080) true (ite (= v185 #x00000000000000000000000000000081) true (ite (= v185 #x00000000000000000000000000000082) false (ite (= v185 #x00000000000000000000000000000083) true (ite (= v185 #x00000000000000000000000000000084) true (ite (= v185 #x00000000000000000000000000000085) true (ite (= v185 #x00000000000000000000000000000086) true (ite (= v185 #x00000000000000000000000000000087) true (ite (= v185 #x00000000000000000000000000000088) true (ite (= v185 #x00000000000000000000000000000089) true (ite (= v185 #x0000000000000000000000000000008a) true (ite (= v185 #x0000000000000000000000000000008b) true (ite (= v185 #x0000000000000000000000000000008c) true (ite (= v185 #x0000000000000000000000000000008d) true (ite (= v185 #x0000000000000000000000000000008e) true (ite (= v185 #x0000000000000000000000000000008f) true (ite (= v185 #x00000000000000000000000000000090) false (ite (= v185 #x00000000000000000000000000000091) false (ite (= v185 #x00000000000000000000000000000092) false (ite (= v185 #x00000000000000000000000000000093) false (ite (= v185 #x00000000000000000000000000000094) false (ite (= v185 #x00000000000000000000000000000095) false (ite (= v185 #x00000000000000000000000000000096) false (ite (= v185 #x00000000000000000000000000000097) false (ite (= v185 #x00000000000000000000000000000098) false (ite (= v185 #x00000000000000000000000000000099) false (ite (= v185 #x0000000000000000000000000000009a) false (ite (= v185 #x0000000000000000000000000000009b) false (ite (= v185 #x0000000000000000000000000000009c) false (ite (= v185 #x0000000000000000000000000000009d) false (ite (= v185 #x0000000000000000000000000000009e) false (ite (= v185 #x0000000000000000000000000000009f) false (ite (= v185 #x000000000000000000000000000000a0) false (ite (= v185 #x000000000000000000000000000000a1) false (ite (= v185 #x000000000000000000000000000000a2) false (ite (= v185 #x000000000000000000000000000000a3) false (ite (= v185 #x000000000000000000000000000000a4) false (ite (= v185 #x000000000000000000000000000000a5) false (ite (= v185 #x000000000000000000000000000000a6) false (ite (= v185 #x000000000000000000000000000000a7) false (ite (= v185 #x000000000000000000000000000000a8) false (ite (= v185 #x000000000000000000000000000000a9) false (ite (= v185 #x000000000000000000000000000000aa) false (ite (= v185 #x000000000000000000000000000000ab) false (ite (= v185 #x000000000000000000000000000000ac) false (ite (= v185 #x000000000000000000000000000000ad) false (ite (= v185 #x000000000000000000000000000000ae) false (ite (= v185 #x000000000000000000000000000000af) false (ite (= v185 #x000000000000000000000000000000b0) false (ite (= v185 #x000000000000000000000000000000b1) false (ite (= v185 #x000000000000000000000000000000b2) false (ite (= v185 #x000000000000000000000000000000b3) false (ite (= v185 #x000000000000000000000000000000b4) false (ite (= v185 #x000000000000000000000000000000b5) false (ite (= v185 #x000000000000000000000000000000b6) false (ite (= v185 #x000000000000000000000000000000b7) false (ite (= v185 #x000000000000000000000000000000b8) false (ite (= v185 #x000000000000000000000000000000b9) false (ite (= v185 #x000000000000000000000000000000ba) false (ite (= v185 #x000000000000000000000000000000bb) false (ite (= v185 #x000000000000000000000000000000bc) false (ite (= v185 #x000000000000000000000000000000bd) false (ite (= v185 #x000000000000000000000000000000be) false (ite (= v185 #x000000000000000000000000000000bf) false (ite (= v185 #x000000000000000000000000000000c0) true (ite (= v185 #x000000000000000000000000000000c1) true (ite (= v185 #x000000000000000000000000000000c2) false (ite (= v185 #x000000000000000000000000000000c3) false (ite (= v185 #x000000000000000000000000000000c4) false (ite (= v185 #x000000000000000000000000000000c5) false (ite (= v185 #x000000000000000000000000000000c6) true (ite (= v185 #x000000000000000000000000000000c7) true (ite (= v185 #x000000000000000000000000000000c8) false (ite (= v185 #x000000000000000000000000000000c9) false (ite (= v185 #x000000000000000000000000000000ca) false (ite (= v185 #x000000000000000000000000000000cb) false (ite (= v185 #x000000000000000000000000000000cc) false (ite (= v185 #x000000000000000000000000000000cd) false (ite (= v185 #x000000000000000000000000000000ce) false (ite (= v185 #x000000000000000000000000000000cf) false (ite (= v185 #x000000000000000000000000000000d0) true (ite (= v185 #x000000000000000000000000000000d1) true (ite (= v185 #x000000000000000000000000000000d2) true (ite (= v185 #x000000000000000000000000000000d3) true (ite (= v185 #x000000000000000000000000000000d4) false (ite (= v185 #x000000000000000000000000000000d5) false (ite (= v185 #x000000000000000000000000000000d6) false (ite (= v185 #x000000000000000000000000000000d7) false (ite (= v185 #x000000000000000000000000000000d8) false (ite (= v185 #x000000000000000000000000000000d9) false (ite (= v185 #x000000000000000000000000000000da) false (ite (= v185 #x000000000000000000000000000000db) false (ite (= v185 #x000000000000000000000000000000dc) false (ite (= v185 #x000000000000000000000000000000dd) false (ite (= v185 #x000000000000000000000000000000de) false (ite (= v185 #x000000000000000000000000000000df) false (ite (= v185 #x000000000000000000000000000000e0) false (ite (= v185 #x000000000000000000000000000000e1) false (ite (= v185 #x000000000000000000000000000000e2) false (ite (= v185 #x000000000000000000000000000000e3) false (ite (= v185 #x000000000000000000000000000000e4) false (ite (= v185 #x000000000000000000000000000000e5) false (ite (= v185 #x000000000000000000000000000000e6) false (ite (= v185 #x000000000000000000000000000000e7) false (ite (= v185 #x000000000000000000000000000000e8) false (ite (= v185 #x000000000000000000000000000000e9) false (ite (= v185 #x000000000000000000000000000000ea) false (ite (= v185 #x000000000000000000000000000000eb) false (ite (= v185 #x000000000000000000000000000000ec) false (ite (= v185 #x000000000000000000000000000000ed) false (ite (= v185 #x000000000000000000000000000000ee) false (ite (= v185 #x000000000000000000000000000000ef) false (ite (= v185 #x000000000000000000000000000000f0) false (ite (= v185 #x000000000000000000000000000000f1) false (ite (= v185 #x000000000000000000000000000000f2) false (ite (= v185 #x000000000000000000000000000000f3) false (ite (= v185 #x000000000000000000000000000000f4) false (ite (= v185 #x000000000000000000000000000000f5) false (ite (= v185 #x000000000000000000000000000000f6) true (ite (= v185 #x000000000000000000000000000000f7) true (ite (= v185 #x000000000000000000000000000000f8) false (ite (= v185 #x000000000000000000000000000000f9) false (ite (= v185 #x000000000000000000000000000000fa) false (ite (= v185 #x000000000000000000000000000000fb) false (ite (= v185 #x000000000000000000000000000000fc) false (ite (= v185 #x000000000000000000000000000000fd) false (ite (= v185 #x000000000000000000000000000000fe) true true)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ; 0:0 - 0:0
(assert v186) ; 0:0 - 0:0
(assert (not v181)) ; 0:0 - 0:0
(assert (not v182)) ; 0:0 - 0:0
(assert (not (= #x67 ((_ extract 43 36) v152)))) ; 0:0 - 0:0
(define-const v189 ((_ sign_extend 16) v179)) ; step.sail 2459:103 - 2459:133
(define-const v192 ((_ sign_extend 64) ((_ extract 63 0) ((_ sign_extend 64) v189)))) ; ./segmentation.sail 262:20 - 262:57
(assert (not (not (ite (not (bvsle #xffffffffffffffffffff800000000000 v192)) false (bvslt v192 #x00000000000000000000800000000000))))) ; 0:0 - 0:0
(define-const v198 ((_ sign_extend 64) v189)) ; prelude.sail 682:36 - 682:48
(assert (not (not (ite (not (bvsle #xffffffffffffffffffff800000000000 v198)) false (bvslt v198 #x00000000000000000000800000000000))))) ; 0:0 - 0:0
(define-const v207 ((_ zero_extend 12) ((_ sign_extend 4) (bvadd ((_ extract 47 0) v189) #x000000000000)))) ; /home/mbmcloug/.opam/4.10.0/share/sail/lib/vector.sail 141:76 - 141:100
(declare-const v208 (_ BitVec 8)) ; 0:0 - 0:0
(assert (and (and (bvule #x0000000000401000 v207) (bvult (bvadd ((_ zero_extend 65) v207) ((_ zero_extend 65) #x0000000000000001)) ((_ zero_extend 65) #x0000000000411000))) (= v208 (select v35 v207)))) ; 0:0 - 0:0
(read-mem v208 |Read_plain| v207 1)
(define-const v210 (bvor #x00 v208)) ; 0:0 - 0:0
(assert v186) ; 0:0 - 0:0
(define-const v217 ((_ extract 48 0) ((_ sign_extend 64) (bvadd ((_ extract 63 0) ((_ sign_extend 64) ((_ extract 63 0) ((_ sign_extend 80) v179)))) #x0000000000000001)))) ; 0:0 - 0:0
(define-const v220 ((_ sign_extend 64) ((_ extract 63 0) ((_ sign_extend 79) v217)))) ; ././././decoding_and_spec_utils.sail 80:11 - 80:55
(assert (ite (not (bvsle #xffffffffffffffffffff800000000000 v220)) false (bvslt v220 #x00000000000000000000800000000000))) ; 0:0 - 0:0
(assert v186) ; 0:0 - 0:0
(assert (not (= #x67 ((_ extract 43 36) v152)))) ; 0:0 - 0:0
(assert (not (= ((_ extract 2 0) v210) #b100))) ; 0:0 - 0:0
(assert (not (= ((_ zero_extend 120) v153) #x00000000000000000000000000000000))) ; 0:0 - 0:0
(assert (not (not (= ((_ zero_extend 120) v153) #x00000000000000000000000000000001)))) ; 0:0 - 0:0
(assert (= ((_ extract 7 6) v210) #b11)) ; 0:0 - 0:0
(assert (not (= #xf0 ((_ extract 11 4) v152)))) ; 0:0 - 0:0
(define-const v243 ((_ extract 2 0) v210)) ; 392:0 - 0:0
(define-const v244 ((_ extract 7 6) v210)) ; 381:0 - 0:0
(assert (not (= #b0 (bvand #b1 ((_ extract 0 0) v153))))) ; 0:0 - 0:0
(assert (= ((_ extract 0 0) (bvlshr v85 #x03)) #b1)) ; 0:0 - 0:0
(assert (= ((_ extract 0 0) (bvlshr v85 #x02)) #b1)) ; 0:0 - 0:0
(define-const v260 ((_ sign_extend 64) ((_ extract 63 0) ((_ zero_extend 124) (bvor #x8 ((_ zero_extend 1) ((_ extract 5 3) v210))))))) ; ./././././register_readers_and_writers.sail 210:4 - 210:23
(assert (bvsle #x00000000000000000000000000000000 v260)) ; 0:0 - 0:0
(assert (bvslt v260 #x00000000000000000000000000000010)) ; 0:0 - 0:0
(define-const v263 ((_ extract 63 0) v260)) ; register_accessors.sail 7:20 - 7:36
(assert (not (= ((_ sign_extend 64) v263) #x00000000000000000000000000000000))) ; 0:0 - 0:0
(assert (not (= ((_ sign_extend 64) v263) #x00000000000000000000000000000001))) ; 0:0 - 0:0
(assert (not (= ((_ sign_extend 64) v263) #x00000000000000000000000000000002))) ; 0:0 - 0:0
(assert (not (= ((_ sign_extend 64) v263) #x00000000000000000000000000000003))) ; 0:0 - 0:0
(assert (not (= ((_ sign_extend 64) v263) #x00000000000000000000000000000004))) ; 0:0 - 0:0
(assert (not (= ((_ sign_extend 64) v263) #x00000000000000000000000000000005))) ; 0:0 - 0:0
(assert (not (= ((_ sign_extend 64) v263) #x00000000000000000000000000000006))) ; 0:0 - 0:0
(assert (not (= ((_ sign_extend 64) v263) #x00000000000000000000000000000007))) ; 0:0 - 0:0
(assert (not (= ((_ sign_extend 64) v263) #x00000000000000000000000000000008))) ; 0:0 - 0:0
(assert (not (= ((_ sign_extend 64) v263) #x00000000000000000000000000000009))) ; 0:0 - 0:0
(assert (not (= ((_ sign_extend 64) v263) #x0000000000000000000000000000000a))) ; 0:0 - 0:0
(assert (not (= ((_ sign_extend 64) v263) #x0000000000000000000000000000000b))) ; 0:0 - 0:0
(assert (not (= ((_ sign_extend 64) v263) #x0000000000000000000000000000000c))) ; 0:0 - 0:0
(assert (not (not (= ((_ sign_extend 64) v263) #x0000000000000000000000000000000d)))) ; 0:0 - 0:0
(read-reg |r13| nil v24)
(define-const v306 ((_ extract 27 20) v152)) ; 1335:0 - 0:0
(assert (not (= ((_ zero_extend 120) v306) #x0000000000000000000000000000002e))) ; 0:0 - 0:0
(assert (not (= ((_ zero_extend 120) v306) #x00000000000000000000000000000036))) ; 0:0 - 0:0
(assert (not (= ((_ zero_extend 120) v306) #x0000000000000000000000000000003e))) ; 0:0 - 0:0
(assert (not (= ((_ zero_extend 120) v306) #x00000000000000000000000000000026))) ; 0:0 - 0:0
(assert (not (= ((_ zero_extend 120) v306) #x00000000000000000000000000000064))) ; 0:0 - 0:0
(assert (not (= ((_ zero_extend 120) v306) #x00000000000000000000000000000065))) ; 0:0 - 0:0
(assert (not (= #x67 ((_ extract 43 36) v152)))) ; 0:0 - 0:0
(assert (not (= v244 #b01))) ; 0:0 - 0:0
(assert (not (= v244 #b10))) ; 0:0 - 0:0
(assert (not (not (= v244 #b11)))) ; 0:0 - 0:0
(assert (= v244 #b11)) ; 0:0 - 0:0
(assert (= v244 #b11)) ; 0:0 - 0:0
(assert (not (= ((_ extract 0 0) (bvlshr v85 #x00)) #b1))) ; 0:0 - 0:0
(define-const v340 ((_ sign_extend 64) ((_ extract 63 0) ((_ zero_extend 124) ((_ zero_extend 1) v243))))) ; ./././././register_readers_and_writers.sail 210:4 - 210:23
(assert (bvsle #x00000000000000000000000000000000 v340)) ; 0:0 - 0:0
(assert (bvslt v340 #x00000000000000000000000000000010)) ; 0:0 - 0:0
(define-const v343 ((_ extract 63 0) v340)) ; register_accessors.sail 7:20 - 7:36
(assert (not (= ((_ sign_extend 64) v343) #x00000000000000000000000000000000))) ; 0:0 - 0:0
(assert (not (= ((_ sign_extend 64) v343) #x00000000000000000000000000000001))) ; 0:0 - 0:0
(assert (not (not (= ((_ sign_extend 64) v343) #x00000000000000000000000000000002)))) ; 0:0 - 0:0
(read-reg |rdx| nil v33)
(define-const v359 ((_ extract 48 0) ((_ sign_extend 64) ((_ extract 63 0) ((_ sign_extend 64) ((_ extract 63 0) ((_ sign_extend 80) ((_ extract 47 0) v217)))))))) ; 0:0 - 0:0
(define-const v362 ((_ sign_extend 64) ((_ extract 63 0) ((_ sign_extend 79) v359)))) ; ././././decoding_and_spec_utils.sail 80:11 - 80:55
(assert (ite (not (bvsle #xffffffffffffffffffff800000000000 v362)) false (bvslt v362 #x00000000000000000000800000000000))) ; 0:0 - 0:0
(define-const v367 ((_ extract 47 0) v359)) ; 0:0 - 0:0
(assert (not (bvslt #x0000000000000000000000000000000f ((_ sign_extend 64) ((_ extract 63 0) ((_ sign_extend 78) ((_ extract 49 0) ((_ sign_extend 64) (bvsub ((_ extract 63 0) ((_ sign_extend 64) ((_ extract 63 0) ((_ sign_extend 79) ((_ extract 48 0) ((_ sign_extend 64) ((_ extract 63 0) ((_ sign_extend 64) ((_ extract 63 0) ((_ sign_extend 80) ((_ extract 47 0) ((_ sign_extend 80) v367)))))))))))) ((_ extract 63 0) ((_ sign_extend 64) ((_ extract 63 0) ((_ sign_extend 80) ((_ extract 47 0) ((_ sign_extend 80) v49))))))))))))))) ; 0:0 - 0:0
(declare-const v392 (_ BitVec 32)) ; ./././arith_and_logic.sail 43:36 - 43:42
(read-reg |rflags| nil (_ struct (|bits| v392)))
(define-const v393 ((_ extract 63 0) ((_ zero_extend 64) v33))) ; 0:0 - 0:0
(define-const v397 (bvadd ((_ extract 64 0) ((_ zero_extend 64) v393)) ((_ extract 64 0) ((_ zero_extend 64) v24)))) ; 0:0 - 0:0
(define-const v406 ((_ extract 63 0) v397)) ; 0:0 - 0:0
(define-const v407 ((_ zero_extend 63) v397)) ; ././././././rflags_spec.sail 38:46 - 38:66
(assert (bvsle #x00000000000000000000000000000000 v407)) ; 0:0 - 0:0
(define-const v410 (not (bvslt v407 #x00000000000000010000000000000000))) ; ././././././rflags_spec.sail 38:17 - 38:68
(define-const v418 ((_ extract 7 0) v406)) ; 0:0 - 0:0
(define-const v471 (not (ite (not (not (= (bvadd ((_ extract 0 0) (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ((_ sign_extend 64) ((_ extract 63 0) ((_ zero_extend 127) (bvor #b0 ((_ extract 0 0) (bvlshr v418 #x00)))))) ((_ sign_extend 64) ((_ extract 63 0) ((_ zero_extend 127) (bvor #b0 ((_ extract 0 0) (bvlshr v418 #x01))))))) ((_ sign_extend 64) ((_ extract 63 0) ((_ zero_extend 127) (bvor #b0 ((_ extract 0 0) (bvlshr v418 #x02))))))) ((_ sign_extend 64) ((_ extract 63 0) ((_ zero_extend 127) (bvor #b0 ((_ extract 0 0) (bvlshr v418 #x03))))))) ((_ sign_extend 64) ((_ extract 63 0) ((_ zero_extend 127) (bvor #b0 ((_ extract 0 0) (bvlshr v418 #x04))))))) ((_ sign_extend 64) ((_ extract 63 0) ((_ zero_extend 127) (bvor #b0 ((_ extract 0 0) (bvlshr v418 #x05))))))) ((_ sign_extend 64) ((_ extract 63 0) ((_ zero_extend 127) (bvor #b0 ((_ extract 0 0) (bvlshr v418 #x06)))))))) ((_ extract 0 0) ((_ sign_extend 64) ((_ extract 63 0) ((_ zero_extend 127) (bvor #b0 ((_ extract 0 0) (bvlshr v418 #x07)))))))) #b1))) true false))) ; ../test-generation-patches/logcount_alt.sail 35:17 - 35:69
(define-const v494 (bvslt #x0000000000000000000000000000000f ((_ sign_extend 64) ((_ extract 63 0) ((_ zero_extend 123) ((_ extract 4 0) ((_ sign_extend 64) (bvadd ((_ extract 63 0) ((_ sign_extend 64) ((_ extract 63 0) ((_ zero_extend 124) ((_ extract 3 0) v393))))) ((_ extract 63 0) ((_ sign_extend 64) ((_ extract 63 0) ((_ zero_extend 124) ((_ extract 3 0) v24))))))))))))) ; ././././././rflags_spec.sail 205:36 - 205:54
(define-const v507 ((_ sign_extend 63) (bvadd ((_ extract 64 0) ((_ sign_extend 64) ((_ extract 63 0) ((_ sign_extend 64) v393)))) ((_ extract 64 0) ((_ sign_extend 64) ((_ extract 63 0) ((_ sign_extend 64) v24))))))) ; ././././././rflags_spec.sail 76:44 - 76:69
(define-const v512 (not (ite (not (bvsle #xffffffffffffffff8000000000000000 v507)) false (bvslt v507 #x00000000000000008000000000000000)))) ; ././././././rflags_spec.sail 76:17 - 76:71
(define-const v525 (bvor (bvand (bvor (bvand (bvor (bvand (bvor (bvand (bvor (bvand (bvor (bvand v392 #xfffffffe) ((_ zero_extend 31) (ite (and (not (= v410 true)) (not (not (= v410 false)))) #b0 #b1))) #xfffffffb) (bvshl ((_ zero_extend 31) (ite (and (not (= v471 true)) (not (not (= v471 false)))) #b0 #b1)) #x00000002)) #xffffffef) (bvshl ((_ zero_extend 31) (ite (and (not (= v494 true)) (not (not (= v494 false)))) #b0 #b1)) #x00000004)) #xffffffbf) (bvshl ((_ zero_extend 31) (ite (not (= ((_ zero_extend 64) v406) #x00000000000000000000000000000000)) #b0 #b1)) #x00000006)) #xffffff7f) (bvshl ((_ zero_extend 31) ((_ extract 63 63) v406)) #x00000007)) #xfffff7ff) (bvshl ((_ zero_extend 31) (ite (and (not (= v512 true)) (not (not (= v512 false)))) #b0 #b1)) #x0000000b))) ; 0:0 - 0:0
(assert (= v244 #b11)) ; 0:0 - 0:0
(assert (not (= ((_ extract 0 0) (bvlshr v85 #x00)) #b1))) ; 0:0 - 0:0
(define-const v531 ((_ extract 63 0) ((_ zero_extend 64) v406))) ; 0:0 - 0:0
(define-const v534 ((_ sign_extend 64) ((_ extract 63 0) ((_ zero_extend 124) ((_ zero_extend 1) v243))))) ; ./././././register_readers_and_writers.sail 218:4 - 218:38
(assert (bvsle #x00000000000000000000000000000000 v534)) ; 0:0 - 0:0
(assert (bvslt v534 #x00000000000000000000000000000010)) ; 0:0 - 0:0
(define-const v537 ((_ extract 63 0) v534)) ; register_accessors.sail 13:4 - 13:55
(assert (not (= ((_ sign_extend 64) v537) #x00000000000000000000000000000000))) ; 0:0 - 0:0
(assert (not (= ((_ sign_extend 64) v537) #x00000000000000000000000000000001))) ; 0:0 - 0:0
(assert (not (not (= ((_ sign_extend 64) v537) #x00000000000000000000000000000002)))) ; 0:0 - 0:0
(write-reg |rdx| nil v531)
(read-reg |log_register_writes| nil false)
(define-const v548 (bvor (bvand v392 #xfffffffe) ((_ zero_extend 31) ((_ extract 0 0) v525)))) ; 0:0 - 0:0
(write-reg |rflags| nil (_ struct (|bits| v548)))
(read-reg |rflags| nil (_ struct (|bits| v548)))
(define-const v550 (bvor (bvand v548 #xfffffffb) (bvshl ((_ zero_extend 31) ((_ extract 2 2) v525)) #x00000002))) ; 0:0 - 0:0
(write-reg |rflags| nil (_ struct (|bits| v550)))
(read-reg |rflags| nil (_ struct (|bits| v550)))
(define-const v552 (bvor (bvand v550 #xffffffef) (bvshl ((_ zero_extend 31) ((_ extract 4 4) v525)) #x00000004))) ; 0:0 - 0:0
(write-reg |rflags| nil (_ struct (|bits| v552)))
(read-reg |rflags| nil (_ struct (|bits| v552)))
(define-const v554 (bvor (bvand v552 #xffffffbf) (bvshl ((_ zero_extend 31) ((_ extract 6 6) v525)) #x00000006))) ; 0:0 - 0:0
(write-reg |rflags| nil (_ struct (|bits| v554)))
(read-reg |rflags| nil (_ struct (|bits| v554)))
(define-const v556 (bvor (bvand v554 #xffffff7f) (bvshl ((_ zero_extend 31) ((_ extract 7 7) v525)) #x00000007))) ; 0:0 - 0:0
(write-reg |rflags| nil (_ struct (|bits| v556)))
(read-reg |rflags| nil (_ struct (|bits| v556)))
(define-const v558 (bvor (bvand v556 #xfffff7ff) (bvshl ((_ zero_extend 31) ((_ extract 11 11) v525)) #x0000000b))) ; 0:0 - 0:0
(write-reg |rflags| nil (_ struct (|bits| v558)))
(define-const v559 ((_ sign_extend 16) v367)) ; register_accessors.sail 21:26 - 21:53
(write-reg |rip| nil v559))
Raw
x64footprint.rs
use clap::Parser;
use crossbeam::queue::SegQueue;
use isla_lib::init::{initialize_architecture, Initialized};
use isla_lib::ir::{AssertionMode, Def, IRTypeInfo, Name, Symtab, Ty, Val};
use isla_lib::ir_lexer::new_ir_lexer;
use isla_lib::ir_parser;
use isla_lib::log;
use isla_lib::memory::{Memory, SmtKind};
use isla_lib::simplify::{self, WriteOpts};
use isla_lib::smt::smtlib::{self, bits64};
use isla_lib::smt::{self, Checkpoint, Event, ReadOpts, Solver, Sym};
use isla_lib::source_loc::SourceLoc;
use isla_lib::{
bitvector::{b64::B64, BV},
zencode,
};
use isla_lib::{config::ISAConfig, executor::unfreeze_frame};
use isla_lib::{
error::{ExecError, IslaError},
memory::Address,
};
use isla_lib::{
executor::{self, freeze_frame, LocalFrame, TaskState},
ir::linearize,
};
use sha2::{Digest, Sha256};
use std::io::prelude::*;
use std::io::BufWriter;
use std::path::PathBuf;
use std::sync::Arc;
#[derive(Parser)]
struct Options {
/// Architecture definition.
#[clap(long)]
arch: PathBuf,
/// ISA config file.
#[clap(long)]
isa_config: PathBuf,
/// Trace output directory.
#[clap(long, default_value = ".")]
output_dir: PathBuf,
}
fn main() -> anyhow::Result<()> {
let options = Options::parse();
log::set_flags(log::VERBOSE);
// Parse ISLA Architecture.
let contents = std::fs::read_to_string(&options.arch)?;
let mut symtab = Symtab::new();
let mut arch = parse_ir::<B64>(&contents, &mut symtab)?;
// ISLA ISA Config.
let mut hasher = Sha256::new();
let type_info = IRTypeInfo::new(&arch);
let isa_config = match ISAConfig::<B64>::from_file(
&mut hasher,
&options.isa_config,
None,
&symtab,
&type_info,
) {
Ok(isa_config) => isa_config,
Err(msg) => anyhow::bail!(msg),
};
let linearize_functions = vec![
// See: https://github.com/rems-project/isla-testgen/blob/a9759247bfdff9c9c39d95a4cfd85318e5bf50fe/c86-command
//"fdiv_int",
"bool_to_bits",
"bits_to_bool",
//"bit_to_bool",
//"isEven",
"signed_byte_p_int",
"zf_spec",
//"b_xor",
//"logand_int",
//"not_bit",
//"floor2",
];
for name in linearize_functions {
linearize_function(&mut arch, name, &mut symtab)?;
}
let use_model_reg_init = true;
let iarch = initialize_architecture(
&mut arch,
symtab,
type_info,
&isa_config,
AssertionMode::Optimistic,
use_model_reg_init,
);
// Setup machine code.
let machine_code = vec![0x4c, 0x01, 0xea];
println!("machine code = {:02x?}", machine_code);
// ISLA trace.
let paths = trace_opcode(&machine_code, &iarch)?;
// Dump.
for (i, events) in paths.iter().enumerate() {
let filename = format!("trace{i:04}.out");
let path = options.output_dir.join(filename);
log!(log::VERBOSE, format!("write trace to {}", path.display()));
let file = std::fs::File::create(path)?;
write_events(&events, &iarch, file)?;
}
log!(
log::VERBOSE,
format!("generated {} trace paths", paths.len())
);
Ok(())
}
fn trace_opcode<'ir, B: BV>(
opcode: &Vec<u8>,
iarch: &'ir Initialized<'ir, B>,
) -> anyhow::Result<Vec<Vec<Event<B>>>> {
let shared_state = &&iarch.shared_state;
let symtab = &shared_state.symtab;
let initial_checkpoint = Checkpoint::new();
let solver_cfg = smt::Config::new();
let solver_ctx = smt::Context::new(solver_cfg);
let mut solver = Solver::from_checkpoint(&solver_ctx, initial_checkpoint);
let memory = Memory::new();
// Initialization -----------------------------------------------------------
// - run initialization function to set processor in 64-bit mode
let init_function = zencode::encode("initialise_64_bit_mode");
let function_id = shared_state.symtab.lookup(&init_function);
let (args, ret_ty, instrs) = shared_state.functions.get(&function_id).unwrap();
let task_state = TaskState::<B>::new();
let checkpoint = smt::checkpoint(&mut solver);
let task = LocalFrame::new(function_id, args, ret_ty, None, instrs)
.add_lets(&iarch.lets)
.add_regs(&iarch.regs)
.set_memory(memory)
.task_with_checkpoint(0, &task_state, checkpoint);
let queue = Arc::new(SegQueue::new());
executor::start_single(
task,
&shared_state,
&queue,
&move |_tid, _task_id, result, _shared_state, mut solver, queue| match result {
Ok((_, frame)) => {
queue.push((freeze_frame(&frame), smt::checkpoint(&mut solver)));
}
Err(err) => panic!("Initialisation failed: {:?}", err),
},
);
assert_eq!(queue.len(), 1);
let (frame, checkpoint) = queue.pop().expect("pop failed");
let mut solver = Solver::from_checkpoint(&solver_ctx, checkpoint);
// Initialize registers -----------------------------------------------------
// - set symbolic values for all general-purpose registers
let mut local_frame = executor::unfreeze_frame(&frame);
for (n, ty) in &shared_state.registers {
// Only handle general-purpose registers.
if let Ty::Bits(bits) = ty {
let var = solver.fresh();
solver.add(smtlib::Def::DeclareConst(var, smtlib::Ty::BitVec(*bits)));
let val = Val::Symbolic(var);
local_frame.regs_mut().assign(*n, val, shared_state);
}
}
let frame = freeze_frame(&local_frame);
// Setup memory -------------------------------------------------------------
let mut local_frame = unfreeze_frame(&frame);
const INIT_PC: Address = 0x401000;
local_frame
.memory_mut()
.add_symbolic_code_region(INIT_PC..INIT_PC + 0x10000);
let memory_var = solver.fresh();
solver.add(smtlib::Def::DeclareConst(
memory_var,
smtlib::Ty::Array(
Box::new(smtlib::Ty::BitVec(64)),
Box::new(smtlib::Ty::BitVec(8)),
),
));
let memory_client_info: Box<dyn isla_lib::memory::MemoryCallbacks<B>> =
Box::new(SeqMemory { memory_var });
local_frame.memory_mut().set_client_info(memory_client_info);
let frame = freeze_frame(&local_frame);
// Set initial program counter ----------------------------------------------
let local_frame = unfreeze_frame(&frame);
let pc_name = zencode::encode("rip");
let pc_id = symtab.lookup(&pc_name);
let pc = local_frame.regs().get_last_if_initialized(pc_id).unwrap();
solver.add(smtlib::Def::Assert(smtlib::Exp::Eq(
Box::new(smt_value(pc).unwrap()),
Box::new(smtlib::Exp::Bits64(B64::from_u64(INIT_PC))),
)));
let frame = freeze_frame(&local_frame);
// Setup opcode -------------------------------------------------------------
let local_frame = unfreeze_frame(&frame);
let read_val = local_frame
.memory()
.read(
Val::Unit, /* read_kind */
pc.clone(),
Val::I128(opcode.len() as i128),
&mut solver,
false,
ReadOpts::ifetch(),
)
.unwrap();
let opcode_var = solver.fresh();
solver.add(smtlib::Def::DeclareConst(
opcode_var,
smtlib::Ty::BitVec(8 * opcode.len() as u32),
));
solver.add(smtlib::Def::Assert(smtlib::Exp::Eq(
Box::new(smtlib::Exp::Var(opcode_var)),
Box::new(smt_bytes(opcode)),
)));
let read_exp = smt_value(&read_val).unwrap();
solver.add(smtlib::Def::Assert(smtlib::Exp::Eq(
Box::new(smtlib::Exp::Var(opcode_var)),
Box::new(read_exp),
)));
let frame = freeze_frame(&local_frame);
// Debug dump ---------------------------------------------------------------
assert_eq!(solver.check_sat(), smt::SmtResult::Sat);
let checkpoint = smt::checkpoint(&mut solver);
dump_checkpoint(&checkpoint, iarch)?;
// Execute fetch and decode -------------------------------------------------
let local_frame = unfreeze_frame(&frame);
local_frame.memory().log();
let run_instruction_function = zencode::encode("x86_fetch_decode_execute");
let function_id = shared_state.symtab.lookup(&run_instruction_function);
let (args, ret_ty, instrs) = shared_state.functions.get(&function_id).unwrap();
let task_state = TaskState::<B>::new();
let task = local_frame
.new_call(function_id, args, ret_ty, None, instrs)
.task_with_checkpoint(1, &task_state, checkpoint);
let num_threads = 1;
let queue = Arc::new(SegQueue::new());
executor::start_multi(
num_threads,
None,
vec![task],
shared_state,
queue.clone(),
&executor::trace_collector,
);
let mut paths = Vec::new();
loop {
match queue.pop() {
Some(Ok((_, mut events))) => {
// simplify::hide_initialization(&mut events);
simplify::remove_extra_register_fields(&mut events);
simplify::remove_repeated_register_reads(&mut events);
simplify::remove_unused_register_assumptions(&mut events);
simplify::remove_unused(&mut events);
simplify::propagate_forwards_used_once(&mut events);
simplify::commute_extract(&mut events);
simplify::eval(&mut events);
let events: Vec<Event<B>> = events.drain(..).rev().collect();
paths.push(events);
}
// Error during execution
Some(Err(err)) => {
let msg = format!("{}", err);
eprintln!(
"{}",
err.source_loc().message::<PathBuf>(
None,
shared_state.symtab.files(),
&msg,
true,
true
)
);
anyhow::bail!("{}", err);
}
// Empty queue
None => break,
}
}
Ok(paths)
}
#[derive(Debug, Clone)]
struct SeqMemory {
memory_var: Sym,
}
impl<B: BV> isla_lib::memory::MemoryCallbacks<B> for SeqMemory {
fn symbolic_read(
&self,
regions: &[isla_lib::memory::Region<B>],
solver: &mut Solver<B>,
value: &Val<B>,
_read_kind: &Val<B>,
address: &Val<B>,
bytes: u32,
_tag: &Option<Val<B>>,
opts: &ReadOpts,
) {
use isla_lib::smt::smtlib::{Def, Exp};
let read_exp = smt_value(value)
.unwrap_or_else(|err| panic!("Bad memory read value {:?}: {}", value, err));
let addr_exp = smt_value(address)
.unwrap_or_else(|err| panic!("Bad read address value {:?}: {}", address, err));
let read_prop = Exp::Eq(
Box::new(read_exp.clone()),
Box::new(smt_read_exp(self.memory_var, &addr_exp, bytes as u64)),
);
let kind = if opts.is_ifetch {
SmtKind::ReadInstr
} else if opts.is_exclusive {
// We produce a dummy read so that failed store exclusives still get address
// constraints, but the memory must be writable.
SmtKind::WriteData
} else {
SmtKind::ReadData
};
let address_constraint =
isla_lib::memory::smt_address_constraint(regions, &addr_exp, bytes, kind, solver, None);
let full_constraint = Exp::And(Box::new(address_constraint), Box::new(read_prop));
solver.add(Def::Assert(full_constraint));
}
fn symbolic_write(
&mut self,
regions: &[isla_lib::memory::Region<B>],
solver: &mut Solver<B>,
_value: Sym,
_read_kind: &Val<B>,
address: &Val<B>,
data: &Val<B>,
bytes: u32,
_tag: &Option<Val<B>>,
_opts: &smt::WriteOpts,
) {
use isla_lib::smt::smtlib::{Def, Exp};
let data_exp = smt_value(data)
.unwrap_or_else(|err| panic!("Bad memory write value {:?}: {}", data, err));
let addr_exp = smt_value(address)
.unwrap_or_else(|err| panic!("Bad write address value {:?}: {}", address, err));
// TODO: endianness?
let mut mem_exp = Exp::Store(
Box::new(Exp::Var(self.memory_var)),
Box::new(addr_exp.clone()),
Box::new(Exp::Extract(7, 0, Box::new(data_exp.clone()))),
);
for i in 1..bytes {
mem_exp = Exp::Store(
Box::new(mem_exp),
Box::new(Exp::Bvadd(
Box::new(addr_exp.clone()),
Box::new(bits64(i as u64, 64)),
)),
Box::new(Exp::Extract(i * 8 + 7, i * 8, Box::new(data_exp.clone()))),
)
}
self.memory_var = solver.fresh();
solver.add(Def::DefineConst(self.memory_var, mem_exp));
let kind = SmtKind::WriteData;
let address_constraint =
isla_lib::memory::smt_address_constraint(regions, &addr_exp, bytes, kind, solver, None);
solver.add(Def::Assert(address_constraint));
}
fn symbolic_write_tag(
&mut self,
_regions: &[isla_lib::memory::Region<B>],
_solver: &mut Solver<B>,
_value: Sym,
_write_kind: &Val<B>,
_address: &Val<B>,
_tag: &Val<B>,
) {
}
}
fn smt_value<B: BV>(v: &Val<B>) -> Result<smtlib::Exp<Sym>, ExecError> {
isla_lib::primop_util::smt_value(v, SourceLoc::unknown())
}
fn smt_read_exp(memory: Sym, addr_exp: &smtlib::Exp<Sym>, bytes: u64) -> smtlib::Exp<Sym> {
use smtlib::Exp;
// TODO: endianness?
let mut mem_exp = Exp::Select(Box::new(Exp::Var(memory)), Box::new(addr_exp.clone()));
for i in 1..bytes {
mem_exp = Exp::Concat(
Box::new(Exp::Select(
Box::new(Exp::Var(memory)),
Box::new(Exp::Bvadd(
Box::new(addr_exp.clone()),
Box::new(bits64(i as u64, 64)),
)),
)),
Box::new(mem_exp),
)
}
mem_exp
}
fn smt_bytes<V>(bytes: &Vec<u8>) -> smtlib::Exp<V> {
let mut bits = Vec::with_capacity(bytes.len() * 8);
for byte in bytes {
for i in 0..8 {
bits.push((byte >> i) & 1 == 1);
}
}
smtlib::Exp::Bits(bits)
}
fn dump_checkpoint<'ir, B: BV>(
checkpoint: &Checkpoint<B>,
iarch: &'ir Initialized<'ir, B>,
) -> anyhow::Result<()> {
if let Some(trace) = checkpoint.trace() {
let events: Vec<Event<B>> = trace.to_vec().into_iter().cloned().collect();
write_events_to_stdout(&events, iarch)?;
}
Ok(())
}
/// Write ISLA trace events to stdout.
fn write_events_to_stdout<'ir, B: BV>(
events: &Vec<Event<B>>,
iarch: &'ir Initialized<'ir, B>,
) -> anyhow::Result<()> {
let stdout = std::io::stdout().lock();
write_events(events, iarch, stdout)
}
fn write_events<'ir, B: BV>(
events: &Vec<Event<B>>,
iarch: &'ir Initialized<'ir, B>,
w: impl Sized + Write,
) -> anyhow::Result<()> {
let mut handle = BufWriter::with_capacity(5 * usize::pow(2, 20), w);
let write_opts = WriteOpts::default();
simplify::write_events_with_opts(&mut handle, &events, &iarch.shared_state, &write_opts)
.unwrap();
handle.flush().unwrap();
Ok(())
}
/// Parse Jib IR.
fn parse_ir<'a, 'input, B: BV>(
contents: &'input str,
symtab: &'a mut Symtab<'input>,
) -> anyhow::Result<Vec<Def<Name, B>>> {
match ir_parser::IrParser::new().parse(symtab, new_ir_lexer(&contents)) {
Ok(ir) => Ok(ir),
Err(_) => Err(anyhow::Error::msg("bad")),
}
}
fn linearize_function<'ir, B: BV>(
arch: &mut Vec<Def<Name, B>>,
name: &str,
symtab: &mut Symtab<'ir>,
) -> anyhow::Result<()> {
log!(log::VERBOSE, format!("linearize function {}", name));
// Lookup function name.
let target = match symtab.get(&zencode::encode(name)) {
Some(t) => t,
None => anyhow::bail!("function {} could not be found", name),
};
// Find signature.
let (_args, ret) = lookup_signature(arch, target)?;
// Rewrite.
for def in arch.iter_mut() {
if let Def::Fn(f, _, body) = def {
if *f == target {
let rewritten = linearize::linearize(body.to_vec(), &ret, symtab);
*body = rewritten;
}
}
}
Ok(())
}
fn lookup_signature<B: BV>(
arch: &Vec<Def<Name, B>>,
target: Name,
) -> anyhow::Result<(Vec<Ty<Name>>, Ty<Name>)> {
for def in arch {
match def {
Def::Val(f, args, ret) if *f == target => return Ok((args.clone(), ret.clone())),
_ => (),
}
}
anyhow::bail!("could not find type signature")
}
Raw
x86.toml
pc = "rip"
ifetch = "Read_ifetch"
read_exclusives = []
write_exclusives = []
[[toolchain]]
name = "default"
assembler = "as"
objdump = "objdump"
nm = "nm"
linker = "ld"
[mmu]
page_table_base = "0x300000"
page_size = "4096"
s2_page_table_base = "0x300000"
s2_page_size = "4096"
# This section contains the base address for loading the code for each
# thread in a litmus test, and the stride which is the distance
# between each thread in bytes. The overall range for thread memory is
# the half-open range [base,top)"
[threads]
base = "0x400000"
top = "0x500000"
stride = "0x10000"
[symbolic_addrs]
base = "0x600000"
top = "0x600000"
stride = "0x10"
[registers]
ignore = []
[registers.defaults]
app_view = true
ms_reg = false
fault_reg = false
log_register_writes = false
# A map from register names in the litmus to Sail register specifiers
# (roughtly corresponding to l-expressions in Sail, i.e. subscripting
# R[n] and field accesses R.field are allowed.)
[registers.renames]
[reads]
[writes]
[cache_ops]
# target/release/isla-testgen -a c86 -T 1 -C ../../x86.toml -A ../sail-cheri-x86/x86.ir
#--max-retries 20
#-L fdiv_int
#-L bool_to_bits
#-L bits_to_bool
#-L bit_to_bool
#-L isEven -L signed_byte_p_int -L zf_spec -L b_xor -L logand_int -L not_bit -L floor2 -L encCapabilityToCapability -L capToEncCap -L getCapBoundsBits
# --debug fmlp
#--test-file
#--sparse
#--code-region 0x10000-0x10fff
#--memory-region 0x11000-0x11fff
#--acl2-insts ../../inst.sexp _
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment