Skip to content

Commit 08487ad

Browse files
peterschrammelpeterschrammel
authored
Merge pull request #634 from smowton/sss_pretty_printing
Add simple pretty-printer extension mechanism
2 parents ebf7b78 + ff0f281 commit 08487ad

19 files changed

+412
-83
lines changed

‎src/ansi-c/ansi_c_language.cpp‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
2121
#include "ansi_c_typecheck.h"
2222
#include "ansi_c_parser.h"
2323
#include "expr2c.h"
24+
#include "expr2c_class.h"
2425
#include "c_preprocess.h"
2526
#include "ansi_c_internal_additions.h"
2627
#include "type2name.h"
@@ -285,6 +286,24 @@ bool ansi_c_languaget::from_type(
285286

286287
/*******************************************************************\
287288
289+
Function: ansi_c_languaget::get_pretty_printer
290+
291+
Inputs:
292+
293+
Outputs:
294+
295+
Purpose:
296+
297+
\*******************************************************************/
298+
299+
std::unique_ptr<pretty_printert>
300+
ansi_c_languaget::get_pretty_printer(const namespacet &ns)
301+
{
302+
return std::unique_ptr<pretty_printert>(new expr2ct(ns));
303+
}
304+
305+
/*******************************************************************\
306+
288307
Function: ansi_c_languaget::type_to_name
289308
290309
Inputs:

‎src/ansi-c/ansi_c_language.h‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -53,6 +53,9 @@ class ansi_c_languaget:public languaget
5353
std::string &code,
5454
const namespacet &ns) override;
5555

56+
std::unique_ptr<pretty_printert>
57+
get_pretty_printer(const namespacet &) override;
58+
5659
bool type_to_name(
5760
const typet &type,
5861
std::string &name,

‎src/ansi-c/expr2c.cpp‎

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -204,6 +204,7 @@ Function: expr2ct::convert
204204

205205
std::string expr2ct::convert(const typet &src)
206206
{
207+
assert(next_pretty_printer && "Next pretty-printer should be set");
207208
return convert_rec(src, c_qualifierst(), "");
208209
}
209210

@@ -679,14 +680,7 @@ std::string expr2ct::convert_rec(
679680
return q+"__attribute__(("+id2string(src.id())+")) void"+d;
680681
}
681682

682-
{
683-
lispexprt lisp;
684-
irep2lisp(src, lisp);
685-
std::string dest="irep(\""+MetaString(lisp.expr2string())+"\")";
686-
dest+=d;
687-
688-
return dest;
689-
}
683+
return next_pretty_printer->convert(src);
690684
}
691685

692686
/*******************************************************************\
@@ -5009,7 +5003,7 @@ std::string expr2ct::convert(
50095003
return convert(src.type());
50105004

50115005
// no C language expression for internal representation
5012-
return convert_norep(src, precedence);
5006+
return next_pretty_printer->convert(src);
50135007
}
50145008

50155009
/*******************************************************************\
@@ -5046,7 +5040,9 @@ std::string expr2c(const exprt &expr, const namespacet &ns)
50465040
{
50475041
std::string code;
50485042
expr2ct expr2c(ns);
5043+
norep_pretty_printert norep;
50495044
expr2c.get_shorthands(expr);
5045+
expr2c.set_next_pretty_printer(&norep);
50505046
return expr2c.convert(expr);
50515047
}
50525048

@@ -5065,6 +5061,8 @@ Function: type2c
50655061
std::string type2c(const typet &type, const namespacet &ns)
50665062
{
50675063
expr2ct expr2c(ns);
5064+
norep_pretty_printert norep;
5065+
expr2c.set_next_pretty_printer(&norep);
50685066
// expr2c.get_shorthands(expr);
50695067
return expr2c.convert(type);
50705068
}

‎src/ansi-c/expr2c_class.h‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,17 +16,19 @@ Author: Daniel Kroening, kroening@kroening.com
1616
#include <util/std_code.h>
1717
#include <util/std_expr.h>
1818

19+
#include <langapi/pretty_printer.h>
20+
1921
class c_qualifierst;
2022
class namespacet;
2123

22-
class expr2ct
24+
class expr2ct:public pretty_printert
2325
{
2426
public:
2527
explicit expr2ct(const namespacet &_ns):ns(_ns), sizeof_nesting(0) { }
2628
virtual ~expr2ct() { }
2729

28-
virtual std::string convert(const typet &src);
29-
virtual std::string convert(const exprt &src);
30+
std::string convert(const typet &src) override;
31+
std::string convert(const exprt &src) override;
3032

3133
void get_shorthands(const exprt &expr);
3234

‎src/cpp/cpp_language.cpp‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
2222
#include "cpp_internal_additions.h"
2323
#include "cpp_language.h"
2424
#include "expr2cpp.h"
25+
#include "expr2cpp_class.h"
2526
#include "cpp_parser.h"
2627
#include "cpp_typecheck.h"
2728
#include "cpp_type2name.h"
@@ -362,6 +363,24 @@ bool cpp_languaget::from_type(
362363

363364
/*******************************************************************\
364365
366+
Function: cpp_languaget::get_pretty_printer
367+
368+
Inputs:
369+
370+
Outputs:
371+
372+
Purpose:
373+
374+
\*******************************************************************/
375+
376+
std::unique_ptr<pretty_printert>
377+
cpp_languaget::get_pretty_printer(const namespacet &ns)
378+
{
379+
return std::unique_ptr<pretty_printert>(new expr2cppt(ns));
380+
}
381+
382+
/*******************************************************************\
383+
365384
Function: cpp_languaget::type_to_name
366385
367386
Inputs:

‎src/cpp/cpp_language.h‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -62,6 +62,9 @@ class cpp_languaget:public languaget
6262
std::string &code,
6363
const namespacet &ns) override;
6464

65+
std::unique_ptr<pretty_printert>
66+
get_pretty_printer(const namespacet &) override;
67+
6568
bool type_to_name(
6669
const typet &type,
6770
std::string &name,

‎src/cpp/expr2cpp.cpp‎

Lines changed: 5 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -17,44 +17,9 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
1717

1818
#include <ansi-c/c_misc.h>
1919
#include <ansi-c/c_qualifiers.h>
20-
#include <ansi-c/expr2c_class.h>
2120

2221
#include "expr2cpp.h"
23-
24-
class expr2cppt:public expr2ct
25-
{
26-
public:
27-
explicit expr2cppt(const namespacet &_ns):expr2ct(_ns) { }
28-
29-
std::string convert(const exprt &src) override
30-
{
31-
return expr2ct::convert(src);
32-
}
33-
34-
std::string convert(const typet &src) override
35-
{
36-
return expr2ct::convert(src);
37-
}
38-
39-
protected:
40-
std::string convert(const exprt &src, unsigned &precedence) override;
41-
std::string convert_cpp_this(const exprt &src, unsigned precedence);
42-
std::string convert_cpp_new(const exprt &src, unsigned precedence);
43-
std::string convert_extractbit(const exprt &src, unsigned precedence);
44-
std::string convert_extractbits(const exprt &src, unsigned precedence);
45-
std::string convert_code_cpp_delete(const exprt &src, unsigned precedence);
46-
std::string convert_struct(const exprt &src, unsigned &precedence) override;
47-
std::string convert_code(const codet &src, unsigned indent) override;
48-
// NOLINTNEXTLINE(whitespace/line_length)
49-
std::string convert_constant(const constant_exprt &src, unsigned &precedence) override;
50-
51-
std::string convert_rec(
52-
const typet &src,
53-
const c_qualifierst &qualifiers,
54-
const std::string &declarator) override;
55-
56-
typedef std::unordered_set<std::string, string_hash> id_sett;
57-
};
22+
#include "expr2cpp_class.h"
5823

5924
/*******************************************************************\
6025
@@ -647,6 +612,8 @@ std::string expr2cpp(const exprt &expr, const namespacet &ns)
647612
{
648613
expr2cppt expr2cpp(ns);
649614
expr2cpp.get_shorthands(expr);
615+
norep_pretty_printert norep;
616+
expr2cpp.set_next_pretty_printer(&norep);
650617
return expr2cpp.convert(expr);
651618
}
652619

@@ -665,5 +632,7 @@ Function: type2cpp
665632
std::string type2cpp(const typet &type, const namespacet &ns)
666633
{
667634
expr2cppt expr2cpp(ns);
635+
norep_pretty_printert norep;
636+
expr2cpp.set_next_pretty_printer(&norep);
668637
return expr2cpp.convert(type);
669638
}

‎src/cpp/expr2cpp_class.h‎

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
/*******************************************************************\
2+
3+
Module:
4+
5+
Author: Daniel Kroening, kroening@cs.cmu.edu
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_CPP_EXPR2CPP_CLASS_H
10+
#define CPROVER_CPP_EXPR2CPP_CLASS_H
11+
12+
#include <ansi-c/expr2c_class.h>
13+
14+
class expr2cppt:public expr2ct
15+
{
16+
public:
17+
explicit expr2cppt(const namespacet &_ns):expr2ct(_ns) { }
18+
19+
std::string convert(const exprt &src) override
20+
{
21+
return expr2ct::convert(src);
22+
}
23+
24+
std::string convert(const typet &src) override
25+
{
26+
return expr2ct::convert(src);
27+
}
28+
29+
protected:
30+
std::string convert(const exprt &src, unsigned &precedence) override;
31+
std::string convert_cpp_this(const exprt &src, unsigned precedence);
32+
std::string convert_cpp_new(const exprt &src, unsigned precedence);
33+
std::string convert_extractbit(const exprt &src, unsigned precedence);
34+
std::string convert_extractbits(const exprt &src, unsigned precedence);
35+
std::string convert_code_cpp_delete(const exprt &src, unsigned precedence);
36+
std::string convert_struct(const exprt &src, unsigned &precedence) override;
37+
std::string convert_code(const codet &src, unsigned indent) override;
38+
// NOLINTNEXTLINE(whitespace/line_length)
39+
std::string convert_constant(const constant_exprt &src, unsigned &precedence) override;
40+
41+
std::string convert_rec(
42+
const typet &src,
43+
const c_qualifierst &qualifiers,
44+
const std::string &declarator) override;
45+
46+
typedef std::unordered_set<std::string, string_hash> id_sett;
47+
};
48+
49+
#endif

‎src/java_bytecode/expr2java.cpp‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -565,6 +565,8 @@ std::string expr2java(const exprt &expr, const namespacet &ns)
565565
{
566566
expr2javat expr2java(ns);
567567
expr2java.get_shorthands(expr);
568+
norep_pretty_printert norep;
569+
expr2java.set_next_pretty_printer(&norep);
568570
return expr2java.convert(expr);
569571
}
570572

@@ -583,5 +585,7 @@ Function: type2java
583585
std::string type2java(const typet &type, const namespacet &ns)
584586
{
585587
expr2javat expr2java(ns);
588+
norep_pretty_printert norep;
589+
expr2java.set_next_pretty_printer(&norep);
586590
return expr2java.convert(type);
587591
}

‎src/java_bytecode/java_bytecode_language.cpp‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -876,6 +876,24 @@ bool java_bytecode_languaget::from_type(
876876

877877
/*******************************************************************\
878878
879+
Function: java_bytecode_languaget::get_pretty_printer
880+
881+
Inputs:
882+
883+
Outputs:
884+
885+
Purpose:
886+
887+
\*******************************************************************/
888+
889+
std::unique_ptr<pretty_printert>
890+
java_bytecode_languaget::get_pretty_printer(const namespacet &ns)
891+
{
892+
return std::unique_ptr<pretty_printert>(new expr2javat(ns));
893+
}
894+
895+
/*******************************************************************\
896+
879897
Function: java_bytecode_languaget::to_expr
880898
881899
Inputs:

0 commit comments

Comments
 (0)