Skip to content

Commit

Permalink
SMV: removing typing from parser
Browse files Browse the repository at this point in the history 
This removes an ill-fated attempt to do typing while parsing SMV.
  • Loading branch information
@kroening
kroening committed Dec 26, 2024
1 parent f8aa6bd commit 8a54d3a
Show file tree
Hide file tree
Showing 3 changed files with 54 additions and 61 deletions.
3 changes: 1 addition & 2 deletions regression/smv/define/define1.desc
View file
Original file line number Diff line number Diff line change
@@ -1,8 +1,7 @@
KNOWNBUG
CORE broken-smt-backend
define1.smv

^EXIT=0$
^SIGNAL=0$
--
--
This yields a type error.
3 changes: 3 additions & 0 deletions regression/smv/define/define1.smv
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,7 @@ MODULE main
DEFINE a := 1;

VAR b : 1..4;
ASSIGN init(b) := 2;
ASSIGN next(b) := a + 1;

LTLSPEC G b=2
109 changes: 50 additions & 59 deletions src/smvlang/parser.y
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,49 +83,40 @@ Function: init

/// binary TODO[docu]
static void binary(YYSTYPE & x_result, YYSTYPE & y_lhs, const irep_idt &id,
YYSTYPE &z_rhs, const typet &t)
YYSTYPE &z_rhs)
{
init(x_result, id);
stack_expr(x_result).type() = t;
auto &lhs = stack_expr(y_lhs);
auto &rhs = stack_expr(z_rhs);
stack_expr(x_result).add_to_operands(std::move(lhs), std::move(rhs));
}

/// binary TODO[docu]
static void binary_arith(YYSTYPE & x_result, YYSTYPE & y_lhs,
const irep_idt &id, YYSTYPE &z_rhs)
{
init(x_result, id);
auto &lhs = stack_expr(y_lhs);
DATA_INVARIANT(lhs.type().id() != ID_nil, "arith expr without lhs type");
stack_expr(x_result).type() = lhs.type();
auto &rhs = stack_expr(z_rhs);
stack_expr(x_result).add_to_operands(std::move(lhs), std::move(rhs));
}

/*******************************************************************\
/*******************************************************************\
Function: j_binary
Function: j_binary
Inputs:
Inputs:
Outputs:
Outputs:
Purpose:
Purpose:
\*******************************************************************/
\*******************************************************************/

