From 1fe7b1be796318da0f93b7016673c8a049ea01f4 Mon Sep 17 00:00:00 2001 From: caballa Date: Sun, 9 Jun 2019 13:18:45 -0700 Subject: [PATCH] Generic backward transfer function for invertible operations --- .../domains/backward_assign_operations.hpp | 158 +++++++++--------- 1 file changed, 81 insertions(+), 77 deletions(-) diff --git a/include/crab/domains/backward_assign_operations.hpp b/include/crab/domains/backward_assign_operations.hpp index 8568b125..c30b8897 100644 --- a/include/crab/domains/backward_assign_operations.hpp +++ b/include/crab/domains/backward_assign_operations.hpp @@ -1,9 +1,11 @@ #pragma once /** - * Implement generic backward assignments. Unless the assignment is - * invertible the result is an over-approximation so we need to adapt - * these operations in case we need under-approximations. + * Implement generic backward assignments. + * + * Be aware that unless the assignment is invertible the result is an + * over-approximation so we need to adapt these operations in case we + * need under-approximations. **/ @@ -16,7 +18,7 @@ namespace crab { namespace domains { - template + template class BackwardAssignOps { public: typedef typename AbsDom::number_t number_t; @@ -27,36 +29,44 @@ namespace crab { /* * Backward x := e - * case 1: if e is invertible + * + * General case: + * if x does not appear in e + * 1) add constraint x = e + * 2) forget x + * else + * 1) add new variable x' + * 2) add constraint x = e[x'/x] + * 3) forget x + * 4) rename x' as x + * + * Invertible operation (y can be equal to x): * x = y + k <--> y = x - k * x = y - k <--> y = x + k * x = y * k <--> y = x / k if (k != 0) * x = y / k <--> y = x * k if (k != 0) - * case 2: if x does not appear in e - * 1) add constraint x = e - * 2) forget x - * case 3: if x appears in e - * TODO: - * This is a just a general recipe. Better to implement a more - * precise transformer inside the domain. - * 1) add new variable x' - * 1) add constraint x = e[x'/x] - * 3) forget x - * 4) rename x' as x + * + * Fallback case: + * forget(x) **/ // x := e - // pre: dom is not bottom static void assign(AbsDom& dom, variable_t x, linear_expression_t e, AbsDom inv) { - crab::CrabStats::count (AbsDom::getDomainName() + ".count.backward_assign"); + crab::CrabStats::count(AbsDom::getDomainName() + ".count.backward_assign"); crab::ScopedCrabStats __st__(AbsDom::getDomainName() + ".backward_assign"); if(dom.is_bottom()) return; if (e.variables() >= x) { - CRAB_WARN("backwards x:=e when x appears in e not implemented"); + auto& vfac = x.name().get_var_factory(); + variable_t old_x(vfac.get(x.index()), x.get_type()); + std::map renaming_map; + renaming_map.insert({x, old_x}); + linear_expression_t renamed_e = e.rename(renaming_map); + dom += linear_constraint_t(renamed_e - x, linear_constraint_t::EQUALITY); dom -= x; + dom.rename({old_x}, {x}); } else { dom += linear_constraint_t(e - x, linear_constraint_t::EQUALITY); dom -= x; @@ -65,58 +75,60 @@ namespace crab { } // x := y op k - // pre: dom is not bottom static void apply(AbsDom& dom, operation_t op, variable_t x, variable_t y, number_t k, AbsDom inv) { - crab::CrabStats::count (AbsDom::getDomainName() + ".count.backward_apply"); + crab::CrabStats::count(AbsDom::getDomainName() + ".count.backward_apply"); crab::ScopedCrabStats __st__(AbsDom::getDomainName() + ".backward_apply"); if(dom.is_bottom()) { return; } - + CRAB_LOG("backward", crab::outs() << x << ":=" << y << " " << op << " " << k << "\n" << "BEFORE " << dom << "\n";); - - if (x == y) { - CRAB_WARN("backwards x:=e when x appears in e not implemented"); - dom -= x; - } else { - switch(op) { - case OP_ADDITION: - dom.apply(OP_SUBTRACTION, y, x, k); - dom -= x; - break; - case OP_SUBTRACTION: - dom.apply(OP_ADDITION, y, x, k); + + switch(op) { + case OP_ADDITION: + dom.apply(OP_SUBTRACTION, y, x, k); + if (!(x == y)) { dom -= x; - break; - case OP_MULTIPLICATION: - if(k != 0) { - dom.apply(OP_SDIV, y, x, k); - } else { - CRAB_WARN("backwards x:= y * k is not invertible"); + } + break; + case OP_SUBTRACTION: + dom.apply(OP_ADDITION, y, x, k); + if (!(x == y)) { + dom -= x; + } + break; + case OP_MULTIPLICATION: + if(k != 0) { + dom.apply(OP_SDIV, y, x, k); + if (!(x == y)) { dom -= x; } - break; - case OP_SDIV: - if(k != 0) { - dom.apply(OP_MULTIPLICATION, y, x, k); - } else { - CRAB_WARN("backwards x:= y / k is not invertible"); + } else { + dom -= x; + } + break; + case OP_SDIV: + if(k != 0) { + dom.apply(OP_MULTIPLICATION, y, x, k); + if (!(x == y)) { dom -= x; } - break; - case OP_UDIV: - case OP_SREM: - case OP_UREM: - default: - CRAB_WARN("backwards x:= y ", op, " k is not implemented"); + } else { dom -= x; } + break; + case OP_UDIV: + case OP_SREM: + case OP_UREM: + default: + CRAB_WARN("backwards x:= y ", op, " k is not implemented"); + dom -= x; } - + dom = dom & inv; CRAB_LOG("backward", crab::outs()<< "AFTER " << dom << "\n"); @@ -127,7 +139,7 @@ namespace crab { static void apply(AbsDom& dom, operation_t op, variable_t x, variable_t y, variable_t z, AbsDom inv) { - crab::CrabStats::count (AbsDom::getDomainName() + ".count.backward_apply"); + crab::CrabStats::count(AbsDom::getDomainName() + ".count.backward_apply"); crab::ScopedCrabStats __st__(AbsDom::getDomainName() + ".backward_apply"); if(dom.is_bottom()) { @@ -138,31 +150,23 @@ namespace crab { crab::outs() << x << ":=" << y << " " << op << " " << z << "\n" << "BEFORE " << dom << "\n";); - if (x == y || x == z) { - CRAB_WARN("backwards x:=e when x appears in e not implemented"); - dom -= x; - } else { - switch(op) { - case OP_ADDITION: - dom += linear_constraint_t(y + z - x, linear_constraint_t::EQUALITY); - dom -= x; - break; - case OP_SUBTRACTION: - dom += linear_constraint_t(y - z - x, linear_constraint_t::EQUALITY); - dom -= x; - break; - case OP_MULTIPLICATION: - case OP_SDIV: - case OP_UDIV: - case OP_SREM: - case OP_UREM: - CRAB_WARN("backwards x = y ", op, " z not implemented"); - dom -= x; - break; - } + switch(op) { + case OP_ADDITION: + assign(dom, x, linear_expression_t(y+z), inv); + break; + case OP_SUBTRACTION: + assign(dom, x, linear_expression_t(y-z), inv); + break; + case OP_MULTIPLICATION: + case OP_SDIV: + case OP_UDIV: + case OP_SREM: + case OP_UREM: + CRAB_WARN("backwards x = y ", op, " z not implemented"); + dom -= x; + break; } dom = dom & inv; - CRAB_LOG("backward", crab::outs()<< "AFTER " << dom << "\n"); } };