/*******************************************************************\

Module: C++ Language Module

Author: Daniel Kroening, kroening@cs.cmu.edu

\*******************************************************************/

/// \file

/// C++ Language Module

#include "cpp_type2name.h"

#include <string>

#include <util/cprover_prefix.h>

#include <util/pointer_expr.h>

#include <util/type.h>

static std::string do_prefix(const std::string &s)

{

if(s.find(',') != std::string::npos || (!s.empty() && isdigit(s[0])))

return std::to_string(s.size())+"_"+s;

return s;

}

static std::string irep2name(const irept &irep)

{

std::string result;

if(is_reference(static_cast<const typet&>(irep)))

result+="reference";

if(is_rvalue_reference(static_cast<const typet &>(irep)))

result += "rvalue_reference";

if(irep.id() == ID_frontend_pointer)

{

if(irep.get_bool(ID_C_reference))

result += "reference";

if(irep.get_bool(ID_C_rvalue_reference))

result += "rvalue_reference";

}

else if(!irep.id().empty())

result+=do_prefix(irep.id_string());

if(irep.get_named_sub().empty() && irep.get_sub().empty())

return result;

result+='(';

bool first=true;

for(const auto &named_sub : irep.get_named_sub())

{

if(!irept::is_comment(named_sub.first))

{

if(first)

first = false;

else

result += ',';

result += do_prefix(id2string(named_sub.first));

result += '=';

result += irep2name(named_sub.second);

}

}

for(const auto &named_sub : irep.get_named_sub())

{

if(

named_sub.first == ID_C_constant || named_sub.first == ID_C_volatile ||

named_sub.first == ID_C_restricted)

{

if(first)

first=false;

else

result+=',';

result += do_prefix(id2string(named_sub.first));

result+='=';

result += irep2name(named_sub.second);

}

}

for(const auto &sub : irep.get_sub())

{

if(first)

first=false;

else

result+=',';

result += irep2name(sub);

}

result+=')';

return result;

}

std::string cpp_type2name(const typet &type)

{

std::string result;

if(type.get_bool(ID_C_constant))

result+="const_";

if(type.get_bool(ID_C_restricted))

result+="restricted_";

if(type.get_bool(ID_C_volatile))

result+="volatile_";

if(type.id()==ID_empty || type.id()==ID_void)

result+="void";

else if(type.id() == ID_c_bool)

result+="bool";

else if(type.id() == ID_bool)

result += CPROVER_PREFIX "bool";

else if(type.id()==ID_pointer)

{

if(is_reference(type))

result += "ref_" + cpp_type2name(to_reference_type(type).base_type());

else if(is_rvalue_reference(type))

result += "rref_" + cpp_type2name(to_pointer_type(type).base_type());

else

result += "ptr_" + cpp_type2name(to_pointer_type(type).base_type());

}

else if(type.id()==ID_signedbv || type.id()==ID_unsignedbv)

{

// we try to use #c_type

const irep_idt c_type=type.get(ID_C_c_type);

if(!c_type.empty())

result+=id2string(c_type);

else if(type.id()==ID_unsignedbv)

result+="unsigned_int";

else

result+="signed_int";

}

else if(type.id()==ID_fixedbv || type.id()==ID_floatbv)

{

// we try to use #c_type

const irep_idt c_type=type.get(ID_C_c_type);

if(!c_type.empty())

result+=id2string(c_type);

else

result+="double";

}

else if(type.id()==ID_code)

{

// we do (args)->(return_type)

const code_typet::parameterst &parameters=to_code_type(type).parameters();

const typet &return_type=to_code_type(type).return_type();

result+='(';

for(code_typet::parameterst::const_iterator

arg_it=parameters.begin();

arg_it!=parameters.end();

arg_it++)

{

if(arg_it!=parameters.begin())

result+=',';

result+=cpp_type2name(arg_it->type());

}

result+=')';

result+="->(";

result+=cpp_type2name(return_type);

result+=')';

}

else

{

// give up

return irep2name(type);

}

return result;

}

std::string cpp_expr2name(const exprt &expr)

{

return irep2name(expr);

}