smt2_parser: avoid access to vector without prior size check

Daniel Kroening · Daniel Kroening · commit bffb1ca01356 · 2018-06-12T18:55:25.000+01:00
diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp
@@ -313,24 +313,26 @@ exprt smt2_parsert::function_application(
   return nil_exprt();
 }
 
-exprt smt2_parsert::cast_bv_to_signed(const exprt &expr)
+exprt::operandst smt2_parsert::cast_bv_to_signed(const exprt::operandst &op)
 {
-  if(expr.type().id()==ID_signedbv) // no need to cast
-    return expr;
+  exprt::operandst result = op;
 
-  if(expr.type().id()!=ID_unsignedbv)
+  for(auto &expr : result)
   {
-    error() << "expected unsigned bitvector" << eom;
-    return expr;
+    if(expr.type().id() == ID_signedbv) // no need to cast
+    {
+    }
+    else if(expr.type().id() != ID_unsignedbv)
+    {
+      error() << "expected unsigned bitvector" << eom;
+    }
+    else
+    {
+      const auto width = to_unsignedbv_type(expr.type()).get_width();
+      expr = typecast_exprt(expr, signedbv_typet(width));
+    }
   }
 
-  auto width=to_unsignedbv_type(expr.type()).get_width();
-  signedbv_typet signed_type(width);
-
-  typecast_exprt result(expr, signed_type);
-  result.op0()=expr;
-  result.type()=signed_type;
-
   return result;
 }
 
@@ -345,17 +347,11 @@ exprt smt2_parsert::cast_bv_to_unsigned(const exprt &expr)
     return expr;
   }
 
-  auto width=to_signedbv_type(expr.type()).get_width();
-  unsignedbv_typet unsigned_type(width);
-
-  typecast_exprt result(expr, unsigned_type);
-  result.op0()=expr;
-  result.type()=unsigned_type;
-
-  return result;
+  const auto width=to_signedbv_type(expr.type()).get_width();
+  return typecast_exprt(expr, unsignedbv_typet(width));
 }
 
-exprt smt2_parsert::multi_ary(irep_idt id, exprt::operandst &op)
+exprt smt2_parsert::multi_ary(irep_idt id, const exprt::operandst &op)
 {
   if(op.empty())
   {
@@ -377,12 +373,12 @@ exprt smt2_parsert::multi_ary(irep_idt id, exprt::operandst &op)
     }
 
     exprt result(id, op[0].type());
-    result.operands().swap(op);
+    result.operands() = op;
     return result;
   }
 }
 
-exprt smt2_parsert::binary_predicate(irep_idt id, exprt::operandst &op)
+exprt smt2_parsert::binary_predicate(irep_idt id, const exprt::operandst &op)
 {
   if(op.size()!=2)
   {
@@ -404,7 +400,7 @@ exprt smt2_parsert::binary_predicate(irep_idt id, exprt::operandst &op)
   }
 }
 
