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

@@ -168,6 +168,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).op0();
+  exprt &upper = to_range_exprt(expr).op1();
+
+  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

@@ -101,6 +101,7 @@ extern char *yyansi_ctext;
 %token TOK_NE        "!="
 %token TOK_ANDAND    "&&"
 %token TOK_OROR      "||"
+%token TOK_RANGE     ".."
 %token TOK_ELLIPSIS  "..."
 
 /*** modifying assignment operators ***/
@@ -532,15 +533,62 @@ target_list:
         ;
 
 target:
+          deref_target
+        | target '[' array_index ']'
+        { binary($$, $1, $2, ID_range, $3); }
+        | target '[' array_range ']'
+        { binary($$, $1, $2, ID_range, $3); }
+        ;
+
+array_index:
           identifier
-        | '*' target
+        | integer
+        ;
+
+array_range:
+        array_index ',' 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; }
+        ;
+
 statement_expression: '(' compound_statement ')'
         { 
           $$=$1;

src/util/std_expr.h

@@ -824,6 +824,51 @@ 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)})
+  {
+  }
+
+  // make op0 and op1 public
+  using exprt::op0;
+  using exprt::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.