cprover
expr2java.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_JAVA_BYTECODE_EXPR2JAVA_H
11 #define CPROVER_JAVA_BYTECODE_EXPR2JAVA_H
12 
13 #include <cmath>
14 #include <numeric>
15 #include <sstream>
16 #include <string>
17 #include <ansi-c/expr2c_class.h>
18 
19 class expr2javat:public expr2ct
20 {
21 public:
22  explicit expr2javat(const namespacet &_ns):expr2ct(_ns) { }
23  virtual std::string convert(const typet &src) override;
24  virtual std::string convert(const exprt &src) override;
25 
26 protected:
27  virtual std::string convert_with_precedence(
28  const exprt &src, unsigned &precedence) override;
29  std::string convert_java_this(const exprt &src, unsigned precedence);
30  std::string convert_java_instanceof(const exprt &src, unsigned precedence);
31  std::string convert_java_new(const exprt &src, unsigned precedence);
32  std::string convert_code_java_delete(const exprt &src, unsigned precedence);
33  virtual std::string convert_struct(
34  const exprt &src, unsigned &precedence) override;
35  virtual std::string convert_code(const codet &src, unsigned indent) override;
36  virtual std::string convert_constant(
37  const constant_exprt &src, unsigned &precedence) override;
38  // Hides base class version
39  std::string convert_code_function_call(
40  const code_function_callt &src, unsigned indent);
41 
42  virtual std::string convert_rec(
43  const typet &src,
44  const qualifierst &qualifiers,
45  const std::string &declarator) override;
46 
47  // length of string representation of Java Char
48  // representation is '\u0000'
49  const std::size_t char_representation_length=8;
50 };
51 
52 std::string expr2java(const exprt &expr, const namespacet &ns);
53 std::string type2java(const typet &type, const namespacet &ns);
54 
58 template <typename float_type>
60 {
61  const bool is_float = std::is_same<float_type, float>::value;
62  const std::string class_name = is_float ? "Float" : "Double";
63  if(std::isnan(value))
64  return class_name + ".NaN";
65  if(std::isinf(value) && value >= 0.)
66  return class_name + ".POSITIVE_INFINITY";
67  if(std::isinf(value) && value <= 0.)
68  return class_name + ".NEGATIVE_INFINITY";
69  const std::string decimal = [&]() -> std::string {
70  // Using ostringstream instead of to_string to get string without
71  // trailing zeros
72  std::ostringstream raw_stream;
73  raw_stream << value;
74  const auto raw_decimal = raw_stream.str();
75  if(raw_decimal.find('.') == std::string::npos)
76  return raw_decimal + ".0";
77  return raw_decimal;
78  }();
79  const bool is_lossless = [&] {
80  if(value == std::numeric_limits<float_type>::min())
81  return true;
82  try
83  {
84  return std::stod(decimal) == value;
85  }
86  catch(std::out_of_range &)
87  {
88  return false;
89  }
90  }();
91  const std::string lossless = [&]() -> std::string {
92  if(is_lossless)
93  return decimal;
94  std::ostringstream stream;
95  stream << std::hexfloat << value;
96  return stream.str();
97  }();
98  const auto literal = is_float ? lossless + 'f' : lossless;
99  if(is_lossless)
100  return literal;
101  return literal + " /* " + decimal + " */";
102 }
103 
104 #endif // CPROVER_JAVA_BYTECODE_EXPR2JAVA_H
type2java
std::string type2java(const typet &type, const namespacet &ns)
Definition: expr2java.cpp:448
typet
The type of an expression, extends irept.
Definition: type.h:27
expr2javat::convert
virtual std::string convert(const typet &src) override
Definition: expr2java.cpp:28
exprt
Base class for all expressions.
Definition: expr.h:54
expr2javat::convert_java_this
std::string convert_java_this(const exprt &src, unsigned precedence)
Definition: expr2java.cpp:313
qualifierst
Definition: c_qualifiers.h:18
expr2javat::convert_with_precedence
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence) override
Definition: expr2java.cpp:378
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1036
expr2ct
Definition: expr2c_class.h:25
expr2javat::expr2javat
expr2javat(const namespacet &_ns)
Definition: expr2java.h:22
expr2javat::convert_java_new
std::string convert_java_new(const exprt &src, unsigned precedence)
Definition: expr2java.cpp:333
expr2javat::convert_code_function_call
std::string convert_code_function_call(const code_function_callt &src, unsigned indent)
Definition: expr2java.cpp:38
float_type
floatbv_typet float_type()
Definition: c_types.cpp:185
expr2javat::convert_rec
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator) override
Definition: expr2java.cpp:239
expr2c_class.h
expr2javat::convert_code_java_delete
std::string convert_code_java_delete(const exprt &src, unsigned precedence)
Definition: expr2java.cpp:359
floating_point_to_java_string
std::string floating_point_to_java_string(float_type value)
Convert floating point number to a string without printing unnecessary zeros.
Definition: expr2java.h:59
expr2javat
Definition: expr2java.h:19
expr2javat::convert_constant
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence) override
Definition: expr2java.cpp:165
expr2javat::convert_struct
virtual std::string convert_struct(const exprt &src, unsigned &precedence) override
Definition: expr2java.cpp:107
expr2javat::convert_code
virtual std::string convert_code(const codet &src, unsigned indent) override
Definition: expr2java.cpp:425
expr2javat::convert_java_instanceof
std::string convert_java_instanceof(const exprt &src, unsigned precedence)
Definition: expr2java.cpp:320
expr2java
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:441
constant_exprt
A constant literal expression.
Definition: std_expr.h:4384
expr2javat::char_representation_length
const std::size_t char_representation_length
Definition: expr2java.h:49
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34