Open mmcloughlin opened 9 months ago
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}"
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.
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.
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.
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.
I have built IR from the latest armv9.4 model, but the configs do not appear to work.
For example:
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!