SMV: abs, bool, count, max, min, toint, word1

CHANGELOG

@@ -6,6 +6,7 @@
 * SystemVerilog: fix for #-# and #=# for empty matches
 * SystemVerilog: fix for |-> and |=> for empty matches
 * LTL/SVA to Buechi with --buechi
+* SMV: abs, bool, count, max, min, toint, word1
 
 # EBMC 5.6
 

regression/smv/expressions/smv_abs1.desc

@@ -0,0 +1,13 @@
+KNOWNBUG
+smv_abs1.smv
+
+^\[.*\] abs\(0\) = 0: PROVED .*$
+^\[.*\] abs\(1\) = 1: PROVED .*$
+^\[.*\] abs\(2\) = 2: PROVED .*$
+^\[.*\] abs\(-1\) = 1: PROVED .*$
+^\[.*\] abs\(-2\) = 2: PROVED .*$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Unary minus on ranges does not work.

regression/smv/expressions/smv_abs1.smv

@@ -0,0 +1,7 @@
+MODULE main
+
+CTLSPEC abs(0) = 0
+CTLSPEC abs(1) = 1
+CTLSPEC abs(2) = 2
+CTLSPEC abs(-1) = 1
+CTLSPEC abs(-2) = 2

regression/smv/expressions/smv_bool1.desc

@@ -0,0 +1,11 @@
+CORE
+smv_bool1.smv
+
+^\[.*\] !bool\(0\): PROVED .*$
+^\[.*\] bool\(1\): PROVED .*$
+^\[.*\] bool\(2\): PROVED .*$
+^\[.*\] !bool\(0ud1_0\): PROVED .*$
+^\[.*\] bool\(0ud1_1\): PROVED .*$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/smv/expressions/smv_bool1.smv

@@ -0,0 +1,7 @@
+MODULE main
+
+CTLSPEC !bool(0)
+CTLSPEC bool(1)
+CTLSPEC bool(2)
+CTLSPEC !bool(uwconst(0, 1))
+CTLSPEC bool(uwconst(1, 1))

regression/smv/expressions/smv_count1.desc

@@ -0,0 +1,12 @@
+CORE broken-smt-backend
+smv_count1.smv
+
+^\[.*\] count\(FALSE\) = 0: PROVED .*$
+^\[.*\] count\(TRUE\) = 1: PROVED .*$
+^\[.*\] count\(FALSE, TRUE\) = 1: PROVED .*$
+^\[.*\] count\(TRUE, FALSE\) = 1: PROVED .*$
+^\[.*\] count\(TRUE, TRUE, TRUE\) = 3: PROVED .*$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

regression/smv/expressions/smv_count1.smv

@@ -0,0 +1,7 @@
+MODULE main
+
+CTLSPEC count(FALSE) = 0
+CTLSPEC count(TRUE) = 1
+CTLSPEC count(FALSE, TRUE) = 1
+CTLSPEC count(TRUE, FALSE) = 1
+CTLSPEC count(TRUE, TRUE, TRUE) = 3

regression/smv/expressions/smv_max1.desc

@@ -0,0 +1,11 @@
+CORE
+smv_max1.smv
+
+^\[.*\] max\(0, 1\) = 1: PROVED .*$
+^\[.*\] max\(-1, -2\) = -1: PROVED .*$
+^\[.*\] max\(-1, 1\) = 1: PROVED .*$
+^\[.*\] max\(1, 2\) = 2: PROVED .*$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

regression/smv/expressions/smv_max1.smv

@@ -0,0 +1,6 @@
+MODULE main
+
+CTLSPEC max(0, 1) = 1
+CTLSPEC max(-1, -2) = -1
+CTLSPEC max(-1, 1) = 1
+CTLSPEC max(1, 2) = 2

regression/smv/expressions/smv_min1.desc

@@ -0,0 +1,11 @@
+CORE
+smv_min1.smv
+
+^\[.*\] min\(0, 1\) = 0: PROVED .*$
+^\[.*\] min\(-1, -2\) = -2: PROVED .*$
+^\[.*\] min\(-1, 1\) = -1: PROVED .*$
+^\[.*\] min\(1, 2\) = 1: PROVED .*$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

