Updates parser and type checking to handle ranges

We now support ranges on code contracts when specifiying
which portions of an array should or should not change.
We update the parser and type checking to support this
new annotations within assigns clauses.

Signed-off-by: Felipe R. Monteiro <[email protected]>

Author: feliperodri

src/ansi-c/c_typecheck_base.h

@@ -163,6 +163,7 @@ class c_typecheck_baset:
   virtual void typecheck_expr_operands(exprt &expr);
   virtual void typecheck_expr_comma(exprt &expr);
   virtual void typecheck_expr_constant(exprt &expr);
+  virtual void typecheck_expr_range(exprt &expr);
   virtual void typecheck_expr_side_effect(side_effect_exprt &expr);
   virtual void typecheck_expr_unary_arithmetic(exprt &expr);
   virtual void typecheck_expr_unary_boolean(exprt &expr);

src/ansi-c/c_typecheck_expr.cpp

@@ -491,6 +491,10 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
   {
     // already type checked
   }
+  else if(expr.id() == ID_range)
+  {
+    typecheck_expr_range(expr);
+  }
   else
   {
     error().source_location = expr.source_location();
@@ -499,6 +503,16 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
   }
 }
 
+void c_typecheck_baset::typecheck_expr_range(exprt &expr)
+{
+  // Already type checked
+  exprt &lower = to_range_exprt(expr).lower();
+  exprt &upper = to_range_exprt(expr).upper();
+
+  implicit_typecast_arithmetic(lower);
+  implicit_typecast_arithmetic(upper);
+}
+
 void c_typecheck_baset::typecheck_expr_comma(exprt &expr)
 {
   expr.type() = to_binary_expr(expr).op1().type();

src/ansi-c/parser.y

@@ -102,6 +102,7 @@ extern char *yyansi_ctext;
 %token TOK_ANDAND    "&&"
 %token TOK_OROR      "||"
 %token TOK_ELLIPSIS  "..."
+%token TOK_RANGE     ".."
 
 /*** modifying assignment operators ***/
 
@@ -3243,7 +3244,7 @@ cprover_contract:
           set($$, ID_C_spec_requires);
           mto($$, $3);
         }
-        | TOK_CPROVER_ASSIGNS '(' argument_expression_list ')'
+        | TOK_CPROVER_ASSIGNS '(' target_list ')'
         {
           $$=$1;
           set($$, ID_C_spec_assigns);
@@ -3252,6 +3253,76 @@ cprover_contract:
         }
         ;
 
+target_list:
+          target
+        {
+          init($$, ID_target_list);
+          mto($$, $1);
+        }
+        | target_list ',' target
+        {
+          $$=$1;
+          mto($$, $3);
+        }
+        ;
+
+target:
+          deref_target
+        | target '[' array_index ']'
+        { binary($$, $1, $2, ID_range, $3); }
+        | target '[' array_range ']'
+        { binary($$, $1, $2, ID_range, $3); }
+        ;
+
+array_index:
+          identifier
+        | integer
+        ;
+
+array_range:
+        array_index TOK_RANGE array_index
+        {
+          $$=$2;
+          set($$, ID_range);
+          mto($$, $1);
+          mto($$, $3);
+        }
+        ;
+
+deref_target:
+          member_target
+        | '*' deref_target
+        {
+          $$=$1;
+          set($$, ID_dereference);
+          mto($$, $2);
+        }
+        ;
+
+member_target:
+          primary_target
+        | member_target '.' member_name
+        {
+          $$=$2;
+          set($$, ID_member);
+          mto($$, $1);
+          parser_stack($$).set(ID_component_name, parser_stack($3).get(ID_C_base_name));
+        }
+        | member_target TOK_ARROW member_name
+        {
+          $$=$2;
+          set($$, ID_ptrmember);
+          mto($$, $1);
+          parser_stack($$).set(ID_component_name, parser_stack($3).get(ID_C_base_name));
+        }
+        ;
+
+primary_target:
+          identifier
+        | '(' target ')'
+        { $$ = $2; }
+        ;
+
 cprover_contract_sequence:
           cprover_contract
         | cprover_contract_sequence cprover_contract

src/ansi-c/scanner.l

@@ -1517,6 +1517,7 @@ __decltype          { if(PARSER.cpp98 &&
 "&&"            { loc(); return TOK_ANDAND; }
 "||"            { loc(); return TOK_OROR; }
 "..."           { loc(); return TOK_ELLIPSIS; }
+".."            { loc(); return TOK_RANGE; }
 
 "*="            { loc(); return TOK_MULTASSIGN; }
 "/="            { loc(); return TOK_DIVASSIGN; }

src/util/std_expr.h

@@ -824,6 +824,67 @@ inline multi_ary_exprt &to_multi_ary_expr(exprt &expr)
   return static_cast<multi_ary_exprt &>(expr);
 }
 
+/// \brief A base class for int-range expressions
+class range_exprt : public expr_protectedt
+{
+public:
+  range_exprt(exprt &lower, exprt &upper, typet _type)
+    : expr_protectedt(
+        ID_range,
+        std::move(_type),
+        {std::move(lower), std::move(upper)})
+  {
+  }
+
+  exprt &lower()
+  {
+    return op0();
+  }
+
+  const exprt &lower() const
+  {
+    return op0();
+  }
+
+  exprt &upper()
+  {
+    return op1();
+  }
+
+  const exprt &upper() const
+  {
+    return op1();
+  }
+
+  const exprt &op2() const = delete;
+  exprt &op2() = delete;
+  const exprt &op3() const = delete;
+  exprt &op3() = delete;
+};
+
+/// \brief Cast an exprt to a \ref range_exprt
+///
+/// \a expr must be known to be \ref range_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref range_exprt
+inline const range_exprt &to_range_exprt(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_range);
+  return static_cast<const range_exprt &>(expr);
+}
+
+/// \brief Cast an exprt to a \ref range_exprt
+///
+/// \a expr must be known to be \ref range_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref range_exprt
+inline range_exprt &to_range_exprt(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_range);
+  return static_cast<range_exprt &>(expr);
+}
 
 /// \brief The plus expression
 /// Associativity is not specified.