Skip to content

Commit 6ee12f0

Browse files
peterschrammelpeterschrammel
committed
Call expr/type to json via languaget
1 parent 975d19d commit 6ee12f0

File tree

10 files changed

+298
-175
lines changed

10 files changed

+298
-175
lines changed

‎src/cbmc/bmc_cover.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -384,7 +384,7 @@ bool bmc_covert::operator()()
384384
json_input["id"]=json_stringt(id2string(step.io_id));
385385
if(step.io_args.size()==1)
386386
json_input["value"]=
387-
json(step.io_args.front(), bmc.ns, ID_unknown);
387+
json(bmc.ns, step.pc->function, step.io_args.front());
388388
json_test.push_back(json_input);
389389
}
390390
}

‎src/goto-programs/json_goto_trace.cpp

+11-30
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ Author: Daniel Kroening
2020
#include <util/simplify_expr.h>
2121

2222
#include <langapi/language_util.h>
23+
#include <langapi/mode.h>
2324
#include <util/json_irep.h>
2425

2526
/// Produce a json representation of a trace.
@@ -90,7 +91,6 @@ void convert(
9091
json_assignment["sourceLocation"]=json_location;
9192

9293
std::string value_string, binary_string, type_string, full_lhs_string;
93-
json_objectt full_lhs_value;
9494

9595
DATA_INVARIANT(
9696
step.full_lhs.is_not_nil(),
@@ -132,27 +132,18 @@ void convert(
132132
const symbolt *symbol;
133133
irep_idt base_name, display_name;
134134

135+
135136
if(!ns.lookup(identifier, symbol))
136137
{
137138
base_name=symbol->base_name;
138139
display_name=symbol->display_name();
139-
if(type_string=="")
140-
type_string=from_type(ns, identifier, symbol->type);
140+
type_string = from_type(ns, identifier, symbol->type);
141141

142142
json_assignment["mode"]=json_stringt(id2string(symbol->mode));
143-
exprt simplified=simplify_expr(step.full_lhs_value, ns);
144-
145-
full_lhs_value=json(simplified, ns, symbol->mode);
146-
}
147-
else
148-
{
149-
DATA_INVARIANT(
150-
step.full_lhs_value.is_not_nil(),
151-
"full_lhs_value in assignment must not be nil");
152-
full_lhs_value=json(step.full_lhs_value, ns, ID_unknown);
153143
}
154144

155-
json_assignment["value"]=full_lhs_value;
145+
const exprt value_simplified = simplify_expr(step.full_lhs_value, ns);
146+
json_assignment["value"] = json(ns, identifier, value_simplified);
156147
json_assignment["lhs"]=json_stringt(full_lhs_string);
157148
if(trace_options.json_full_lhs)
158149
{
@@ -184,13 +175,8 @@ void convert(
184175
json_output["outputID"]=json_stringt(id2string(step.io_id));
185176

186177
// Recovering the mode from the function
187-
irep_idt mode;
188-
const symbolt *function_name;
189-
if(ns.lookup(source_location.get_function(), function_name))
190-
// Failed to find symbol
191-
mode=ID_unknown;
192-
else
193-
mode=function_name->mode;
178+
const irep_idt mode =
179+
get_mode_from_identifier(ns.get_symbol_table(), source_location.get_function());
194180
json_output["mode"]=json_stringt(id2string(mode));
195181
json_arrayt &json_values=json_output["values"].make_array();
196182

@@ -199,7 +185,7 @@ void convert(
199185
if(arg.is_nil())
200186
json_values.push_back(json_stringt(""));
201187
else
202-
json_values.push_back(json(arg, ns, mode));
188+
json_values.push_back(json(ns, source_location.get_function(), arg));
203189
}
204190

205191
if(!json_location.is_null())
@@ -218,13 +204,8 @@ void convert(
218204
json_input["inputID"]=json_stringt(id2string(step.io_id));
219205

220206
// Recovering the mode from the function
221-
irep_idt mode;
222-
const symbolt *function_name;
223-
if(ns.lookup(source_location.get_function(), function_name))
224-
// Failed to find symbol
225-
mode=ID_unknown;
226-
else
227-
mode=function_name->mode;
207+
const irep_idt mode =
208+
get_mode_from_identifier(ns.get_symbol_table(), source_location.get_function());
228209
json_input["mode"]=json_stringt(id2string(mode));
229210
json_arrayt &json_values=json_input["values"].make_array();
230211

@@ -233,7 +214,7 @@ void convert(
233214
if(arg.is_nil())
234215
json_values.push_back(json_stringt(""));
235216
else
236-
json_values.push_back(json(arg, ns, mode));
217+
json_values.push_back(json(ns, source_location.get_function(), arg));
237218
}
238219

239220
if(!json_location.is_null())

‎src/java_bytecode/java_json_expr.cpp

+49
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
/*******************************************************************\
2+
3+
Module: Expressions in JSON for Java
4+
5+
Author: Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Expressions in JSON for Java
11+
12+
#include "java_json_expr.h"
13+
14+
#include <util/json_expr.h>
15+
16+
/// Output a Java source location in json.
17+
/// \param location: a source location
18+
/// \return a json object
19+
json_objectt java_json(const source_locationt &location)
20+
{
21+
json_objectt result = json(source_location);
22+
23+
if(!location.get_java_bytecode_index().empty())
24+
result["bytecodeIndex"]=
25+
json_stringt(id2string(location.get_java_bytecode_index()));
26+
27+
return result;
28+
}
29+
30+
/// Output a Java expression in json.
31+
/// \param expr: an expression
32+
/// \param ns: a namespace
33+
/// \return a json object
34+
json_objectt java_json(
35+
const exprt &expr,
36+
const namespacet &ns)
37+
{
38+
if(expr.id()==ID_constant)
39+
{
40+
json_objectt result;
41+
json(result, ns, to_constant_expr(expr), type,
42+
[](const namespacet &ns, const exprt &expr) { return from_expr(ns, ID_java, expr); },
43+
[](const namespacet &ns, const typet &type) { return from_type(ns, ID_java, type); });
44+
return result;
45+
}
46+
47+
return json(expr, ns);
48+
}
49+
}

‎src/java_bytecode/java_json_expr.h

+33
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
/*******************************************************************\
2+
3+
Module: Expressions in JSON for Java
4+
5+
Author: Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Expressions in JSON for Java
11+
12+
#ifndef CPROVER_JAVA_BYTECODE_JAVA_JSON_EXPR_H
13+
#define CPROVER_JAVA_BYTECODE_JAVA_JSON_EXPR_H
14+
15+
#include "json.h"
16+
#include "irep.h"
17+
18+
class source_locationt;
19+
class typet;
20+
class exprt;
21+
class namespacet;
22+
23+
json_objectt java_json(
24+
const exprt &,
25+
const namespacet &);
26+
27+
json_objectt java_json(
28+
const typet &,
29+
const namespacet &);
30+
31+
json_objectt java_json(const source_locationt &);
32+
33+
#endif // CPROVER_JAVA_BYTECODE_JAVA_JSON_EXPR_H

‎src/langapi/language.cpp

+20
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
1212
#include "language.h"
1313

1414
#include <util/expr.h>
15+
#include <util/json_expr.h>
1516
#include <util/symbol.h>
1617
#include <util/symbol_table.h>
1718
#include <util/prefix.h>
@@ -52,6 +53,25 @@ bool languaget::from_type(
5253
return false;
5354
}
5455

56+
json_objectt languaget::json(
57+
const exprt &expr,
58+
const namespacet &ns)
59+
{
60+
return ::json(expr, ns);
61+
}
62+
63+
json_objectt languaget::json(
64+
const typet &type,
65+
const namespacet &ns)
66+
{
67+
return ::json(type, ns);
68+
}
69+
70+
json_objectt languaget::json(const source_locationt &source_location)
71+
{
72+
return ::json(source_location);
73+
}
74+
5575
bool languaget::type_to_name(
5676
const typet &type,
5777
std::string &name,

‎src/langapi/language.h

+11
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,7 @@ class exprt;
3131
class namespacet;
3232
class typet;
3333
class cmdlinet;
34+
class json_objectt;
3435

3536
#define OPT_FUNCTIONS \
3637
"(function):"
@@ -126,6 +127,16 @@ class languaget:public messaget
126127
std::string &code,
127128
const namespacet &ns);
128129

130+
virtual json_objectt json(
131+
const exprt &,
132+
const namespacet &);
133+
134+
virtual json_objectt json(
135+
const typet &,
136+
const namespacet &);
137+
138+
virtual json_objectt json(const source_locationt &);
139+
129140
virtual bool type_to_name(
130141
const typet &type,
131142
std::string &name,

‎src/langapi/language_util.cpp

+23
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,29 @@ std::string from_type(
4545
return result;
4646
}
4747

48+
json_objectt json(
49+
const namespacet &ns,
50+
const irep_idt &identifier,
51+
const exprt &expr)
52+
{
53+
std::unique_ptr<languaget> p(
54+
get_language_from_identifier(ns.get_symbol_table(), identifier));
55+
56+
std::string result;
57+
return p->json(expr, ns);
58+
}
59+
60+
json_objectt json(
61+
const namespacet &ns,
62+
const irep_idt &identifier,
63+
const typet &type)
64+
{
65+
std::unique_ptr<languaget> p(
66+
get_language_from_identifier(ns.get_symbol_table(), identifier));
67+
68+
return p->json(type, ns);
69+
}
70+
4871
std::string type_to_name(
4972
const namespacet &ns,
5073
const irep_idt &identifier,

‎src/langapi/language_util.h

+11
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
1515
class exprt;
1616
class namespacet;
1717
class typet;
18+
class json_objectt;
1819

1920
std::string from_expr(
2021
const namespacet &ns,
@@ -23,13 +24,23 @@ std::string from_expr(
2324

2425
std::string from_expr(const exprt &expr);
2526

27+
json_objectt json(
28+
const namespacet &ns,
29+
const irep_idt &identifier,
30+
const exprt &expr);
31+
2632
std::string from_type(
2733
const namespacet &ns,
2834
const irep_idt &identifier,
2935
const typet &type);
3036

3137
std::string from_type(const typet &type);
3238

39+
json_objectt json(
40+
const namespacet &ns,
41+
const irep_idt &identifier,
42+
const typet &type);
43+
3344
exprt to_expr(
3445
const namespacet &ns,
3546
const irep_idt &identifier,

0 commit comments

Comments
 (0)