Skip to content

Commit

Permalink
verifier: enum support (avanhatt#81)
Browse files Browse the repository at this point in the history 
Implement support for complex enum types in the verifier.

Features of this limited support:

* Enum types cannot be directly declared by users. A verification domain
  enum can only be derived from its corresponding ISLE definition.
* Enum variants can be constructed: `(Enum.Variant a b c)`
* Discriminator expressions: `(Variant? e)` tests if `e` has variant
  `Variant`.
* Enums can be compared for equality.

Updates avanhatt#48
  • Loading branch information
@mmcloughlin
mmcloughlin authored Sep 28, 2024
1 parent 898f3c1 commit c2483ed
Show file tree
Hide file tree
Showing 12 changed files with 557 additions and 226 deletions.
40 changes: 1 addition & 39 deletions cranelift/codegen/src/isa/aarch64/inst.isle
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1243,30 +1243,6 @@
(SbcS)
))

(model ALUOp
(enum (bv 8)
(Add #x00)
(Sub #x01)
(Orr #x02)
(OrrNot #x03)
(And #x04)
(AndNot #x05)
(Eor #x06)
(EorNot #x07)
(AddS #x08)
(SubS #x09)
(SMulH #x0a)
(UMulH #x0b)
(SDiv #x0c)
(UDiv #x0d)
(RotR #x0e)
(Lsr #x0f)
(Asr #x10)
(Lsl #x11)
(Adc #x12)
)
)

;; An ALU operation with three arguments.
(type ALUOp3
(enum
Expand All @@ -1280,15 +1256,6 @@
(SMAddL)
))

(model ALUOp3
(enum (bv 8)
(MAdd #x00)
(MSub #x01)
(UMAddL #x02)
(SMAddL #x03)
)
)

(type MoveWideOp
(enum
(MovZ)
Expand Down Expand Up @@ -1495,18 +1462,13 @@
(enum Size32
Size64))

(model OperandSize
(enum Int
(Size32 32)
(Size64 64)))

(type TestBitAndBranchKind (enum (Z) (NZ)))

;; Helper for calculating the `OperandSize` corresponding to a type
(decl operand_size (Type) OperandSize)
(spec (operand_size ty)
(provide
(= result (if (<= ty 32) 32 64)))
(= result (if (<= ty 32) (OperandSize.Size32) (OperandSize.Size64))))
(require
(or (= ty 8) (= ty 16) (= ty 32) (= ty 64))))
(rule 1 (operand_size (fits_in_32 _ty)) (OperandSize.Size32))
Expand Down
21 changes: 1 addition & 20 deletions cranelift/codegen/src/isa/x64/inst.isle
View file
Original file line number Diff line number Diff line change
Expand Up @@ -781,13 +781,6 @@
Size32
Size64))

(model OperandSize
(enum Int
(Size8 8)
(Size16 16)
(Size32 32)
(Size64 64)))

(type DivSignedness
(enum Signed
Unsigned))
Expand All @@ -804,7 +797,7 @@
(decl operand_size_of_type_32_64 (Type) OperandSize)
(spec (operand_size_of_type_32_64 ty)
(provide
(= result (if (= ty 64) 64 32))
(= result (if (= ty 64) (OperandSize.Size64) (OperandSize.Size32)))
)
)
(extern constructor operand_size_of_type_32_64 operand_size_of_type_32_64)
Expand All @@ -829,18 +822,6 @@
Or
Xor))

(model AluRmiROpcode
(enum (bv 8)
(Add #x00)
(Adc #x01)
(Sub #x02)
(Sbb #x03)
(And #x04)
(Or #x05)
(Xor #x06)
)
)

(type AluRmROpcode
(enum Andn
Sarx
Expand Down
13 changes: 10 additions & 3 deletions cranelift/isle/isle/src/ast.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -145,6 +145,12 @@ pub enum SpecExpr {
x: Box<SpecExpr>,
pos: Pos,
},
/// Discriminator is a predicate that tests the variant of an enum value.
Discriminator {
variant: Ident,
x: Box<SpecExpr>,
pos: Pos,
},
/// An application of a type variant or term.
Op {
op: SpecOp,
Expand All @@ -169,9 +175,11 @@ pub enum SpecExpr {
r: Box<SpecExpr>,
pos: Pos,
},
/// Enums variant values (enums defined by model)
/// Construct enum variant.
Enum {
name: Ident,
variant: Ident,
args: Vec<SpecExpr>,
pos: Pos,
},
}
Expand All @@ -184,6 +192,7 @@ impl SpecExpr {
| &Self::ConstBool { pos, .. }
| &Self::Var { pos, .. }
| &Self::Field { pos, .. }
| &Self::Discriminator { pos, .. }
| &Self::Op { pos, .. }
| &Self::Let { pos, .. }
| &Self::With { pos, .. }
Expand Down Expand Up @@ -309,8 +318,6 @@ pub struct ModelField {
pub enum ModelValue {
/// Correspond to ISLE types
TypeValue(ModelType),
/// Correspond to ISLE enums, identifier is the enum variant name
EnumValues(ModelType, Vec<(Ident, SpecExpr)>),
/// Corresponds to ISLE external constants.
ConstValue(SpecExpr),
}
Expand Down
66 changes: 17 additions & 49 deletions cranelift/isle/isle/src/parser.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -504,7 +504,12 @@ impl<'a> Parser<'a> {
} else if self.is_sym() && !self.is_spec_bit_vector() {
let sym_pos = self.pos();
let sym = self.expect_symbol()?;
if let Ok(op) = self.parse_spec_op(sym.as_str()) {
if let Some(variant) = sym.strip_suffix('?') {
let variant = self.str_to_ident(sym_pos, variant)?;
let x = Box::new(self.parse_spec_expr()?);
self.expect_rparen()?;
Ok(SpecExpr::Discriminator { variant, x, pos })
} else if let Ok(op) = self.parse_spec_op(sym.as_str()) {
let mut args: Vec<SpecExpr> = vec![];
while !self.is_rparen() {
args.push(self.parse_spec_expr()?);
Expand All @@ -516,10 +521,18 @@ impl<'a> Parser<'a> {
let x = Box::new(self.parse_spec_expr()?);
self.expect_rparen()?;
Ok(SpecExpr::Field { field, x, pos })
} else {
let name = self.str_to_ident(pos, &sym)?;
} else if let Some((name, variant)) = sym.split_once('.') {
let name = self.str_to_ident(pos, &name)?;
let variant = self.str_to_ident(pos, &variant)?;
self.expect_rparen()?;
Ok(SpecExpr::Enum { name, pos })
Ok(SpecExpr::Enum {
name,
variant,
args: Vec::new(),
pos,
})
} else {
Err(self.error(pos, "Unexpected spec expression".into()))
}
} else {
// TODO(mbm): support Unit
Expand Down Expand Up @@ -626,51 +639,6 @@ impl<'a> Parser<'a> {
let val = if self.eat_sym_str("type")? {
let ty = self.parse_model_type()?;
ModelValue::TypeValue(ty)
} else if self.eat_sym_str("enum")? {
let ty = self.parse_model_type()?;

let mut variants = vec![];
let mut has_explicit_value = false;
let mut implicit_idx = None;

while !self.is_rparen() {
self.expect_lparen()?; // enum value
let name = self.parse_ident()?;
let val = if self.is_rparen() {
// has implicit enum value
if has_explicit_value {
return Err(self.error(
pos,
format!(
"Spec enum has unexpected implicit value after implicit value."
),
));
}
implicit_idx = Some(if let Some(idx) = implicit_idx {
idx + 1
} else {
0
});
SpecExpr::ConstInt {
val: implicit_idx.unwrap(),
pos,
}
} else {
if implicit_idx.is_some() {
return Err(self.error(
pos,
format!(
"Spec enum has unexpected explicit value after implicit value."
),
));
}
has_explicit_value = true;
self.parse_spec_expr()?
};
self.expect_rparen()?;
variants.push((name, val));
}
ModelValue::EnumValues(ty, variants)
} else if self.eat_sym_str("const")? {
let val = self.parse_spec_expr()?;
ModelValue::ConstValue(val)
Expand Down
23 changes: 13 additions & 10 deletions cranelift/isle/isle/src/printer.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -182,15 +182,6 @@ impl Printable for ModelValue {
fn to_doc(&self) -> RcDoc<()> {
match self {
ModelValue::TypeValue(ref mt) => sexp(vec![RcDoc::text("type"), mt.to_doc()]),
ModelValue::EnumValues(ref ty, ref values) => sexp(
Vec::from([RcDoc::text("enum"), ty.to_doc()])
.into_iter()
.chain(
values
.iter()
.map(|(name, expr)| sexp(vec![name.to_doc(), expr.to_doc()])),
),
),
v => todo!("model value: {v:?}"),
}
}
Expand Down Expand Up @@ -250,10 +241,22 @@ impl Printable for SpecExpr {
.chain(args.iter().map(|a| a.to_doc())),
),
SpecExpr::Pair { l, r, .. } => sexp(vec![l.to_doc(), r.to_doc()]),
SpecExpr::Enum { name, .. } => sexp(vec![name.to_doc()]),
SpecExpr::Enum {
name,
variant,
args,
pos: _,
} => sexp(
Vec::from([RcDoc::text(format!("{}.{}", name.0, variant.0))])
.into_iter()
.chain(args.iter().map(|a| a.to_doc())),
),
SpecExpr::Field { field, x, pos: _ } => {
sexp(vec![RcDoc::text(format!(":{}", field.0)), x.to_doc()])
}
SpecExpr::Discriminator { variant, x, pos: _ } => {
sexp(vec![RcDoc::text(format!("{}?", variant.0)), x.to_doc()])
}
SpecExpr::Let { defs, body, pos: _ } => sexp(vec![
RcDoc::text("let"),
sexp(defs.iter().map(|(n, e)| sexp(vec![n.to_doc(), e.to_doc()]))),
Expand Down
14 changes: 7 additions & 7 deletions cranelift/isle/veri/isaspec/src/bin/isaspec.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ use cranelift_isle::printer;
use cranelift_isle_veri_aslp::client::Client;
use cranelift_isle_veri_isaspec::aarch64::pstate_field;
use cranelift_isle_veri_isaspec::spec::{
spec_const_int, spec_enum, spec_eq, spec_eq_bool, spec_field, spec_var,
spec_const_int, spec_enum_unit, spec_eq, spec_eq_bool, spec_field, spec_var,
};
use itertools::Itertools;

Expand Down Expand Up @@ -169,11 +169,11 @@ fn define() -> Vec<FileConfig> {
require: vec![
spec_eq(
spec_var("alu_op".to_string()),
spec_enum("ALUOp".to_string(), format!("{alu_op:?}")),
spec_enum_unit("ALUOp".to_string(), format!("{alu_op:?}")),
),
spec_eq(
spec_var("size".to_string()),
spec_enum("OperandSize".to_string(), format!("{size:?}")),
spec_enum_unit("OperandSize".to_string(), format!("{size:?}")),
),
],

Expand Down Expand Up @@ -231,11 +231,11 @@ fn define() -> Vec<FileConfig> {
require: vec![
spec_eq(
spec_var("alu_op".to_string()),
spec_enum("ALUOp3".to_string(), format!("{alu_op:?}")),
spec_enum_unit("ALUOp3".to_string(), format!("{alu_op:?}")),
),
spec_eq(
spec_var("size".to_string()),
spec_enum("OperandSize".to_string(), format!("{size:?}")),
spec_enum_unit("OperandSize".to_string(), format!("{size:?}")),
),
],

Expand Down Expand Up @@ -288,11 +288,11 @@ fn define() -> Vec<FileConfig> {
require: vec![
spec_eq(
spec_var("op".to_string()),
spec_enum("BitOp".to_string(), format!("{op:?}")),
spec_enum_unit("BitOp".to_string(), format!("{op:?}")),
),
spec_eq(
spec_var("size".to_string()),
spec_enum("OperandSize".to_string(), format!("{size:?}")),
spec_enum_unit("OperandSize".to_string(), format!("{size:?}")),
),
],

Expand Down
26 changes: 22 additions & 4 deletions cranelift/isle/veri/isaspec/src/builder.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -209,10 +209,9 @@ fn substitute(
}

// Constants are unchanged.
SpecExpr::ConstInt { .. }
| SpecExpr::ConstBitVec { .. }
| SpecExpr::ConstBool { .. }
| SpecExpr::Enum { .. } => expr,
SpecExpr::ConstInt { .. } | SpecExpr::ConstBitVec { .. } | SpecExpr::ConstBool { .. } => {
expr
}

// Scopes require care to ensure we are not replacing introduced variables.
SpecExpr::Let { defs, body, pos } => SpecExpr::Let {
Expand Down Expand Up @@ -247,6 +246,11 @@ fn substitute(
x: Box::new(substitute(*x, substitutions)?),
pos,
},
SpecExpr::Discriminator { variant, x, pos } => SpecExpr::Discriminator {
variant,
x: Box::new(substitute(*x, substitutions)?),
pos,
},
SpecExpr::Op { op, args, pos } => SpecExpr::Op {
op,
args: args
Expand All @@ -260,5 +264,19 @@ fn substitute(
r: Box::new(substitute(*r, substitutions)?),
pos,
},
SpecExpr::Enum {
name,
variant,
args,
pos,
} => SpecExpr::Enum {
name,
variant,
args: args
.into_iter()
.map(|arg| substitute(arg, substitutions))
.collect::<anyhow::Result<_>>()?,
pos,
},
})
}
10 changes: 8 additions & 2 deletions cranelift/isle/veri/isaspec/src/spec.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -84,13 +84,19 @@ pub fn spec_op(op: SpecOp, args: Vec<SpecExpr>) -> SpecExpr {
}
}

pub fn spec_enum(name: String, variant: String) -> SpecExpr {
pub fn spec_enum(name: String, variant: String, args: Vec<SpecExpr>) -> SpecExpr {
SpecExpr::Enum {
name: spec_ident(format!("{}.{}", name, variant)),
name: spec_ident(name),
variant: spec_ident(variant),
args,
pos: Pos::default(),
}
}

pub fn spec_enum_unit(name: String, variant: String) -> SpecExpr {
spec_enum(name, variant, Vec::new())
}

pub fn spec_field(field: String, x: SpecExpr) -> SpecExpr {
SpecExpr::Field {
field: spec_ident(field),
Expand Down
Loading

0 comments on commit c2483ed

Please sign in to comment.