static void j_binary(YYSTYPE & dest, YYSTYPE & op1, const irep_idt &id,
YYSTYPE &op2, const typet &t) {
if (stack_expr(op1).id() == id) {
dest = op1;
mto(dest, op2);
} else if (stack_expr(op2).id() == id) {
dest = op2;
mto(dest, op1);
} else
binary(dest, op1, id, op2, t);
static void j_binary(YYSTYPE & dest, YYSTYPE & op1, const irep_idt &id, YYSTYPE &op2)
{
if(stack_expr(op1).id() == id)
{
dest = op1;
mto(dest, op2);
}
else if(stack_expr(op2).id() == id)
{
dest = op2;
mto(dest, op1);
}
else
binary(dest, op1, id, op2);
}

/*******************************************************************\
Expand Down Expand Up @@ -375,7 +366,7 @@ assignments: assignment

assignment : assignment_head '(' assignment_var ')' BECOMES_Token formula ';'
{
binary($$, $3, ID_equal, $6, bool_typet{});
binary($$, $3, ID_equal, $6);

if(stack_expr($1).id()==ID_smv_next)
{
Expand Down Expand Up @@ -430,7 +421,7 @@ define : assignment_var BECOMES_Token formula ';'
DATA_INVARIANT(false, "unexpected variable class");
}

binary($$, $1, ID_equal, $3, bool_typet{});
binary($$, $1, ID_equal, $3);
PARSER.module->add_define(stack_expr($$));
}
;
Expand All @@ -444,7 +435,7 @@ term : variable_name
| '{' formula_list '}' { $$=$2; stack_expr($$).id("smv_nondet_choice"); }
| INC_Token '(' term ')' { init($$, "inc"); mto($$, $3); }
| DEC_Token '(' term ')' { init($$, "dec"); mto($$, $3); }
| ADD_Token '(' term ',' term ')' { j_binary($$, $3, ID_plus, $5, stack_expr($5).type()); }
| ADD_Token '(' term ',' term ')' { j_binary($$, $3, ID_plus, $5); }
| SUB_Token '(' term ',' term ')' { init($$, ID_minus); mto($$, $3); mto($$, $5); }
| NUMBER_Token { init($$, ID_constant); stack_expr($$).set(ID_value, stack_expr($1).id()); stack_expr($$).type()=integer_typet(); }
| TRUE_Token { init($$, ID_constant); stack_expr($$).set(ID_value, ID_true); stack_expr($$).type()=typet(ID_bool); }
Expand All @@ -455,41 +446,41 @@ term : variable_name
| SWITCH_Token '(' variable_name ')' '{' switches '}' { init($$, ID_switch); mto($$, $3); mto($$, $6); }
| MINUS_Token term %prec UMINUS
{ init($$, ID_unary_minus); mto($$, $2); }
| term MOD_Token term { binary_arith($$, $1, ID_mod, $3); }
| term TIMES_Token term { binary_arith($$, $1, ID_mult, $3); }
| term DIVIDE_Token term { binary_arith($$, $1, ID_div, $3); }
| term PLUS_Token term { binary_arith($$, $1, ID_plus, $3); }
| term MINUS_Token term { binary_arith($$, $1, ID_minus, $3); }
| term EQUIV_Token term { binary($$, $1, ID_smv_iff, $3, bool_typet{}); }
| term IMPLIES_Token term { binary($$, $1, ID_implies, $3, bool_typet{}); }
| term XOR_Token term { j_binary($$, $1, ID_xor, $3, bool_typet{}); }
| term OR_Token term { j_binary($$, $1, ID_or, $3, bool_typet{}); }
| term AND_Token term { j_binary($$, $1, ID_and, $3, bool_typet{}); }
| term MOD_Token term { binary($$, $1, ID_mod, $3); }
| term TIMES_Token term { binary($$, $1, ID_mult, $3); }
| term DIVIDE_Token term { binary($$, $1, ID_div, $3); }
| term PLUS_Token term { binary($$, $1, ID_plus, $3); }
| term MINUS_Token term { binary($$, $1, ID_minus, $3); }
| term EQUIV_Token term { binary($$, $1, ID_smv_iff, $3); }
| term IMPLIES_Token term { binary($$, $1, ID_implies, $3); }
| term XOR_Token term { j_binary($$, $1, ID_xor, $3); }
| term OR_Token term { j_binary($$, $1, ID_or, $3); }
| term AND_Token term { j_binary($$, $1, ID_and, $3); }
| NOT_Token term { init($$, ID_not); mto($$, $2); }
| AX_Token term { init($$, ID_AX); mto($$, $2); }
| AF_Token term { init($$, ID_AF); mto($$, $2); }
| AG_Token term { init($$, ID_AG); mto($$, $2); }
| EX_Token term { init($$, ID_EX); mto($$, $2); }
| EF_Token term { init($$, ID_EF); mto($$, $2); }
| EG_Token term { init($$, ID_EG); mto($$, $2); }
| A_Token '[' term U_Token term ']' { binary($$, $3, ID_AU, $5, bool_typet{}); }
| A_Token '[' term R_Token term ']' { binary($$, $3, ID_AR, $5, bool_typet{}); }
| E_Token '[' term U_Token term ']' { binary($$, $3, ID_EU, $5, bool_typet{}); }
| E_Token '[' term R_Token term ']' { binary($$, $3, ID_ER, $5, bool_typet{}); }
| A_Token '[' term U_Token term ']' { binary($$, $3, ID_AU, $5); }
| A_Token '[' term R_Token term ']' { binary($$, $3, ID_AR, $5); }
| E_Token '[' term U_Token term ']' { binary($$, $3, ID_EU, $5); }
| E_Token '[' term R_Token term ']' { binary($$, $3, ID_ER, $5); }
| F_Token term { init($$, ID_F); mto($$, $2); }
| G_Token term { init($$, ID_G); mto($$, $2); }
| X_Token term { init($$, ID_X); mto($$, $2); }
| term U_Token term { binary($$, $1, ID_U, $3, bool_typet{}); }
| term R_Token term { binary($$, $1, ID_R, $3, bool_typet{}); }
| term EQUAL_Token term { binary($$, $1, ID_equal, $3, bool_typet{}); }
| term NOTEQUAL_Token term { binary($$, $1, ID_notequal, $3, bool_typet{}); }
| term LT_Token term { binary($$, $1, ID_lt, $3, bool_typet{}); }
| term LE_Token term { binary($$, $1, ID_le, $3, bool_typet{}); }
| term GT_Token term { binary($$, $1, ID_gt, $3, bool_typet{}); }
| term GE_Token term { binary($$, $1, ID_ge, $3, bool_typet{}); }
| term UNION_Token term { binary($$, $1, ID_smv_union, $3, bool_typet{}); }
| term IN_Token term { binary($$, $1, ID_smv_setin, $3, bool_typet{}); }
| term NOTIN_Token term { binary($$, $1, ID_smv_setnotin, $3, bool_typet{}); }
| term U_Token term { binary($$, $1, ID_U, $3); }
| term R_Token term { binary($$, $1, ID_R, $3); }
| term EQUAL_Token term { binary($$, $1, ID_equal, $3); }
| term NOTEQUAL_Token term { binary($$, $1, ID_notequal, $3); }
| term LT_Token term { binary($$, $1, ID_lt, $3); }
| term LE_Token term { binary($$, $1, ID_le, $3); }
| term GT_Token term { binary($$, $1, ID_gt, $3); }
| term GE_Token term { binary($$, $1, ID_ge, $3); }
| term UNION_Token term { binary($$, $1, ID_smv_union, $3); }
| term IN_Token term { binary($$, $1, ID_smv_setin, $3); }
| term NOTIN_Token term { binary($$, $1, ID_smv_setnotin, $3); }
;

formula_list: formula { init($$); mto($$, $1); }
Expand Down Expand Up @@ -580,7 +571,7 @@ cases :
;

case : formula ':' formula ';'
{ binary($$, $1, ID_case, $3, stack_expr($3).type()); }
{ binary($$, $1, ID_case, $3); }
;

switches :
Expand Down

0 comments on commit 8a54d3a

Please sign in to comment.