Skip to content

Commit

Permalink
Generic backward transfer function for invertible operations
Browse files Browse the repository at this point in the history
  • Loading branch information
@caballa
caballa committed Jun 9, 2019
1 parent 4527844 commit 1fe7b1b
Showing 1 changed file with 81 additions and 77 deletions.
158 changes: 81 additions & 77 deletions include/crab/domains/backward_assign_operations.hpp
View file
Original file line number Diff line number Diff line change
@@ -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.
**/


Expand All @@ -16,7 +18,7 @@
namespace crab {
namespace domains {

template <class AbsDom>
template<class AbsDom>
class BackwardAssignOps {
public:
typedef typename AbsDom::number_t number_t;
Expand All @@ -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<variable_t,variable_t> 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;
Expand All @@ -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");
Expand All @@ -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()) {
Expand All @@ -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");
}
};
Expand Down

0 comments on commit 1fe7b1b

Please sign in to comment.