regression/smv/expressions/smv_min1.smv

@@ -0,0 +1,6 @@
+MODULE main
+
+CTLSPEC min(0, 1) = 0
+CTLSPEC min(-1, -2) = -2
+CTLSPEC min(-1, 1) = -1
+CTLSPEC min(1, 2) = 1

regression/smv/expressions/smv_toint1.desc

@@ -0,0 +1,14 @@
+KNOWNBUG
+smv_toint1.smv
+
+^\[.*\] toint\(0\) = 0: PROVED .*$
+^\[.*\] toint\(1\) = 1: PROVED .*$
+^\[.*\] toint\(FALSE\) = 0: PROVED .*$
+^\[.*\] toint\(TRUE\) = 1: PROVED .*$
+^\[.*\] toint\(0ud8_1\) = 1: PROVED .*$
+^\[.*\] toint\(-0sd8_1\) = -1: PROVED .*$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Missing typecasts.

regression/smv/expressions/smv_toint1.smv

@@ -0,0 +1,8 @@
+MODULE main
+
+CTLSPEC toint(0) = 0
+CTLSPEC toint(1) = 1
+CTLSPEC toint(FALSE) = 0
+CTLSPEC toint(TRUE) = 1
+CTLSPEC toint(uwconst(1, 8)) = 1
+CTLSPEC toint(swconst(-1, 8)) = -1

regression/smv/expressions/smv_word1.desc

@@ -0,0 +1,9 @@
+CORE
+smv_word1.smv
+
+^\[.*\] word1\(FALSE\) = 0ud1_0: PROVED .*$
+^\[.*\] word1\(TRUE\) = 0ud1_1: PROVED .*$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

regression/smv/expressions/smv_word1.smv

@@ -0,0 +1,4 @@
+MODULE main
+
+CTLSPEC word1(FALSE) = uwconst(0, 1)
+CTLSPEC word1(TRUE) = uwconst(1, 1)

src/hw_cbmc_irep_ids.h

@@ -17,12 +17,18 @@ IREP_ID_ONE(F)
 IREP_ID_ONE(E)
 IREP_ID_ONE(G)
 IREP_ID_ONE(X)
+IREP_ID_ONE(smv_abs)
 IREP_ID_ONE(smv_bitimplies)
+IREP_ID_ONE(smv_bool)
+IREP_ID_ONE(smv_count)
 IREP_ID_ONE(smv_extend)
+IREP_ID_ONE(smv_max)
+IREP_ID_ONE(smv_min)
 IREP_ID_ONE(smv_next)
 IREP_ID_ONE(smv_iff)
 IREP_ID_TWO(C_smv_iff, "#smv_iff")
 IREP_ID_ONE(smv_resize)
+IREP_ID_ONE(smv_toint)
 IREP_ID_ONE(smv_set)
 IREP_ID_ONE(smv_setin)
 IREP_ID_ONE(smv_setnotin)
@@ -32,6 +38,7 @@ IREP_ID_ONE(smv_swconst)
 IREP_ID_ONE(smv_union)
 IREP_ID_ONE(smv_unsigned_cast)
 IREP_ID_ONE(smv_uwconst)
+IREP_ID_ONE(smv_word1)
 IREP_ID_ONE(smv_H)
 IREP_ID_ONE(smv_bounded_H)
 IREP_ID_ONE(smv_O)

src/smvlang/expr2smv.cpp

@@ -831,6 +831,27 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src)
   else if(src.id() == ID_smv_unsigned_cast)
     return convert_function_application("unsigned", src);
 
+  else if(src.id() == ID_smv_abs)
+    return convert_function_application("abs", src);
+
+  else if(src.id() == ID_smv_bool)
+    return convert_function_application("bool", src);
+
+  else if(src.id() == ID_smv_count)
+    return convert_function_application("count", src);
+
+  else if(src.id() == ID_smv_max)
+    return convert_function_application("max", src);
+
+  else if(src.id() == ID_smv_min)
+    return convert_function_application("min", src);
+
+  else if(src.id() == ID_smv_toint)
+    return convert_function_application("toint", src);
+
+  else if(src.id() == ID_smv_word1)
+    return convert_function_application("word1", src);
+
   else if(src.id() == ID_typecast)
   {
     return convert_typecast(to_typecast_expr(src));

src/smvlang/parser.y

@@ -94,6 +94,12 @@ Function: init
    stack_expr(x_result).add_to_operands(std::move(lhs), std::move(rhs));
  }
 
