Skip to content

sys/ppc64: Spec does uses VADL::s/umod without zero check #795

@Jozott00

Description

@Jozott00

The PPC64 specification uses the VADL::s/umod built-ins without a zero check for the divisor:

model XFormModInstr (x : AsmOpExt, type : Id) : IsaDefs = {
instruction AsId($x.asm) : XFormA =
X(rs) := VADL::$x.op(XW(ra), XW(rb)) as $type
encoding AsId($x.asm) = {opcd = 0b011111, extopcd = $x.ext, rc = 0b0}
assembly AsId($x.asm) = ($x.asm, " ", decimal(rs), ",", decimal(ra), ",", decimal(rb))
}

Because the VADL::s/umod operations are undefined for 0, this causes a crash on the x86 runners, as on x86 a division by zero causes an exception.
https://github.com/OpenVADL/openvadl/actions/runs/22714792101#summary-65861829474

The solution is to check the divisor against 0 as it is done for the division instructions

openvadl/sys/ppc64/ppc64.vadl

Lines 1240 to 1252 in d054cd1

model XOFormDivInstrExt (r : XOFormDivInstrRec, oe : Bool, rc : Bool) : IsaDefs = {
instruction AsId($r.x.asm, $orId($oe; $rc)) : XOForm =
if XW(rb) != 0
then let res, flags = VADL::$r.x.op($r.a.arg1, $r.a.arg2) in
let udf = $r.udf in
let result = if udf then $r.ures else res as Word as $r.type in {
X(rs) := result
$SetXERAndCRWithOV3264($oe; false; $rc; mov; udf | flags.overflow)
}
else let result = $r.zres as UDWord in {
X(rs) := result
$SetXERAndCRWithOV3264($oe; false; $rc; mov; true)
}

Metadata

Metadata

Assignees

Labels

VADL-specificationIssues with a specification written in VADLbugSomething isn't working

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions