Merge pull request #1024 from diffblue/arithmetic1

SMV: word-level arithmetic

Author: tautschnig

regression/smv/word/arithmetic1.desc

@@ -0,0 +1,7 @@
+CORE
+arithmetic1.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/smv/word/arithmetic1.smv

@@ -0,0 +1,25 @@
+MODULE main
+
+SPEC uwconst(123, 8) + uwconst(1, 8) = uwconst(124, 8)
+SPEC uwconst(123, 8) + uwconst(200, 8) = uwconst(67, 8)
+SPEC uwconst(123, 8) - uwconst(1, 8) = uwconst(122, 8)
+SPEC uwconst(123, 8) - uwconst(200, 8) = uwconst(179, 8)
+SPEC uwconst(123, 8) * uwconst(2, 8) = uwconst(246, 8)
+SPEC uwconst(123, 8) * uwconst(3, 8) = uwconst(113, 8)
+SPEC uwconst(123, 8) / uwconst(2, 8) = uwconst(61, 8)
+SPEC uwconst(123, 8) / uwconst(3, 8) = uwconst(41, 8)
+SPEC uwconst(123, 8) mod uwconst(2, 8) = uwconst(1, 8)
+SPEC uwconst(123, 8) mod uwconst(3, 8) = uwconst(0, 8)
+SPEC -uwconst(123, 8) = uwconst(133, 8)
+
+SPEC swconst(123, 8) + swconst(1, 8) = swconst(124, 8)
+SPEC swconst(123, 8) + swconst(-56, 8) = swconst(67, 8)
+SPEC swconst(123, 8) - swconst(1, 8) = swconst(122, 8)
+SPEC swconst(123, 8) - swconst(-56, 8) = swconst(-77, 8)
+SPEC swconst(123, 8) * swconst(2, 8) = swconst(-10, 8)
+SPEC swconst(123, 8) * swconst(3, 8) = swconst(113, 8)
+SPEC swconst(123, 8) / swconst(2, 8) = swconst(61, 8)
+SPEC swconst(123, 8) / swconst(3, 8) = swconst(41, 8)
+SPEC swconst(123, 8) mod swconst(2, 8) = swconst(1, 8)
+SPEC swconst(123, 8) mod swconst(3, 8) = swconst(0, 8)
+SPEC -swconst(123, 8) = swconst(-123, 8)

src/smvlang/expr2smv.cpp

@@ -595,6 +595,10 @@ bool expr2smvt::convert(
     return convert_binary(
       src, dest, src.id_string(), precedence = precedencet::MULT);
 
+  else if(src.id() == ID_mod)
+    return convert_binary(
+      src, dest, src.id_string(), precedence = precedencet::MULT);
+
   else if(src.id() == ID_smv_setin)
     return convert_binary(src, dest, "in", precedence = precedencet::IN);
 

src/smvlang/scanner.l

@@ -200,6 +200,8 @@ void newlocation(YYSTYPE &x)
 "!"		return NOT_Token;
 "+"		return PLUS_Token;
 "-"		return MINUS_Token;
+"*"		return TIMES_Token;
+"/"		return DIVIDE_Token;
 "|"		return OR_Token;
 "&"		return AND_Token;
 "->"		return IMPLIES_Token;

src/smvlang/smv_typecheck.cpp

@@ -1004,10 +1004,16 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
       uminus_expr.type() =
         (-smv_ranget::from_type(to_range_type(op_type))).to_type();
     }
+    else if(op_type.id() == ID_signedbv || op_type.id() == ID_unsignedbv)
+    {
+      uminus_expr.type() = op_type;
+    }
     else
+    {
       throw errort().with_location(expr.source_location())
-        << "Operand to unary minus must be integer, but got "
+        << "Operand to unary minus must be integer or word type, but got "
         << to_string(op_type);
+    }
 
     // constant folding
     if(uminus_expr.op().is_constant())