Skip to content

Upstreaming expr2cleanct #2704

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
76 changes: 76 additions & 0 deletions src/ansi-c/expr2cleanc.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,76 @@
/*******************************************************************\

Module:

Author: Daniel Kroening, [email protected]

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

/// \file
/// expr2cleanct

#include "expr2cleanc.h"
#include <ansi-c/c_qualifiers.h>

/// To convert a type in to ANSI-C but with the identifier in place.
/// This is useful for array types where the identifier is inside the type
/// \param src: the type to convert6
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

convert

/// \param identifier: the identifier to use as the type
/// \return A C declaration of the given type with the right identifier.
std::string expr2cleanct::convert_with_identifier(
const typet &src,
const std::string &identifier)
{
return convert_rec(src, c_qualifierst(), identifier);
}

/// To produce C code for assigning a struct. The clean version removes padding
/// variables.
/// \param src: The struct expression being converted
/// \param precedence
/// \return C assignment of a struct
std::string expr2cleanct::convert_struct(const exprt &src, unsigned &precedence)
{
// Generate the normal struct code except we exclude padding members
return expr2ct::convert_struct(src, precedence, false);
}

/// To produce a C type declaration for a given struct.
/// The clean version removes padding and redefining the struct in line.
/// \param src: The struct type being converted
/// \param qualifer_str: Type qualifiers
/// \param declarator_str: Type declarators
/// \return C type declaration for struct
std::string expr2cleanct::convert_struct_type(
const typet &src,
const std::string &qualifer_str,
const std::string &declarator_str)
{
// Disable including the body of the struct when getting the type
return expr2ct::convert_struct_type(
src, qualifer_str, declarator_str, false, false);
}

/// To produce a C type declaration for a given array.
/// The clean version removes specifying the size of the array
/// \param src: The array type being converted
/// \param qualifiers: Type qualifiers
/// \param declarator_str: Type declarators
/// \return C type declaration for an array
std::string expr2cleanct::convert_array_type(
const typet &src,
const qualifierst &qualifiers,
const std::string &declarator_str)
{
return expr2ct::convert_array_type(src, qualifiers, declarator_str, false);
}

/// Output C code for a boolean literal. Clean version uses 1 and 0, otherwise
/// requires additional includes.
/// \param boolean_value: The boolean value to convert
/// \return C code for representing a true or false value
std::string expr2cleanct::convert_constant_bool(bool boolean_value)
{
// This requires #include <stdbool.h>
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In the generated class, or in this class?
If this comments aims on the generated class, why do you need this in the generated class, if using 0 and 1?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You're quite right - this comment was from when this uses true and false - I'll update

return boolean_value?"1":"0";
}
50 changes: 50 additions & 0 deletions src/ansi-c/expr2cleanc.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,50 @@
/*******************************************************************\

Module:

Author: Daniel Kroening, [email protected]

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

/// \file
/// expr2cleanct

#ifndef CPROVER_ANSI_C_EXPR2CLEANC_H
#define CPROVER_ANSI_C_EXPR2CLEANC_H

#include "expr2c_class.h"

#include <string>

/// Produces C from expression and types.
/// It does not print padding components in structs
/// It does not print array sizes when printing array types
/// It does not print the body of the struct when printing the struct type
class expr2cleanct:public expr2ct
Copy link
Member

@peterschrammel peterschrammel Aug 9, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't see much value in having this as a separate class. I'd prefer to see the behaviour of expr2ct be made configurable if necessary.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Did you see this branch: https://github.com/thk123/cbmc/tree/dump/expr2c-configuration. It gets complicated as TG uses a broader interface than just expr2c/type2c so the options are:

  1. rework TG to use the regular interface (probably at least a couple of days)
  2. add an extra method in expr2c.h for this extra route (half day?)
  3. just add the extra method to expr2ct and use the class directly (quickest - but I think have the class defined in a separate header is supposed to indicate it isn't part of the public interface so feels like the worst option)

I'll have a look at the second one unless you think the third one is acceptable?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have had a brief look at the configuration branch and really liked it! Given my limited insight: can you briefly explain what this "broader interface" is that TG uses/requires? Looking at dump-c, this work will help simplify its code a lot, which of course I'll take on once any approach here is merged. I do suspect that TG may have similar pieces of code?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I missed that one. Yes, @thk123, that's what I had envisaged.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wound up being relatively straight forward: #2713

{
public:
explicit expr2cleanct(const namespacet &ns)
: expr2ct(ns)
{}

std::string convert_with_identifier(
const typet &src, const std::string &identifier);

protected:
std::string convert_struct(
const exprt &src, unsigned &precedence) override;

std::string convert_struct_type(
const typet &src,
const std::string &qualifer_str,
const std::string &declarator_str) override;

std::string convert_array_type(
const typet &src,
const qualifierst &qualifiers,
const std::string &declarator_str) override;

std::string convert_constant_bool(bool boolean_value) override;
};

#endif // CPROVER_ANSI_C_EXPR2CLEANC_H