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 <limits>
15 #include <numeric>
16 #include <sstream>
17 #include <string>
18 
19 #include <ansi-c/expr2c_class.h>
20 
21 class expr2javat:public expr2ct
22 {
23 public:
24  explicit expr2javat(const namespacet &_ns):expr2ct(_ns) { }
25  virtual std::string convert(const typet &src) override;
26  virtual std::string convert(const exprt &src) override;
27 
28 protected:
29  virtual std::string convert_with_precedence(
30  const exprt &src, unsigned &precedence) override;
31  std::string convert_java_this();
32  std::string convert_java_instanceof(const exprt &src);
33  std::string convert_java_new(const exprt &src);
34  std::string convert_code_java_new(const exprt &src, unsigned precedence);
35  std::string convert_code_java_delete(const exprt &src, unsigned precedence);
36  virtual std::string convert_struct(
37  const exprt &src, unsigned &precedence) override;
38  virtual std::string convert_code(const codet &src, unsigned indent) override;
39  virtual std::string convert_constant(
40  const constant_exprt &src, unsigned &precedence) override;
41  // Hides base class version
42  std::string convert_code_function_call(
43  const code_function_callt &src, unsigned indent);
44 
45  virtual std::string convert_rec(
46  const typet &src,
47  const qualifierst &qualifiers,
48  const std::string &declarator) override;
49 
50  // length of string representation of Java Char
51  // representation is '\u0000'
52  const std::size_t char_representation_length=8;
53 };
54 
55 std::string expr2java(const exprt &expr, const namespacet &ns);
56 std::string type2java(const typet &type, const namespacet &ns);
57 
61 template <typename float_type>
63 {
64  const bool is_float = std::is_same<float_type, float>::value;
65  const std::string class_name = is_float ? "Float" : "Double";
66  if(std::isnan(value))
67  return class_name + ".NaN";
68  if(std::isinf(value) && value >= 0.)
69  return class_name + ".POSITIVE_INFINITY";
70  if(std::isinf(value) && value <= 0.)
71  return class_name + ".NEGATIVE_INFINITY";
72  const std::string decimal = [&]() -> std::string {
73  // Using ostringstream instead of to_string to get string without
74  // trailing zeros
75  std::ostringstream raw_stream;
76  raw_stream << value;
77  const auto raw_decimal = raw_stream.str();
78  const bool is_scientific = raw_decimal.find('e') != std::string::npos;
79  if(
80  raw_decimal.find('.') == std::string::npos &&
81  !is_scientific) // don't add trailing .0 if in scientific notation
82  {
83  return raw_decimal + ".0";
84  }
85  return raw_decimal;
86  }();
87  const bool is_lossless = [&] {
88  try
89  {
90  return std::stod(decimal) == value;
91  }
92  catch(std::out_of_range &)
93  {
94  return false;
95  }
96  }();
97  const std::string lossless = [&]() -> std::string {
98  if(is_lossless)
99  return decimal;
100  std::ostringstream stream;
101  stream << std::hexfloat << value;
102  return stream.str();
103  }();
104  const auto literal = is_float ? lossless + 'f' : lossless;
105  if(is_lossless)
106  return literal;
107  return literal + " /* " + decimal + " */";
108 }
109 
110 #endif // CPROVER_JAVA_BYTECODE_EXPR2JAVA_H
expr2javat::convert_java_new
std::string convert_java_new(const exprt &src)
Definition: expr2java.cpp:335
expr2javat::convert_java_this
std::string convert_java_this()
Definition: expr2java.cpp:317
type2java
std::string type2java(const typet &type, const namespacet &ns)
Definition: expr2java.cpp:462
typet
The type of an expression, extends irept.
Definition: type.h:29
expr2javat::convert
virtual std::string convert(const typet &src) override
Definition: expr2java.cpp:30
exprt
Base class for all expressions.
Definition: expr.h:53
qualifierst
Definition: c_qualifiers.h:19
expr2javat::convert_java_instanceof
std::string convert_java_instanceof(const exprt &src)
Definition: expr2java.cpp:322
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:92
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
expr2ct
Definition: expr2c_class.h:28
expr2javat::expr2javat
expr2javat(const namespacet &_ns)
Definition: expr2java.h:24
expr2javat::convert_code_function_call
std::string convert_code_function_call(const code_function_callt &src, unsigned indent)
Definition: expr2java.cpp:40
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:244
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:62
expr2javat
Definition: expr2java.h:22
expr2javat::convert_constant
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence) override
Definition: expr2java.cpp:170
expr2javat::convert_struct
virtual std::string convert_struct(const exprt &src, unsigned &precedence) override
Definition: expr2java.cpp:109
expr2javat::convert_code
virtual std::string convert_code(const codet &src, unsigned indent) override
Definition: expr2java.cpp:439
expr2java
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:455
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
expr2javat::char_representation_length
const std::size_t char_representation_length
Definition: expr2java.h:52
expr2javat::convert_code_java_new
std::string convert_code_java_new(const exprt &src, unsigned precedence)
Definition: expr2java.cpp:330
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35