-exprt smt2_parsert::unary(irep_idt id, exprt::operandst &op)
+exprt smt2_parsert::unary(irep_idt id, const exprt::operandst &op)
 {
   if(op.size()!=1)
   {
@@ -415,7 +411,7 @@ exprt smt2_parsert::unary(irep_idt id, exprt::operandst &op)
     return unary_exprt(id, op[0], op[0].type());
 }
 
-exprt smt2_parsert::binary(irep_idt id, exprt::operandst &op)
+exprt smt2_parsert::binary(irep_idt id, const exprt::operandst &op)
 {
   if(op.size()!=2)
   {
@@ -510,45 +506,35 @@ exprt smt2_parsert::function_application()
       }
       else if(id=="bvsle")
       {
-        op[0]=cast_bv_to_signed(op[0]);
-        op[1]=cast_bv_to_signed(op[1]);
-        return binary_predicate(ID_le, op);
+        return binary_predicate(ID_le, cast_bv_to_signed(op));
       }
       else if(id=="bvuge")
       {
         return binary_predicate(ID_ge, op);
       }
       else if(id=="bvsge")
       {
-        op[0]=cast_bv_to_signed(op[0]);
-        op[1]=cast_bv_to_signed(op[1]);
-        return binary_predicate(ID_ge, op);
+        return binary_predicate(ID_ge, cast_bv_to_signed(op));
       }
       else if(id=="bvult")
       {
         return binary_predicate(ID_lt, op);
       }
       else if(id=="bvslt")
       {
-        op[0]=cast_bv_to_signed(op[0]);
-        op[1]=cast_bv_to_signed(op[1]);
-        return binary_predicate(ID_lt, op);
+        return binary_predicate(ID_lt, cast_bv_to_signed(op));
       }
       else if(id=="bvugt")
       {
         return binary_predicate(ID_gt, op);
       }
       else if(id=="bvsgt")
       {
-        op[0]=cast_bv_to_signed(op[0]);
-        op[1]=cast_bv_to_signed(op[1]);
-        return binary_predicate(ID_gt, op);
+        return binary_predicate(ID_gt, cast_bv_to_signed(op));
       }
       else if(id=="bvashr")
       {
-        op[0]=cast_bv_to_signed(op[0]);
-        op[1]=cast_bv_to_signed(op[1]);
-        return cast_bv_to_unsigned(binary(ID_ashr, op));
+        return cast_bv_to_unsigned(binary(ID_ashr, cast_bv_to_signed(op)));
       }
       else if(id=="bvlshr" || id=="bvshr")
       {
@@ -608,9 +594,7 @@ exprt smt2_parsert::function_application()
       }
       else if(id=="bvsdiv")
       {
-        op[0]=cast_bv_to_signed(op[0]);
-        op[1]=cast_bv_to_signed(op[1]);
-        return cast_bv_to_unsigned(binary(ID_div, op));
+        return cast_bv_to_unsigned(binary(ID_div, cast_bv_to_signed(op)));
       }
       else if(id=="bvudiv")
       {
@@ -624,17 +608,13 @@ exprt smt2_parsert::function_application()
       {
         // 2's complement signed remainder (sign follows dividend)
         // This matches our ID_mod, and what C does since C99.
-        op[0]=cast_bv_to_signed(op[0]);
-        op[1]=cast_bv_to_signed(op[1]);
-        return cast_bv_to_unsigned(binary(ID_mod, op));
+        return cast_bv_to_unsigned(binary(ID_mod, cast_bv_to_signed(op)));
       }
       else if(id=="bvsmod")
       {
         // 2's complement signed remainder (sign follows divisor)
         // We don't have that.
-        op[0]=cast_bv_to_signed(op[0]);
-        op[1]=cast_bv_to_signed(op[1]);
-        return cast_bv_to_unsigned(binary(ID_mod, op));
+        return cast_bv_to_unsigned(binary(ID_mod, cast_bv_to_signed(op)));
       }
       else if(id=="bvurem" || id=="%")
       {
diff --git a/src/solvers/smt2/smt2_parser.h b/src/solvers/smt2/smt2_parser.h
@@ -64,17 +64,21 @@ class smt2_parsert:public smt2_tokenizert
   exprt::operandst operands();
   typet function_signature_declaration();
   typet function_signature_definition();
-  exprt multi_ary(irep_idt, exprt::operandst &);
-  exprt binary_predicate(irep_idt, exprt::operandst &);
-  exprt binary(irep_idt, exprt::operandst &);
-  exprt unary(irep_idt, exprt::operandst &);
+  exprt multi_ary(irep_idt, const exprt::operandst &);
+  exprt binary_predicate(irep_idt, const exprt::operandst &);
+  exprt binary(irep_idt, const exprt::operandst &);
+  exprt unary(irep_idt, const exprt::operandst &);
 
   exprt let_expression();
   exprt quantifier_expression(irep_idt);
   exprt function_application(
     const irep_idt &identifier,
     const exprt::operandst &op);
-  exprt cast_bv_to_signed(const exprt &);
+
+  /// Apply typecast to signedbv to expressions in vector
+  exprt::operandst cast_bv_to_signed(const exprt::operandst &);
+
+  /// Apply typecast to unsignedbv to given expression
   exprt cast_bv_to_unsigned(const exprt &);
 };
 

Original file line number	Diff line number	Diff line change
`@@ -313,24 +313,26 @@ exprt smt2_parsert::function_application(`
`313`	`313`	`return nil_exprt();`
`314`	`314`	`}`
`315`	`315`
`316`		`-exprt smt2_parsert::cast_bv_to_signed(const exprt &expr)`
	`316`	`+exprt::operandst smt2_parsert::cast_bv_to_signed(const exprt::operandst &op)`
`317`	`317`	`{`
`318`		`- if(expr.type().id()==ID_signedbv) // no need to cast`
`319`		`- return expr;`
	`318`	`+ exprt::operandst result = op;`
`320`	`319`
`321`		`- if(expr.type().id()!=ID_unsignedbv)`
	`320`	`+ for(auto &expr : result)`
`322`	`321`	`{`
`323`		`- error() << "expected unsigned bitvector" << eom;`
`324`		`- return expr;`
	`322`	`+ if(expr.type().id() == ID_signedbv) // no need to cast`
	`323`	`+ {`
	`324`	`+ }`
	`325`	`+ else if(expr.type().id() != ID_unsignedbv)`
	`326`	`+ {`
	`327`	`+ error() << "expected unsigned bitvector" << eom;`
	`328`	`+ }`
	`329`	`+ else`
	`330`	`+ {`
	`331`	`+ const auto width = to_unsignedbv_type(expr.type()).get_width();`
	`332`	`+ expr = typecast_exprt(expr, signedbv_typet(width));`
	`333`	`+ }`
`325`	`334`	`}`
`326`	`335`
`327`		`- auto width=to_unsignedbv_type(expr.type()).get_width();`
`328`		`- signedbv_typet signed_type(width);`
`329`		`-`
`330`		`- typecast_exprt result(expr, signed_type);`
`331`		`- result.op0()=expr;`
`332`		`- result.type()=signed_type;`
`333`		`-`
`334`	`336`	`return result;`
`335`	`337`	`}`
`336`	`338`
`@@ -345,17 +347,11 @@ exprt smt2_parsert::cast_bv_to_unsigned(const exprt &expr)`
`345`	`347`	`return expr;`
`346`	`348`	`}`
`347`	`349`
`348`		`- auto width=to_signedbv_type(expr.type()).get_width();`
`349`		`- unsignedbv_typet unsigned_type(width);`
`350`		`-`
`351`		`- typecast_exprt result(expr, unsigned_type);`
`352`		`- result.op0()=expr;`
`353`		`- result.type()=unsigned_type;`
`354`		`-`
`355`		`- return result;`
	`350`	`+ const auto width=to_signedbv_type(expr.type()).get_width();`
	`351`	`+ return typecast_exprt(expr, unsignedbv_typet(width));`
`356`	`352`	`}`
`357`	`353`
`358`		`-exprt smt2_parsert::multi_ary(irep_idt id, exprt::operandst &op)`
	`354`	`+exprt smt2_parsert::multi_ary(irep_idt id, const exprt::operandst &op)`
`359`	`355`	`{`
`360`	`356`	`if(op.empty())`
`361`	`357`	`{`
`@@ -377,12 +373,12 @@ exprt smt2_parsert::multi_ary(irep_idt id, exprt::operandst &op)`
`377`	`373`	`}`
`378`	`374`
`379`	`375`	`exprt result(id, op[0].type());`
`380`		`- result.operands().swap(op);`
	`376`	`+ result.operands() = op;`
`381`	`377`	`return result;`
`382`	`378`	`}`
`383`	`379`	`}`
`384`	`380`
`385`		`-exprt smt2_parsert::binary_predicate(irep_idt id, exprt::operandst &op)`
	`381`	`+exprt smt2_parsert::binary_predicate(irep_idt id, const exprt::operandst &op)`
`386`	`382`	`{`
`387`	`383`	`if(op.size()!=2)`
`388`	`384`	`{`
`@@ -404,7 +400,7 @@ exprt smt2_parsert::binary_predicate(irep_idt id, exprt::operandst &op)`
`404`	`400`	`}`
`405`	`401`	`}`
`406`	`402`
`407`		`-exprt smt2_parsert::unary(irep_idt id, exprt::operandst &op)`
	`403`	`+exprt smt2_parsert::unary(irep_idt id, const exprt::operandst &op)`
`408`	`404`	`{`
`409`	`405`	`if(op.size()!=1)`
`410`	`406`	`{`
`@@ -415,7 +411,7 @@ exprt smt2_parsert::unary(irep_idt id, exprt::operandst &op)`
`415`	`411`	`return unary_exprt(id, op[0], op[0].type());`
`416`	`412`	`}`
`417`	`413`
`418`		`-exprt smt2_parsert::binary(irep_idt id, exprt::operandst &op)`
	`414`	`+exprt smt2_parsert::binary(irep_idt id, const exprt::operandst &op)`
`419`	`415`	`{`
`420`	`416`	`if(op.size()!=2)`
`421`	`417`	`{`
`@@ -510,45 +506,35 @@ exprt smt2_parsert::function_application()`
`510`	`506`	`}`
`511`	`507`	`else if(id=="bvsle")`
`512`	`508`	`{`
`513`		`- op[0]=cast_bv_to_signed(op[0]);`
`514`		`- op[1]=cast_bv_to_signed(op[1]);`
`515`		`- return binary_predicate(ID_le, op);`
	`509`	`+ return binary_predicate(ID_le, cast_bv_to_signed(op));`
`516`	`510`	`}`
`517`	`511`	`else if(id=="bvuge")`
`518`	`512`	`{`
`519`	`513`	`return binary_predicate(ID_ge, op);`
`520`	`514`	`}`
`521`	`515`	`else if(id=="bvsge")`
`522`	`516`	`{`
`523`		`- op[0]=cast_bv_to_signed(op[0]);`
`524`		`- op[1]=cast_bv_to_signed(op[1]);`
`525`		`- return binary_predicate(ID_ge, op);`
	`517`	`+ return binary_predicate(ID_ge, cast_bv_to_signed(op));`
`526`	`518`	`}`
`527`	`519`	`else if(id=="bvult")`
`528`	`520`	`{`
`529`	`521`	`return binary_predicate(ID_lt, op);`
`530`	`522`	`}`
`531`	`523`	`else if(id=="bvslt")`
`532`	`524`	`{`
`533`		`- op[0]=cast_bv_to_signed(op[0]);`
`534`		`- op[1]=cast_bv_to_signed(op[1]);`
`535`		`- return binary_predicate(ID_lt, op);`
	`525`	`+ return binary_predicate(ID_lt, cast_bv_to_signed(op));`
`536`	`526`	`}`
`537`	`527`	`else if(id=="bvugt")`
`538`	`528`	`{`
`539`	`529`	`return binary_predicate(ID_gt, op);`
`540`	`530`	`}`
`541`	`531`	`else if(id=="bvsgt")`
`542`	`532`	`{`
`543`		`- op[0]=cast_bv_to_signed(op[0]);`
`544`		`- op[1]=cast_bv_to_signed(op[1]);`
`545`		`- return binary_predicate(ID_gt, op);`
	`533`	`+ return binary_predicate(ID_gt, cast_bv_to_signed(op));`
`546`	`534`	`}`
`547`	`535`	`else if(id=="bvashr")`
`548`	`536`	`{`
`549`		`- op[0]=cast_bv_to_signed(op[0]);`
`550`		`- op[1]=cast_bv_to_signed(op[1]);`
`551`		`- return cast_bv_to_unsigned(binary(ID_ashr, op));`
	`537`	`+ return cast_bv_to_unsigned(binary(ID_ashr, cast_bv_to_signed(op)));`
`552`	`538`	`}`
`553`	`539`	`else if(id=="bvlshr" \|\| id=="bvshr")`
`554`	`540`	`{`
`@@ -608,9 +594,7 @@ exprt smt2_parsert::function_application()`
`608`	`594`	`}`
`609`	`595`	`else if(id=="bvsdiv")`
`610`	`596`	`{`
`611`		`- op[0]=cast_bv_to_signed(op[0]);`
`612`		`- op[1]=cast_bv_to_signed(op[1]);`
`613`		`- return cast_bv_to_unsigned(binary(ID_div, op));`
	`597`	`+ return cast_bv_to_unsigned(binary(ID_div, cast_bv_to_signed(op)));`
`614`	`598`	`}`
`615`	`599`	`else if(id=="bvudiv")`
`616`	`600`	`{`
`@@ -624,17 +608,13 @@ exprt smt2_parsert::function_application()`
`624`	`608`	`{`
`625`	`609`	`// 2's complement signed remainder (sign follows dividend)`
`626`	`610`	`// This matches our ID_mod, and what C does since C99.`
`627`		`- op[0]=cast_bv_to_signed(op[0]);`
`628`		`- op[1]=cast_bv_to_signed(op[1]);`
`629`		`- return cast_bv_to_unsigned(binary(ID_mod, op));`
	`611`	`+ return cast_bv_to_unsigned(binary(ID_mod, cast_bv_to_signed(op)));`
`630`	`612`	`}`
`631`	`613`	`else if(id=="bvsmod")`
`632`	`614`	`{`
`633`	`615`	`// 2's complement signed remainder (sign follows divisor)`
`634`	`616`	`// We don't have that.`
`635`		`- op[0]=cast_bv_to_signed(op[0]);`
`636`		`- op[1]=cast_bv_to_signed(op[1]);`
`637`		`- return cast_bv_to_unsigned(binary(ID_mod, op));`
	`617`	`+ return cast_bv_to_unsigned(binary(ID_mod, cast_bv_to_signed(op)));`
`638`	`618`	`}`
`639`	`619`	`else if(id=="bvurem" \|\| id=="%")`
`640`	`620`	`{`