Merge pull request #3197 from diffblue/acsl-operators

fix ACSL unicode operators

Author: tautschnig

regression/cbmc/ACSL/operators.c

@@ -0,0 +1,28 @@
+void boolean()
+{
+  __CPROVER_bool a, b;
+  __CPROVER_assert((a ≡ b) == (a == b), "≥");
+  __CPROVER_assert((a ≢ b) == (a != b), "≢");
+  __CPROVER_assert((a ⇒ b) == (!a || b), "⇒");
+  __CPROVER_assert((a ⇔ b) == (a == b), "⇔");
+  __CPROVER_assert((a ∧ b) == (a && b), "∧");
+  __CPROVER_assert((a ∨ b) == (a || b), "∨");
+  __CPROVER_assert((a ⊻ b) == (a != b), "⊻");
+  __CPROVER_assert((¬ a) == (!a), "¬");
+}
+
+void relations()
+{
+  int a, b;
+  __CPROVER_assert((a ≥ b) == (a >= b), "≥");
+  __CPROVER_assert((a ≤ b) == (a <= b), "≤");
+  __CPROVER_assert((a ≡ b) == (a == b), "≥");
+  __CPROVER_assert((a ≢ b) == (a != b), "≢");
+  __CPROVER_assert((− a) == (-a), "−");
+}
+
+int main()
+{
+  boolean();
+  relations();
+}

regression/cbmc/ACSL/operators.desc

@@ -0,0 +1,8 @@
+CORE
+operators.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/ansi-c/c_typecheck_expr.cpp

@@ -180,7 +180,9 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
     typecheck_expr_unary_arithmetic(expr);
   else if(expr.id()==ID_not)
     typecheck_expr_unary_boolean(expr);
-  else if(expr.id()==ID_and || expr.id()==ID_or || expr.id()==ID_implies)
+  else if(
+    expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies ||
+    expr.id() == ID_xor)
     typecheck_expr_binary_boolean(expr);
   else if(expr.id()==ID_address_of)
     typecheck_expr_address_of(expr);

src/ansi-c/expr2c.cpp

@@ -3815,7 +3815,7 @@ std::string expr2ct::convert_with_precedence(
     return convert_multi_ary(src, "||", precedence=4, false);
 
   else if(src.id()==ID_xor)
-    return convert_multi_ary(src, "^", precedence=7, false);
+    return convert_multi_ary(src, "!=", precedence = 9, false);
 
   else if(src.id()==ID_implies)
     return convert_binary(src, "==>", precedence=3, true);

src/ansi-c/parser.y

@@ -174,6 +174,7 @@ extern char *yyansi_ctext;
 %token TOK_EXISTS      "exists"
 %token TOK_ACSL_FORALL "\\forall"
 %token TOK_ACSL_EXISTS "\\exists"
+%token TOK_ACSL_LET    "\\let"
 %token TOK_ARRAY_OF    "array_of"
 %token TOK_CPROVER_BITVECTOR "__CPROVER_bitvector"
 %token TOK_CPROVER_FLOATBV "__CPROVER_floatbv"
@@ -190,6 +191,7 @@ extern char *yyansi_ctext;
 %token TOK_CPROVER_ENSURES  "__CPROVER_ensures"
 %token TOK_IMPLIES     "==>"
 %token TOK_EQUIVALENT  "<==>"
+%token TOK_XORXOR      "^^"
 %token TOK_TRUE        "TRUE"
 %token TOK_FALSE       "FALSE"
 %token TOK_REAL        "__real__"
@@ -775,9 +777,15 @@ logical_and_expression:
         { binary($$, $1, $2, ID_and, $3); }
         ;
 
-logical_or_expression:
+logical_xor_expression:
           logical_and_expression
-        | logical_or_expression TOK_OROR logical_and_expression
+        | logical_xor_expression TOK_XORXOR logical_and_expression
+        { binary($$, $1, $2, ID_xor, $3); }
+        ;
+
+logical_or_expression:
+          logical_xor_expression
+        | logical_or_expression TOK_OROR logical_xor_expression
         { binary($$, $1, $2, ID_or, $3); }
         ;
 

src/ansi-c/scanner.l

@@ -1223,41 +1223,67 @@ __decltype          { if(PARSER.cpp98 &&
 "__CPROVER_requires"     { loc(); return TOK_CPROVER_REQUIRES; }
 "__CPROVER_ensures"      { loc(); return TOK_CPROVER_ENSURES; }
 
-"\x22\x00" |
+"\xe2\x88\x80" |
 "\\forall"      { /* Non-standard, obviously. Found in ACSL syntax. */
                   loc(); return TOK_ACSL_FORALL;
                 }
 
-"\x22\x03" |
+"\xe2\x88\x83" |
 "\\exists"      { /* Non-standard, obviously. Found in ACSL syntax. */
                   loc(); return TOK_ACSL_EXISTS;
                 }
-"\x21\xD2" |
+
+"\\let"         { /* Non-standard, obviously. Found in ACSL syntax. */
+                  loc(); return TOK_ACSL_LET;
+                }
+
+"\xe2\x87\x92" |
 "==>"           { /* Non-standard, obviously. Found in Spec# and ACSL syntax. */
                   loc(); return TOK_IMPLIES;
                 }
 
-"\x21\xD4" |
+"\xe2\x87\x94" |
 "<==>"          { /* Non-standard, obviously. Found in Spec# and ACSL syntax. */
                   loc(); return TOK_EQUIVALENT;
                 }
 
-"\x22\x65"      { /* Non-standard, obviously. Found in ACSL syntax. */
+"\xe2\x89\xa5"  { /* Non-standard, obviously. Found in ACSL syntax. */
                   loc(); return TOK_GE;
                 }
 
-"\x22\x64"      { /* Non-standard, obviously. Found in ACSL syntax. */
+"\xe2\x89\xa1"  { /* Non-standard, obviously. Found in ACSL syntax. */
+                  loc(); return TOK_EQ;
+                }
+
+"\xe2\x89\xa2"  { /* Non-standard, obviously. Found in ACSL syntax. */
+                  loc(); return TOK_NE;
+                }
+
+"\xe2\x89\xa4"  { /* Non-standard, obviously. Found in ACSL syntax. */
                   loc(); return TOK_LE;
                 }
 
-"\x22\x27"      { /* Non-standard, obviously. Found in ACSL syntax. */
+"\xe2\x88\xa7"  { /* Non-standard, obviously. Found in ACSL syntax. */
                   loc(); return TOK_ANDAND;
                 }
 
-"\x22\x28"      { /* Non-standard, obviously. Found in ACSL syntax. */
+"\xe2\x88\xa8"  { /* Non-standard, obviously. Found in ACSL syntax. */
                   loc(); return TOK_OROR;
                 }
 
+"\xc2\xac"      { /* Non-standard, obviously. Found in ACSL syntax. */
+                  loc(); return '!';
+                }
+
+"\xe2\x8a\xbb" |
+"^^"            { /* Non-standard, obviously. Found in ACSL syntax. */
+                  loc(); return TOK_XORXOR;
+                }
+
+"\xe2\x88\x92"  { /* Non-standard, obviously. Found in ACSL syntax. */
+                  loc(); return '-';
+                }
+
 "\\true"        { /* Non-standard, obviously. Found in ACSL syntax. */
                   loc(); return TOK_TRUE;
                 }