@@ -1001,7 +1001,21 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
1001
1001
}
1002
1002
else if (expr.id () == ID_smv_setin)
1003
1003
{
1004
- expr.type ()=bool_typet ();
1004
+ // The RHS can be a set or a singleton
1005
+ #if 0
1006
+ auto &lhs = to_binary_expr(expr).lhs();
1007
+ auto &rhs = to_binary_expr(expr).rhs();
1008
+
1009
+ typecheck_expr_rec(lhs, mode);
1010
+ typecheck_expr_rec(rhs, mode);
1011
+
1012
+ typet op_type = type_union(lhs.type(), rhs.type(), expr.source_location());
1013
+
1014
+ convert_expr_to(lhs, op_type);
1015
+ convert_expr_to(rhs, op_type);
1016
+ #endif
1017
+
1018
+ expr.type () = bool_typet ();
1005
1019
}
1006
1020
else if (expr.id () == ID_smv_setnotin)
1007
1021
{
@@ -1232,6 +1246,11 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
1232
1246
<< " signed operand must have unsigned word type" ;
1233
1247
}
1234
1248
}
1249
+ else if (expr.id () == ID_smv_set)
1250
+ {
1251
+ // a set literal
1252
+ expr.type () = typet{ID_smv_set};
1253
+ }
1235
1254
else
1236
1255
{
1237
1256
throw errort ().with_location (expr.find_source_location ())
@@ -1285,28 +1304,50 @@ Function: smv_typecheckt::convert_expr_to
1285
1304
1286
1305
\*******************************************************************/
1287
1306
1288
- void smv_typecheckt::convert_expr_to (exprt &expr, const typet &type )
1307
+ void smv_typecheckt::convert_expr_to (exprt &expr, const typet &dest_type )
1289
1308
{
1290
- PRECONDITION (type.is_not_nil ());
1309
+ const auto &src_type = expr.type ();
1310
+
1311
+ PRECONDITION (dest_type.is_not_nil ());
1291
1312
1292
- if (expr. type () != type )
1313
+ if (src_type != dest_type )
1293
1314
{
1294
- if (type.id () == ID_signedbv || type.id () == ID_unsignedbv)
1315
+ if (src_type.id () == ID_smv_set && expr.id () == ID_smv_set)
1316
+ {
1317
+ // sets can be assigned to scalars, which yields a nondeterministic
1318
+ // choice
1319
+ std::string identifier =
1320
+ module + " ::var::" + std::to_string (nondet_count++);
1321
+
1322
+ expr.set (ID_identifier, identifier);
1323
+ expr.set (" #smv_nondet_choice" , true );
1324
+
1325
+ expr.id (ID_constraint_select_one);
1326
+ expr.type () = dest_type;
1327
+
1328
+ // apply recursively
1329
+ for (auto &op : expr.operands ())
1330
+ convert_expr_to (op, dest_type);
1331
+
1332
+ return ;
1333
+ }
1334
+
1335
+ if (dest_type.id () == ID_signedbv || dest_type.id () == ID_unsignedbv)
1295
1336
{
1296
1337
// no implicit conversion
1297
1338
}
1298
- else if (type .id () == ID_range)
1339
+ else if (dest_type .id () == ID_range)
1299
1340
{
1300
- if (expr. type () .id () == ID_range)
1341
+ if (src_type .id () == ID_range)
1301
1342
{
1302
1343
// range to range
1303
1344
if (expr.id () == ID_constant)
1304
1345
{
1305
1346
// re-type the constant
1306
1347
auto value = numeric_cast_v<mp_integer>(to_constant_expr (expr));
1307
- if (to_range_type (type ).includes (value))
1348
+ if (to_range_type (dest_type ).includes (value))
1308
1349
{
1309
- expr = from_integer (value, type );
1350
+ expr = from_integer (value, dest_type );
1310
1351
return ;
1311
1352
}
1312
1353
}
@@ -1318,26 +1359,40 @@ void smv_typecheckt::convert_expr_to(exprt &expr, const typet &type)
1318
1359
for (auto &op : expr.operands ())
1319
1360
{
1320
1361
if (!condition)
1321
- convert_expr_to (op, type );
1362
+ convert_expr_to (op, dest_type );
1322
1363
1323
1364
condition = !condition;
1324
1365
}
1325
- expr.type () = type ;
1366
+ expr.type () = dest_type ;
1326
1367
return ;
1327
1368
}
1328
1369
else
1329
1370
{
1330
- expr = typecast_exprt{expr, type };
1371
+ expr = typecast_exprt{expr, dest_type };
1331
1372
return ;
1332
1373
}
1333
1374
}
1375
+ else if (src_type.id () == ID_integer)
1376
+ {
1377
+ // integer to range
1378
+ if (expr.id () == ID_constant)
1379
+ {
1380
+ // re-type the constant
1381
+ auto value = numeric_cast_v<mp_integer>(to_constant_expr (expr));
1382
+ if (to_range_type (dest_type).includes (value))
1383
+ {
1384
+ expr = from_integer (value, dest_type);
1385
+ return ;
1386
+ }
1387
+ }
1388
+ }
1334
1389
}
1335
- else if (type .id () == ID_bool)
1390
+ else if (dest_type .id () == ID_bool)
1336
1391
{
1337
1392
// legacy -- convert 0/1 to false/true
1338
- if (expr. type () .id () == ID_range)
1393
+ if (src_type .id () == ID_range)
1339
1394
{
1340
- auto &range_type = to_range_type (expr. type () );
1395
+ auto &range_type = to_range_type (src_type );
1341
1396
if (range_type.get_from () == 0 && range_type.get_to () == 0 )
1342
1397
{
1343
1398
expr = false_exprt{};
@@ -1350,43 +1405,41 @@ void smv_typecheckt::convert_expr_to(exprt &expr, const typet &type)
1350
1405
}
1351
1406
}
1352
1407
}
1353
- else if (type .id () == ID_enumeration)
1408
+ else if (dest_type .id () == ID_enumeration)
1354
1409
{
1355
- auto &e_type = to_enumeration_type (type );
1410
+ auto &e_type = to_enumeration_type (dest_type );
1356
1411
1357
- if (expr.id () == ID_constant && expr. type () .id () == ID_enumeration)
1412
+ if (expr.id () == ID_constant && src_type .id () == ID_enumeration)
1358
1413
{
1359
- if (is_contained_in (to_enumeration_type (expr. type () ), e_type))
1414
+ if (is_contained_in (to_enumeration_type (src_type ), e_type))
1360
1415
{
1361
1416
// re-type the constant
1362
- expr.type () = type ;
1417
+ expr.type () = dest_type ;
1363
1418
return ;
1364
1419
}
1365
1420
else
1366
1421
{
1367
1422
throw errort ().with_location (expr.find_source_location ())
1368
1423
<< " enum " << to_string (expr) << " not a member of "
1369
- << to_string (type );
1424
+ << to_string (dest_type );
1370
1425
}
1371
1426
}
1372
1427
else if (expr.id () == ID_typecast)
1373
1428
{
1374
1429
// created by type unions
1375
1430
auto &op = to_typecast_expr (expr).op ();
1376
- if (
1377
- expr.type ().id () == ID_enumeration &&
1378
- op.type ().id () == ID_enumeration)
1431
+ if (src_type.id () == ID_enumeration && op.type ().id () == ID_enumeration)
1379
1432
{
1380
- convert_expr_to (op, type );
1433
+ convert_expr_to (op, dest_type );
1381
1434
expr = std::move (op);
1382
1435
}
1383
1436
}
1384
1437
}
1385
1438
1386
1439
throw errort ().with_location (expr.find_source_location ())
1387
- << " Expected expression of type `" << to_string (type )
1440
+ << " Expected expression of type `" << to_string (dest_type )
1388
1441
<< " ', but got expression `" << to_string (expr) << " ', which is of type `"
1389
- << to_string (expr. type () ) << " '" ;
1442
+ << to_string (src_type ) << " '" ;
1390
1443
}
1391
1444
}
1392
1445
0 commit comments