From 61bd6c27c94fbca125d66b8a3e57a90613c36ee1 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 22 Dec 2025 04:40:42 -0800 Subject: [PATCH] SMV: allow any expression in SMV types This extends the grammar to allow any expressions as the size of arrays and as the width of word types. This matches the NuSMV manual. The type checker enforces that these are constants. --- regression/smv/word/invalid_width1.desc | 8 ++++ regression/smv/word/invalid_width1.smv | 6 +++ src/smvlang/parser.y | 8 ++-- src/smvlang/smv_typecheck.cpp | 50 +++++++++++++++++++------ 4 files changed, 56 insertions(+), 16 deletions(-) create mode 100644 regression/smv/word/invalid_width1.desc create mode 100644 regression/smv/word/invalid_width1.smv diff --git a/regression/smv/word/invalid_width1.desc b/regression/smv/word/invalid_width1.desc new file mode 100644 index 000000000..eda2fa274 --- /dev/null +++ b/regression/smv/word/invalid_width1.desc @@ -0,0 +1,8 @@ +CORE +invalid_width1.smv + +^file .* line 6: expected constant expression$ +^EXIT=2$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/smv/word/invalid_width1.smv b/regression/smv/word/invalid_width1.smv new file mode 100644 index 000000000..761e52146 --- /dev/null +++ b/regression/smv/word/invalid_width1.smv @@ -0,0 +1,6 @@ +MODULE main + +VAR width : 1..10; + +-- The width must be constant +VAR word_var : word[width]; diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y index d71ea3c96..8f703d479 100644 --- a/src/smvlang/parser.y +++ b/src/smvlang/parser.y @@ -556,7 +556,7 @@ type_specifier: ; simple_type_specifier: - array_Token integer_constant DOTDOT_Token integer_constant of_Token simple_type_specifier + array_Token basic_expr DOTDOT_Token basic_expr of_Token simple_type_specifier { init($$, ID_smv_array); stack_type($$).set(ID_from, stack_expr($2)); @@ -564,17 +564,17 @@ simple_type_specifier: stack_type($$).add_subtype()=stack_type($6); } | boolean_Token { init($$, ID_bool); } - | word_Token '[' integer_constant ']' + | word_Token '[' basic_expr ']' { init($$, ID_smv_word); stack_type($$).set(ID_width, stack_expr($3)); } - | signed_Token word_Token '[' integer_constant ']' + | signed_Token word_Token '[' basic_expr ']' { init($$, ID_smv_signed_word); stack_type($$).set(ID_width, stack_expr($4)); } - | unsigned_Token word_Token '[' integer_constant ']' + | unsigned_Token word_Token '[' basic_expr ']' { init($$, ID_smv_unsigned_word); stack_type($$).set(ID_width, stack_expr($4)); diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index e80f10e30..2a072304c 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -144,6 +144,8 @@ class smv_typecheckt:public typecheckt return id; } + mp_integer require_integer_constant(const irept &) const; + void lower_node(exprt &) const; void lower(typet &) const; @@ -363,6 +365,36 @@ void smv_typecheckt::instantiate( /*******************************************************************\ +Function: smv_typecheckt::require_integer_constant + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +mp_integer smv_typecheckt::require_integer_constant(const irept &irep) const +{ + auto &as_expr = static_cast(irep); + if(as_expr.id() != ID_constant) + { + throw errort().with_location(as_expr.source_location()) + << "expected constant expression"; + } + + if(as_expr.type().id() != ID_integer) + { + throw errort().with_location(as_expr.source_location()) + << "expected integer expression"; + } + + return numeric_cast_v(to_constant_expr(as_expr)); +} + +/*******************************************************************\ + Function: smv_typecheckt::check_type Inputs: @@ -377,10 +409,8 @@ void smv_typecheckt::check_type(typet &type) { if(type.id() == ID_smv_array) { - auto from = numeric_cast_v( - to_constant_expr(static_cast(type.find(ID_from)))); - auto to = numeric_cast_v( - to_constant_expr(static_cast(type.find(ID_to)))); + auto from = require_integer_constant(type.find(ID_from)); + auto to = require_integer_constant(type.find(ID_to)); if(to < from) throw errort().with_location(type.source_location()) @@ -402,10 +432,8 @@ void smv_typecheckt::check_type(typet &type) } else if(type.id() == ID_smv_range) { - auto from = numeric_cast_v( - to_constant_expr(static_cast(type.find(ID_from)))); - auto to = numeric_cast_v( - to_constant_expr(static_cast(type.find(ID_to)))); + auto from = require_integer_constant(type.find(ID_from)); + auto to = require_integer_constant(type.find(ID_to)); if(from > to) throw errort().with_location(type.source_location()) << "range is empty"; @@ -416,8 +444,7 @@ void smv_typecheckt::check_type(typet &type) } else if(type.id() == ID_smv_signed_word) { - auto width = numeric_cast_v( - to_constant_expr(static_cast(type.find(ID_width)))); + auto width = require_integer_constant(type.find(ID_width)); if(width < 1) throw errort().with_location(type.source_location()) @@ -428,8 +455,7 @@ void smv_typecheckt::check_type(typet &type) } else if(type.id() == ID_smv_word || type.id() == ID_smv_unsigned_word) { - auto width = numeric_cast_v( - to_constant_expr(static_cast(type.find(ID_width)))); + auto width = require_integer_constant(type.find(ID_width)); if(width < 1) throw errort().with_location(type.source_location())