+static void unary(YYSTYPE &result, const irep_idt &id, YYSTYPE &op)
+{
+  init(result, id);
+  mto(result, op);
+}
+
 /*******************************************************************\
 
 Function: j_binary
@@ -234,6 +240,7 @@ static void new_module(YYSTYPE &module)
 %token xor_Token	"xor"
 %token xnor_Token	"xnor"
 %token self_Token	"self"
+%token toint_Token	"toint"
 %token TRUE_Token	"TRUE"
 %token FALSE_Token	"FALSE"
 %token count_Token	"count"
@@ -684,6 +691,9 @@ term       : constant
            | variable_identifier
            | '(' formula ')'          { $$=$2; }
            | NOT_Token term           { init($$, ID_not); mto($$, $2); }
+           | "abs" '(' term ')'       { unary($$, ID_smv_abs, $3); }
+           | "max" '(' term ',' term ')' { binary($$, $3, ID_smv_max, $5); }
+           | "min" '(' term ',' term ')' { binary($$, $3, ID_smv_min, $5); }
            | term AND_Token term      { j_binary($$, $1, ID_and, $3); }
            | term OR_Token term       { j_binary($$, $1, ID_or, $3); }
            | term xor_Token term      { j_binary($$, $1, ID_xor, $3); }
@@ -706,11 +716,15 @@ term       : constant
            | term GTGT_Token term     { binary($$, $1, ID_shr, $3); }
            | term LTLT_Token term     { binary($$, $1, ID_shl, $3); }
            | term COLONCOLON_Token term { binary($$, $1, ID_concatenation, $3); }
+           | "word1" '(' term ')'     { unary($$, ID_smv_word1, $3); }
+           | "bool" '(' term ')'      { unary($$, ID_smv_bool, $3); }
+           | "toint" '(' term ')'     { unary($$, ID_smv_toint, $3); }
+           | "count" '(' term_list ')' { $$=$3; stack_expr($$).id(ID_smv_count); }
            | swconst_Token '(' term ',' term ')' { binary($$, $3, ID_smv_swconst, $5); }
            | uwconst_Token '(' term ',' term ')' { binary($$, $3, ID_smv_uwconst, $5); }
-           | signed_Token '(' term ')' { init($$, ID_smv_signed_cast); mto($$, $3); }
-           | unsigned_Token '(' term ')' { init($$, ID_smv_unsigned_cast); mto($$, $3); }
-           | sizeof_Token '(' term ')' { init($$, ID_smv_sizeof); mto($$, $3); }
+           | signed_Token '(' term ')' { unary($$, ID_smv_signed_cast, $3); }
+           | unsigned_Token '(' term ')' { unary($$, ID_smv_unsigned_cast, $3); }
+           | sizeof_Token '(' term ')' { unary($$, ID_smv_sizeof, $3); }
            | extend_Token '(' term ',' term ')' { binary($$, $3, ID_smv_extend, $5); }
            | resize_Token '(' term ',' term ')' { binary($$, $3, ID_smv_resize, $5); }
            | term union_Token term    { binary($$, $1, ID_smv_union, $3); }
@@ -791,6 +805,11 @@ set_body_expr:
            | set_body_expr ',' formula { $$=$1; mto($$, $3); }
            ;
 
+term_list:
+             term { init($$); mto($$, $1); }
+           | term_list ',' term { $$=$1; mto($$, $3); }
+           ;
+
 identifier : IDENTIFIER_Token
            | QIDENTIFIER_Token
            {

src/smvlang/scanner.l

@@ -121,6 +121,7 @@ void newlocation(YYSTYPE &x)
 "extend"	token(extend_Token);
 "resize"	token(resize_Token);
 "sizeof"	token(sizeof_Token);
+"toint"		token(toint_Token);
 "uwconst"	token(uwconst_Token);
 "swconst"	token(swconst_Token);