Skip to content

Commit

Permalink
Disallow == or != comparisons for union variant.
Browse files Browse the repository at this point in the history
  • Loading branch information
otrho committed Sep 24, 2024
1 parent 1a25382 commit 30fea79
Show file tree
Hide file tree
Showing 9 changed files with 139 additions and 107 deletions.
22 changes: 21 additions & 1 deletion pintc/src/error/compile_error.rs
Original file line number Diff line number Diff line change
Expand Up @@ -222,6 +222,13 @@ pub enum CompileError {
arity: &'static str,
large_err: Box<LargeTypeError>,
},
#[error("operator invalid type error")]
OperatorInvalidType {
op: &'static str,
ty_kind: &'static str,
bad_ty: String,
span: Span,
},
#[error("{init_kind} initialization type error")]
InitTypeError {
init_kind: &'static str,
Expand Down Expand Up @@ -981,6 +988,17 @@ impl ReportableError for CompileError {
}
},

OperatorInvalidType {
op,
ty_kind,
bad_ty,
span,
} => vec![ErrorLabel {
message: format!("invalid {ty_kind} type `{bad_ty}` for operator `{op}`"),
span: span.clone(),
color: Color::Red,
}],

BadCastTo { ty, span } => vec![ErrorLabel {
message: format!("illegal cast to a `{ty}`"),
span: span.clone(),
Expand Down Expand Up @@ -1363,6 +1381,7 @@ impl ReportableError for CompileError {
| SelectBranchesTypeMismatch { .. }
| ConstraintExpressionTypeError { .. }
| OperatorTypeError { .. }
| OperatorInvalidType { .. }
| InitTypeError { .. }
| StateVarInitTypeError { .. }
| IndexExprNonIndexable { .. }
Expand Down Expand Up @@ -1614,7 +1633,8 @@ impl Spanned for CompileError {
| UnknownUnionVariant { span, .. }
| SuperfluousUnionExprValue { span, .. }
| MissingUnionExprValue { span, .. }
| UnionVariantTypeMismatch { span, .. } => span,
| UnionVariantTypeMismatch { span, .. }
| OperatorInvalidType { span, .. } => span,

DependencyCycle { spans } => &spans[0],

Expand Down
87 changes: 48 additions & 39 deletions pintc/src/predicate/analyse/type_check.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1963,34 +1963,26 @@ impl Contract {
rhs_expr_key: ExprKey,
span: &Span,
) -> Inference {
let check_numeric_args = |lhs_ty: &Type, rhs_ty: &Type, ty_str: &str| {
let check_numeric_args = |lhs_ty: &Type, rhs_ty: &Type| {
if !lhs_ty.is_num() {
if !lhs_ty.is_error() {
handler.emit_err(Error::Compile {
error: CompileError::OperatorTypeError {
arity: "binary",
large_err: Box::new(LargeTypeError::OperatorTypeError {
op: op.as_str(),
expected_ty: ty_str.to_string(),
found_ty: self.with_ctrct(lhs_ty).to_string(),
span: self.expr_key_to_span(lhs_expr_key),
expected_span: None,
}),
error: CompileError::OperatorInvalidType {
op: op.as_str(),
ty_kind: "non-numeric",
bad_ty: self.with_ctrct(lhs_ty).to_string(),
span: span.clone(),
},
});
}
} else if !rhs_ty.is_num() {
if !rhs_ty.is_error() {
handler.emit_err(Error::Compile {
error: CompileError::OperatorTypeError {
arity: "binary",
large_err: Box::new(LargeTypeError::OperatorTypeError {
op: op.as_str(),
expected_ty: ty_str.to_string(),
found_ty: self.with_ctrct(rhs_ty).to_string(),
span: self.expr_key_to_span(rhs_expr_key),
expected_span: None,
}),
error: CompileError::OperatorInvalidType {
op: op.as_str(),
ty_kind: "non-numeric",
bad_ty: self.with_ctrct(rhs_ty).to_string(),
span: span.clone(),
},
});
}
Expand Down Expand Up @@ -2044,7 +2036,7 @@ impl Contract {
| BinaryOp::Mod => {
// Both args must be numeric, i.e., ints or reals; binary op type is same
// as arg types.
check_numeric_args(&lhs_ty, rhs_ty, "numeric");
check_numeric_args(&lhs_ty, rhs_ty);
Inference::Type(lhs_ty)
}
BinaryOp::Equal | BinaryOp::NotEqual => {
Expand Down Expand Up @@ -2074,27 +2066,44 @@ impl Contract {
is_init_constraint = true;
}

// Both args must be equatable, which at this stage is any type; binary op
// type is bool.
if !lhs_ty.eq(&self.new_types, rhs_ty)
&& !lhs_ty.is_nil()
&& !rhs_ty.is_nil()
&& !is_init_constraint
&& !lhs_ty.is_error()
&& !rhs_ty.is_error()
{
// Both args must be equatable, which at this stage is any type *except*
// unions; binary op type is bool.
let lhs_ty_is_union = lhs_ty.is_union(&self.unions);
if lhs_ty_is_union || rhs_ty.is_union(&self.unions) {
handler.emit_err(Error::Compile {
error: CompileError::OperatorTypeError {
arity: "binary",
large_err: Box::new(LargeTypeError::OperatorTypeError {
op: op.as_str(),
expected_ty: self.with_ctrct(lhs_ty).to_string(),
found_ty: self.with_ctrct(rhs_ty).to_string(),
span: self.expr_key_to_span(rhs_expr_key),
expected_span: Some(self.expr_key_to_span(lhs_expr_key)),
}),
error: CompileError::OperatorInvalidType {
op: op.as_str(),
ty_kind: "union",
bad_ty: self
.with_ctrct(if lhs_ty_is_union { &lhs_ty } else { rhs_ty })
.to_string(),
span: span.clone(),
},
});
} else if !lhs_ty.eq(&self.new_types, rhs_ty) {
// Only emit an error if neither side is nil nor error, nor an
// initialiser constraint as per above.
if !lhs_ty.is_nil()
&& !rhs_ty.is_nil()
&& !lhs_ty.is_error()
&& !rhs_ty.is_error()
&& !is_init_constraint
{
handler.emit_err(Error::Compile {
error: CompileError::OperatorTypeError {
arity: "binary",
large_err: Box::new(LargeTypeError::OperatorTypeError {
op: op.as_str(),
expected_ty: self.with_ctrct(lhs_ty).to_string(),
found_ty: self.with_ctrct(rhs_ty).to_string(),
span: self.expr_key_to_span(rhs_expr_key),
expected_span: Some(
self.expr_key_to_span(lhs_expr_key),
),
}),
},
});
}
}

Inference::Type(Type::Primitive {
Expand All @@ -2108,7 +2117,7 @@ impl Contract {
| BinaryOp::GreaterThanOrEqual
| BinaryOp::GreaterThan => {
// Both args must be ordinal, i.e., ints, reals; binary op type is bool.
check_numeric_args(&lhs_ty, rhs_ty, "numeric");
check_numeric_args(&lhs_ty, rhs_ty);
Inference::Type(Type::Primitive {
kind: PrimitiveKind::Bool,
span: span.clone(),
Expand Down
8 changes: 4 additions & 4 deletions pintc/tests/basic_tests/bad_nil.pnt
Original file line number Diff line number Diff line change
Expand Up @@ -22,10 +22,10 @@ predicate test {
// binary operator type error
// @25..26: unexpected argument for operator `==`
// only state variables and next state expressions can be compared to `nil`
// binary operator type error
// @60..63: operator `+` argument has unexpected type `nil`
// binary operator type error
// @100..103: operator `<` argument has unexpected type `nil`
// operator invalid type error
// @56..63: invalid non-numeric type `nil` for operator `+`
// operator invalid type error
// @96..103: invalid non-numeric type `nil` for operator `<`
// variable initialization type error
// @34..37: variable initializer has unexpected type `nil`
// @28..31: expecting type `int`
Expand Down
8 changes: 4 additions & 4 deletions pintc/tests/basic_tests/if_statement_body_type_error.pnt
Original file line number Diff line number Diff line change
Expand Up @@ -67,8 +67,8 @@ predicate test {
// binary operator type error
// @185..186: operator `&&` argument has unexpected type `int`
// @174..186: expecting type `bool`
// binary operator type error
// @271..275: operator `+` argument has unexpected type `bool`
// binary operator type error
// @533..544: operator `+` argument has unexpected type `{int, bool}`
// operator invalid type error
// @267..275: invalid non-numeric type `bool` for operator `+`
// operator invalid type error
// @528..544: invalid non-numeric type `{int, bool}` for operator `+`
// >>>
8 changes: 4 additions & 4 deletions pintc/tests/interfaces/bad_address.pnt
Original file line number Diff line number Diff line change
Expand Up @@ -45,16 +45,16 @@ predicate Simple {
// >>>

// typecheck_failure <<<
// binary operator type error
// @202..206: operator `+` argument has unexpected type `bool`
// operator invalid type error
// @198..206: invalid non-numeric type `bool` for operator `+`
// address expression type error
// @198..206: address expression has unexpected type `int`
// @198..206: expecting type `b256`
// address expression type error
// @242..248: address expression has unexpected type `{int, int}`
// @242..248: expecting type `b256`
// binary operator type error
// @359..363: operator `+` argument has unexpected type `bool`
// operator invalid type error
// @355..363: invalid non-numeric type `bool` for operator `+`
// address expression type error
// @355..363: address expression has unexpected type `int`
// @355..363: expecting type `b256`
Expand Down
34 changes: 17 additions & 17 deletions pintc/tests/types/binary_ops.pnt
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ predicate test {

// parsed <<<
// enum ::T = FortyTwo | FleventyFive;
//
//
// predicate ::test {
// var ::a;
// var ::b;
Expand Down Expand Up @@ -54,28 +54,28 @@ predicate test {
// >>>

// typecheck_failure <<<
// binary operator type error
// @69..74: operator `+` argument has unexpected type `bool`
// binary operator type error
// @93..97: operator `-` argument has unexpected type `bool`
// binary operator type error
// @111..116: operator `*` argument has unexpected type `int[2]`
// binary operator type error
// @135..201: operator `/` argument has unexpected type `b256`
// binary operator type error
// @226..237: operator `%` argument has unexpected type `::T`
// operator invalid type error
// @64..74: invalid non-numeric type `bool` for operator `+`
// operator invalid type error
// @88..97: invalid non-numeric type `bool` for operator `-`
// operator invalid type error
// @111..121: invalid non-numeric type `int[2]` for operator `*`
// operator invalid type error
// @135..206: invalid non-numeric type `b256` for operator `/`
// operator invalid type error
// @221..237: invalid non-numeric type `::T` for operator `%`
// binary operator type error
// @322..337: operator `==` argument has unexpected type `::T`
// @316..318: expecting type `int`
// binary operator type error
// @357..361: operator `!=` argument has unexpected type `bool`
// @351..353: expecting type `int`
// binary operator type error
// @376..380: operator `>` argument has unexpected type `bool`
// binary operator type error
// @407..473: operator `<` argument has unexpected type `b256`
// binary operator type error
// @493..501: operator `<=` argument has unexpected type `int[2]`
// operator invalid type error
// @376..388: invalid non-numeric type `bool` for operator `>`
// operator invalid type error
// @402..473: invalid non-numeric type `b256` for operator `<`
// operator invalid type error
// @487..501: invalid non-numeric type `int[2]` for operator `<=`
// binary operator type error
// @524..526: operator `&&` argument has unexpected type `int`
// @516..526: expecting type `bool`
Expand Down
29 changes: 29 additions & 0 deletions pintc/tests/unions/bad_conditional.pnt
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
union pet = cats(int) | dogs(int) | emu;

predicate test {
var a: pet;

constraint pet::cats(11) == a;
constraint a > pet::cats(11);
constraint pet::dogs(22) <= pet::emu;
}

// parsed <<<
// union ::pet = cats(int) | dogs(int) | emu;
//
// predicate ::test {
// var ::a: ::pet;
// constraint (::pet::cats(11) == ::a);
// constraint (::a > ::pet::cats(11));
// constraint (::pet::dogs(22) <= ::pet::emu);
// }
// >>>

// typecheck_failure <<<
// operator invalid type error
// @91..109: invalid union type `::pet` for operator `==`
// operator invalid type error
// @126..143: invalid non-numeric type `::pet` for operator `>`
// operator invalid type error
// @160..185: invalid non-numeric type `::pet` for operator `<=`
// >>>
8 changes: 2 additions & 6 deletions pintc/tests/unions/no_value_union.pnt
Original file line number Diff line number Diff line change
@@ -1,15 +1,15 @@
union either = left | right;

predicate test {
var x: either = either::right;
var x: either; // DISABLED until we 'fix' initialisers. = either::right;
constraint match x {
either::left => true,
either::right => false,
};
}

predicate decl_test {
var x: either = either::right;
var x: either; // DISABLED until we 'fix' initialisers. = either::right;
match x {
either::left => {
constraint true;
Expand All @@ -25,13 +25,11 @@ predicate decl_test {
//
// predicate ::test {
// var ::x: ::either;
// constraint (::x == ::either::right);
// constraint match ::x { ::either::left => true, ::either::right => false };
// }
//
// predicate ::decl_test {
// var ::x: ::either;
// constraint (::x == ::either::right);
// match ::x {
// ::either::left => {
// constraint true
Expand All @@ -48,14 +46,12 @@ predicate decl_test {
//
// predicate ::test {
// var ::x: ::either;
// constraint (::x == ::either::right);
// constraint ((UnTag(::x) == 0) ? true : false);
// constraint __eq_set(__mut_keys(), {0});
// }
//
// predicate ::decl_test {
// var ::x: ::either;
// constraint (::x == ::either::right);
// constraint (!(UnTag(::x) == 0) || true);
// constraint ((UnTag(::x) == 0) || (!(UnTag(::x) == 1) || false));
// constraint __eq_set(__mut_keys(), {0});
Expand Down
Loading

0 comments on commit 30fea79

Please sign in to comment.