armv9.4 config

[mmcloughlin]

I have built IR from the latest armv9.4 model, but the configs do not appear to work.

For example:

$ ./target/debug/isla-footprint --arch /tmp/tmp.s5sMpblynE/outputs/armv9.ir --config configs/armv9.toml --instruction 'ldrb w1, [x2]'
Warning: Could not find register CFG_ID_AA64PFR0_EL1_MPAM when parsing registers.defaults in configuration
Warning: Could not find register __aa32_hpd_implemented when parsing registers.defaults in configuration
Warning: Could not find register __brbe_implemented when parsing registers.defaults in configuration
Warning: Could not find register __brbev1p1_implemented when parsing registers.defaults in configuration
Warning: Could not find register __crc32_implemented when parsing registers.defaults in configuration
Warning: Could not find register __crypto_aes_implemented when parsing registers.defaults in configuration
Warning: Could not find register __crypto_sha1_implemented when parsing registers.defaults in configuration
Warning: Could not find register __crypto_sha256_implemented when parsing registers.defaults in configuration
Warning: Could not find register __crypto_sha3_implemented when parsing registers.defaults in configuration
Warning: Could not find register __crypto_sha512_implemented when parsing registers.defaults in configuration
Warning: Could not find register __crypto_sm3_implemented when parsing registers.defaults in configuration
Warning: Could not find register __crypto_sm4_implemented when parsing registers.defaults in configuration
Warning: Could not find register __dot_product_implemented when parsing registers.defaults in configuration
Warning: Could not find register __empam_implemented when parsing registers.defaults in configuration
Warning: Could not find register __feat_ls64_accdata when parsing registers.defaults in configuration
Warning: Could not find register __feat_ls64_v when parsing registers.defaults in configuration
Warning: Could not find register __fp16_implemented when parsing registers.defaults in configuration
Warning: Could not find register __has_sme when parsing registers.defaults in configuration
Warning: Could not find register __mpam_implemented when parsing registers.defaults in configuration
Warning: Could not find register __pac_frac_implemented when parsing registers.defaults in configuration
Warning: Could not find register __pacqarma3_implemented when parsing registers.defaults in configuration
Warning: Could not find register __pan_implemented when parsing registers.defaults in configuration
Warning: Could not find register __rme_implemented when parsing registers.defaults in configuration
Warning: Could not find register __v81_implemented when parsing registers.defaults in configuration
Warning: Could not find register __v82_implemented when parsing registers.defaults in configuration
Warning: Could not find register __v83_implemented when parsing registers.defaults in configuration
Warning: Could not find register __v84_implemented when parsing registers.defaults in configuration
Warning: Could not find register __v85_implemented when parsing registers.defaults in configuration
Warning: Could not find register __vmid16_implemented when parsing registers.defaults in configuration
configs/armv9.toml: Could not find register "__v81_implemented" when parsing registers.ignore in configuration

I did try removing all these registers from the configuration, but that just ended up giving me another error, I think related to a type mismatch for HCL_EL2.

Please could you advise me on the correct configuration to use the latest ARM model. Thanks!

[mmcloughlin]

I created my armv9.ir with:

#!/usr/bin/env bash

set -euxo pipefail

OCAML_COMPILER_VERSION="4.14.1"
ISLA_VERSION="4134411c0f463807edd788f67b3db34c1899d9b6"
SAIL_VERSION="eb8af69724828181bf0e91f1728399fe8a81e6f0"
SAIL_ARM_VERSION="f7dedcf3564df71ef065e56b28ff8c9689272596"
SAIL_X86_VERSION="bfc016d354d902bf78f1e2e4a28cc82dd6d5cbfe"

# Options.
function usage() {
    echo "Usage: ${0} [-a] [-x]"
    exit 2
}

archs=()
while getopts "ax" opt; do
    case "${opt}" in
        a) archs+=("arm94") ;;
        x) archs+=("x86") ;;
        *) usage ;;
    esac
