ai_domain.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Abstract Interpretation
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#include "ai_domain.h"
 
#include <util/pointer_expr.h>
#include <util/simplify_expr.h>
 
jsont ai_domain_baset::output_json(const ai_baset &ai, const namespacet &ns)
  const
{
  std::ostringstream out;
  output(out, ai, ns);
  json_stringt json(out.str());
  return std::move(json);
}
 
xmlt ai_domain_baset::output_xml(const ai_baset &ai, const namespacet &ns) const
{
  std::ostringstream out;
  output(out, ai, ns);
  xmlt xml("abstract_state");
  xml.data = out.str();
  return xml;
}
 
bool ai_domain_baset::ai_simplify_lhs(exprt &condition, const namespacet &ns)
  const
{
  // Care must be taken here to give something that is still writable
  if(condition.id() == ID_index)
  {
    index_exprt ie = to_index_expr(condition);
    bool no_simplification = ai_simplify(ie.index(), ns);
    if(!no_simplification)
      condition = simplify_expr(std::move(ie), ns);
 
    return no_simplification;
  }
  else if(condition.id() == ID_dereference)
  {
    dereference_exprt de = to_dereference_expr(condition);
    bool no_simplification = ai_simplify(de.pointer(), ns);
    if(!no_simplification)
      condition = simplify_expr(std::move(de), ns); // So *(&x) -> x
 
    return no_simplification;
  }
  else if(condition.id() == ID_member)
  {
    member_exprt me = to_member_expr(condition);
    // Since simplify_ai_lhs is required to return an addressable object
    // (so remains a valid left hand side), to simplify
    // `(something_simplifiable).b` we require that `something_simplifiable`
    // must also be addressable
    bool no_simplification = ai_simplify_lhs(me.compound(), ns);
    if(!no_simplification)
      condition = simplify_expr(std::move(me), ns);
 
    return no_simplification;
  }
  else
    return true;
}