done

if [[ ${#archs[@]} -eq 0 ]]; then
    echo "no architectures configured"
    exit 2
fi

# Working directory.
workdir=$(mktemp -d)
cd "${workdir}"

outputs="${workdir}/outputs"
mkdir -p "${outputs}"

# Download dependencies.
function github_download() {
    local org="$1"
    local repo="$2"
    local version="$3"

    archive="https://github.com/${org}/${repo}/archive/${version}.tar.gz"
    mkdir -p "${repo}"
    wget -O- "${archive}" | tar xzf - --strip-components 1 -C "${repo}"
}

github_download "rems-project" "isla" "${ISLA_VERSION}"
github_download "rems-project" "sail" "${SAIL_VERSION}"
github_download "rems-project" "sail-arm" "${SAIL_ARM_VERSION}"
github_download "rems-project" "sail-x86-from-acl2" "${SAIL_X86_VERSION}"

# Setup opam.
export OPAMROOT="${workdir}/opam"
mkdir -p "${OPAMROOT}"
opam init --yes --compiler="${OCAML_COMPILER_VERSION}"
eval $(opam env)

opam repo add rems 'https://github.com/rems-project/opam-repository.git'

# Pin and install sail.
opam pin --yes add sail

# Build isla-sail.
ISLA_SAIL_PATH=$(realpath isla/isla-sail)
make -C "${ISLA_SAIL_PATH}" all
export PATH="${ISLA_SAIL_PATH}:${PATH}"

# Build architecture IRs.
function build_arm94() {
    make -C sail-arm/arm-v9.4-a ir/armv9.ir
    cp sail-arm/arm-v9.4-a/ir/armv9.ir "${outputs}/"
}

function build_x86() {
    make -C sail-x86-from-acl2/model x86.ir
    cp sail-x86-from-acl2/model/x86.ir "${outputs}/"
}

for arch in "${archs[@]}"; do
    "build_${arch}"
done

# Show outputs.
tree "${outputs}"

[bacam]

I've added a sample toml file to the sail-arm repository. It's pretty similar to the previous ones, but some of the feature registers have been renamed because Arm have been tidying things up a little.

As an example that includes several of the recent features we've been playing with, here's a command I was playing with to produce traces for a load:

~/local/rems/github/isla/target/release/isla-footprint -A ir/armv9.ir -C ir/armv9.toml -f isla_footprint_no_init -L AddWithCarry -i 'ldrb w0, [x1]' --verbose --debug fp -t -s --simplify-registers  -R PSTATE.EL=0b00 --abstract SPEBranch  --abstract BRBEBranch --fun-assumption 'AArch64_GenerateDebugExceptions((_ unit)) => false' --fun-assumption 'HaltOnBreakpointOrWatchpoint((_ unit)) => false' --probe AArch64_GenerateDebugExceptions --abstract GenMPAMatEL -R PSTATE.nRW=0b0 -I FEAT_MTE_IMPLEMENTED=false -I FEAT_MTE2_IMPLEMENTED=false -I FEAT_MTE3_IMPLEMENTED=false -I FEAT_MTE4_IMPLEMENTED=false --reset-constraint '= ((_ extract 0 0) SCTLR_EL1.bits) 0b0' --reset-constraint '= ((_ extract 0 0) HCR_EL2.bits) 0b0' --reset-constraint '= ((_ extract 12 12) HCR_EL2.bits) 0b0'  --abstract AArch64_S2DecodeTG0  -I FEAT_D128_IMPLEMENTED=false -I FEAT_HAFDBS_IMPLEMENTED=false -I FEAT_LPA2_IMPLEMENTED=false -I FEAT_CMOW_IMPLEMENTED=false -I FEAT_S2PIE_IMPLEMENTED=false -I FEAT_HAFT_IMPLEMENTED=false --fun-assumption 'Halted((_ unit)) => false' --stop-at AArch64_TakeException

Many of the fancy features here like --abstract and --fun-assumption could be replaced by giving a more concrete initial state.

[Alasdair]

We should probably rename the config files here armv8p5.toml, armv9p3.toml, and armv9p4.toml so it's clear which version of the spec each refers to.

[Alasdair]

Looking at the traces for an add instruction I seem to get a bunch of:

  (write-reg |FeatureImpl| nil (_ vec true false false false true true true true true true true true true true true true true true true false true true true true true true true true true true true true true true true true true false true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true false true true true v335 v336 v337 v338 v339 v340 v341 v342 v343 v344 v345 v346 v347 v348 v349 v350 v351 v352 v353 v354 v355 v356 v357 v358 v359 v360 v361 v362 v363 v364 v365 v366 v367 v368 v369 v370 v371 v372 v373 v374 v375 v376 v377 v378 v379 v380 v381 v382 v383 v384 v385 v386 v387 v388 v389 v390 v391 v392 v393 v394 v395 v396 v397 v398 v399 v400 v401 v402 v403 v404 v405 v406 v407 v408 v409 v410 v411 v412 v413 v414 v415 v416 v417 v418 v419 v420 v421 v422 v423 v424 v425 v426 v427 v428 v429 v430 v431 v432 v433 v434 v435 v436 v437 v438 v439 v440 v441 v442 v443 v444 v445 v446 v447 v448 v449 v450 v451 v452 v453 v454 v455 v456 v457 v458 v459 v460 v461 v462 v463 v464 v465 v466 v467 v468 v469 v470 v471 v472 v473 v474 v475 v476 v477 v478 v479 v480 v481 v482 v483 v484 v485 v486 v487 v488 v489 v490 v491 v492 v493 v494 v495 v496 v497 v498 v499 v500 v501 v502 v503 v504 v505 v506 v507 v508 v509 v510 v511 v512 v513 v514 v515 v516 v517))

Not sure if there's a good way to simplify that away.

Running without --function isla_footprint_no_init also seems to get a bit stuck setting up the vector registers as I think there's a if ConstrainedUnpredictable(...) which is giving it some issues.

[mmcloughlin]

Thanks for this! Just confirming this does work for me too. I can get a trace for an add instruction with:

> target/release/isla-footprint -A ../isla-snapshots/armv9p4.ir -C configs/armv9p4.toml -f isla_footprint_no_init -L AddWithCarry -i "add x0, x1, #3" -s --simplify-registers
No primop emulator_read_tag (Name { id: 2624 })
No primop emulator_write_tag (Name { id: 2625 })
(trace
  (assume-reg |__isla_vector_gpr| nil false)
  (assume-reg |CNTCR| nil (_ struct (|bits| #x00000001)))
  (define-enum |Feature| 258 (|FEAT_AA32EL0| |FEAT_AA32EL1| |FEAT_AA32EL2| |FEAT_AA32EL3| |FEAT_AA64EL0| |FEAT_AA64EL1| |FEAT_AA64EL2| |FEAT_AA64EL3| |FEAT_EL0| |FEAT_EL1| |FEAT_EL2| |FEAT_EL3| |FEAT_AES| |FEAT_AdvSIMD| |FEAT_CSV2_1p1| |FEAT_CSV2_1p2| |FEAT_CSV2_2| |FEAT_CSV2_3| |FEAT_DoubleLock| |FEAT_ETMv4| |FEAT_ETMv4p1| |FEAT_ETMv4p2| |FEAT_ETMv4p3| |FEAT_ETMv4p4| |FEAT_ETMv4p5| |FEAT_ETMv4p6| |FEAT_ETS2| |FEAT_FP| |FEAT_GICv3| |FEAT_GICv3_LEGACY| |FEAT_GICv3_TDIR| |FEAT_GICv3p1| |FEAT_GICv4| |FEAT_GICv4p1| |FEAT_IVIPT| |FEAT_PCSRv8| |FEAT_PMULL| |FEAT_PMUv3| |FEAT_PMUv3_EXT| |FEAT_PMUv3_EXT32| |FEAT_SHA1| |FEAT_SHA256| |FEAT_TRC_EXT| |FEAT_TRC_SR| |FEAT_nTLBPA| |FEAT_CRC32| |FEAT_Debugv8p1| |FEAT_HAFDBS| |FEAT_HPDS| |FEAT_LOR| |FEAT_LSE| |FEAT_PAN| |FEAT_PMUv3p1| |FEAT_RDM| |FEAT_VHE| |FEAT_VMID16| |FEAT_AA32BF16| |FEAT_AA32HPD| |FEAT_AA32I8MM| |FEAT_ASMv8p2| |FEAT_DPB| |FEAT_Debugv8p2| |FEAT_EDHSR| |FEAT_F32MM| |FEAT_F64MM| |FEAT_FP16| |FEAT_HPDS2| |FEAT_I8MM| |FEAT_IESB| |FEAT_LPA| |FEAT_LSMAOC| |FEAT_LVA| |FEAT_MPAM| |FEAT_PAN2| |FEAT_PCSRv8p2| |FEAT_RAS| |FEAT_SHA3| |FEAT_SHA512| |FEAT_SM3| |FEAT_SM4| |FEAT_SPE| |FEAT_SVE| |FEAT_TTCNP| |FEAT_UAO| |FEAT_VPIPT| |FEAT_XNX| |FEAT_CCIDX| |FEAT_CONSTPACFIELD| |FEAT_EPAC| |FEAT_FCMA| |FEAT_FPAC| |FEAT_FPACCOMBINE| |FEAT_JSCVT| |FEAT_LRCPC| |FEAT_NV| |FEAT_PACIMP| |FEAT_PACQARMA3| |FEAT_PACQARMA5| |FEAT_PAuth| |FEAT_SPEv1p1| |FEAT_AMUv1| |FEAT_BBM| |FEAT_CNTSC| |FEAT_DIT| |FEAT_Debugv8p4| |FEAT_DotProd| |FEAT_DoubleFault| |FEAT_FHM| |FEAT_FlagM| |FEAT_IDST| |FEAT_LRCPC2| |FEAT_LSE2| |FEAT_NV2| |FEAT_PMUv3p4| |FEAT_RASSAv1p1| |FEAT_RASv1p1| |FEAT_S2FWB| |FEAT_SEL2| |FEAT_TLBIOS| |FEAT_TLBIRANGE| |FEAT_TRF| |FEAT_TTL| |FEAT_TTST| |FEAT_BTI| |FEAT_CSV2| |FEAT_CSV3| |FEAT_DPB2| |FEAT_E0PD| |FEAT_EVT| |FEAT_ExS| |FEAT_FRINTTS| |FEAT_FlagM2| |FEAT_GTG| |FEAT_MTE| |FEAT_MTE2| |FEAT_PMUv3p5| |FEAT_RNG| |FEAT_RNG_TRAP| |FEAT_SB| |FEAT_SPECRES| |FEAT_SSBS| |FEAT_SSBS2| |FEAT_AMUv1p1| |FEAT_BF16| |FEAT_DGH| |FEAT_ECV| |FEAT_FGT| |FEAT_HPMN0| |FEAT_MPAMv0p1| |FEAT_MPAMv1p1| |FEAT_MTPMU| |FEAT_PAuth2| |FEAT_TWED| |FEAT_AFP| |FEAT_EBF16| |FEAT_HCX| |FEAT_LPA2| |FEAT_LS64| |FEAT_LS64_ACCDATA| |FEAT_LS64_V| |FEAT_MTE3| |FEAT_PAN3| |FEAT_PMUv3p7| |FEAT_RPRES| |FEAT_SPEv1p2| |FEAT_WFxT| |FEAT_XS| |FEAT_CMOW| |FEAT_Debugv8p8| |FEAT_GICv3_NMI| |FEAT_HBC| |FEAT_MOPS| |FEAT_NMI| |FEAT_PMUv3_EXT64| |FEAT_PMUv3_TH| |FEAT_PMUv3p8| |FEAT_SCTLR2| |FEAT_SPEv1p3| |FEAT_TCR2| |FEAT_TIDCP1| |FEAT_ADERR| |FEAT_AIE| |FEAT_ANERR| |FEAT_CLRBHB| |FEAT_CSSC| |FEAT_Debugv8p9| |FEAT_DoubleFault2| |FEAT_ECBHB| |FEAT_FGT2| |FEAT_HAFT| |FEAT_LRCPC3| |FEAT_MTE4| |FEAT_MTE_ASYM_FAULT| |FEAT_MTE_ASYNC| |FEAT_MTE_CANONICAL_TAGS| |FEAT_MTE_NO_ADDRESS_TAGS| |FEAT_MTE_PERM| |FEAT_MTE_STORE_ONLY| |FEAT_MTE_TAGGED_FAR| |FEAT_PCSRv8p9| |FEAT_PFAR| |FEAT_PMUv3_EDGE| |FEAT_PMUv3_ICNTR| |FEAT_PMUv3_SS| |FEAT_PMUv3p9| |FEAT_PRFMSLC| |FEAT_RASSAv2| |FEAT_RASv2| |FEAT_RPRFM| |FEAT_S1PIE| |FEAT_S1POE| |FEAT_S2PIE| |FEAT_S2POE| |FEAT_SPECRES2| |FEAT_SPE_CRR| |FEAT_SPE_FDS| |FEAT_SPEv1p4| |FEAT_SPMU| |FEAT_THE| |FEAT_DoPD| |FEAT_ETE| |FEAT_SVE2| |FEAT_SVE_AES| |FEAT_SVE_BitPerm| |FEAT_SVE_PMULL128| |FEAT_SVE_SHA3| |FEAT_SVE_SM4| |FEAT_TME| |FEAT_TRBE| |FEAT_ETEv1p1| |FEAT_BRBE| |FEAT_ETEv1p2| |FEAT_RME| |FEAT_SME| |FEAT_SME_F64F64| |FEAT_SME_FA64| |FEAT_SME_I16I64| |FEAT_BRBEv1p1| |FEAT_MEC| |FEAT_SME2| |FEAT_ABLE| |FEAT_CHK| |FEAT_D128| |FEAT_EBEP| |FEAT_ETEv1p3| |FEAT_GCS| |FEAT_ITE| |FEAT_LSE128| |FEAT_LVA3| |FEAT_SEBEP| |FEAT_SME2p1| |FEAT_SME_F16F16| |FEAT_SVE2p1| |FEAT_SVE_B16B16| |FEAT_SYSINSTR128| |FEAT_SYSREG128| |FEAT_TRBE_EXT| |FEAT_TRBE_MPAM|))
  (define-enum |Signal| 2 (|Signal_Low| |Signal_High|))
  (define-enum |__InstrEnc| 4 (|__A64| |__A32| |__T16| |__T32|))
  (cycle)
  (declare-const v526 (_ BitVec 64)) ; SourceLoc { file: 29, line1: 62, char1: 16, line2: 62, char2: 25 }
  (read-reg |_PC| nil v526)
  (read-reg |SEE| nil (_ bv-1 128))
  (write-reg |SEE| nil (_ bv18 128))
  (read-reg |__isla_vector_gpr| nil false)
  (declare-const v532 (_ BitVec 64)) ; SourceLoc { file: 9, line1: 2146, char1: 13, line2: 2146, char2: 15 }
  (read-reg |R1| nil v532)
  (define-const v573 ((_ zero_extend 0) (bvadd ((_ extract 63 0) ((_ zero_extend 64) ((_ extract 63 0) v532))) #x0000000000000003)))
  (write-reg |R0| nil v573))

I also observe that --function isla_footprint_no_init is crucial, otherwise it gets stuck and later crashes.