Skip to content

Commit e7de09f

Browse files
committed
refactor: trying to go non-heap
1 parent e9c5b32 commit e7de09f

File tree

10 files changed

+90
-67
lines changed

10 files changed

+90
-67
lines changed

src/cli/detcheck/main.cpp

Lines changed: 10 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -24,8 +24,8 @@
2424
#include <plugin_system/plugin_system.h>
2525
#include <timer>
2626

27-
auto get_ntta(const std::vector<std::string>& plugin_dirs, const std::vector<std::string>& ignore_list, const std::string& parser, const std::vector<std::string>& input) -> std::unique_ptr<aaltitoad::ntta_t>;
28-
void find_deadlocks(const std::unique_ptr<aaltitoad::ntta_t>& ntta, const std::vector<std::string>& conditions, const std::optional<std::string>& condition_file, const std::vector<std::string> knowns, const std::optional<std::string>& known_file, const std::vector<std::string>& instance, const std::optional<std::string>& instance_file);
27+
auto get_ntta(const std::vector<std::string>& plugin_dirs, const std::vector<std::string>& ignore_list, const std::string& parser, const std::vector<std::string>& input) -> aaltitoad::ntta_t;
28+
void find_deadlocks(const aaltitoad::ntta_t& ntta, const std::vector<std::string>& conditions, const std::optional<std::string>& condition_file, const std::vector<std::string> knowns, const std::optional<std::string>& known_file, const std::vector<std::string>& instance, const std::optional<std::string>& instance_file);
2929

3030
int main(int argc, char** argv) {
3131
bool show_help = false;
@@ -97,7 +97,7 @@ int main(int argc, char** argv) {
9797

9898
auto automata = get_ntta(plugin_dirs, ignore, parser, input);
9999
if(list_instances) {
100-
for(auto& c: automata->components)
100+
for(auto& c: automata.components)
101101
std::cout << c.first << " ";
102102
std::cout << std::endl;
103103
return 0;
@@ -108,7 +108,7 @@ int main(int argc, char** argv) {
108108
return 0;
109109
}
110110

111-
auto get_ntta(const std::vector<std::string>& plugin_dirs, const std::vector<std::string>& ignore_list, const std::string& parser, const std::vector<std::string>& input) -> std::unique_ptr<aaltitoad::ntta_t> {
111+
auto get_ntta(const std::vector<std::string>& plugin_dirs, const std::vector<std::string>& ignore_list, const std::string& parser, const std::vector<std::string>& input) -> aaltitoad::ntta_t {
112112
/// Load plugins
113113
auto available_plugins = aaltitoad::plugins::load(plugin_dirs);
114114

@@ -124,9 +124,8 @@ auto get_ntta(const std::vector<std::string>& plugin_dirs, const std::vector<std
124124
aaltitoad::warnings::print_warnings(parse_result);
125125
if(!parse_result.has_value())
126126
throw std::logic_error("compilation failed");
127-
auto automata = std::move(parse_result.value().ntta);
128127
spdlog::trace("model parsing took {0}ms", t.milliseconds_elapsed());
129-
return automata;
128+
return parse_result.value().ntta;
130129
}
131130

132131
auto get_mentioned_symbols(const expr::syntax_tree_t& expression, const expr::symbol_table_t& symbols) -> expr::symbol_table_t {
@@ -149,9 +148,9 @@ auto get_mentioned_symbols(const expr::syntax_tree_t& expression, const expr::sy
149148
return mentioned;
150149
}
151150

152-
void find_deadlocks(const std::unique_ptr<aaltitoad::ntta_t>& ntta, const std::vector<std::string>& conditions, const std::optional<std::string>& condition_file, const std::vector<std::string> knowns, const std::optional<std::string>& known_file, const std::vector<std::string>& instance, const std::optional<std::string>& instance_file) {
151+
void find_deadlocks(const aaltitoad::ntta_t& ntta, const std::vector<std::string>& conditions, const std::optional<std::string>& condition_file, const std::vector<std::string> knowns, const std::optional<std::string>& known_file, const std::vector<std::string>& instance, const std::optional<std::string>& instance_file) {
153152
ya::timer<unsigned int> t{};
154-
aaltitoad::expression_driver c{ntta->symbols, ntta->external_symbols};
153+
aaltitoad::expression_driver c{ntta.symbols, ntta.external_symbols};
155154
std::vector<expr::syntax_tree_t> extra_conditions{};
156155
for(auto& condition : conditions) {
157156
auto result = c.parse(condition);
@@ -196,9 +195,9 @@ void find_deadlocks(const std::unique_ptr<aaltitoad::ntta_t>& ntta, const std::v
196195
}
197196
for(auto& instance: instances) {
198197
spdlog::trace("looking for '{0}' in components", instance);
199-
for(auto& location: ntta->components.at(instance).graph->nodes)
198+
for(auto& location: ntta.components.at(instance).graph->nodes)
200199
for(auto& edge: location.second.outgoing_edges)
201-
unknown_symbols += get_mentioned_symbols(edge->second.data.guard, ntta->symbols + ntta->external_symbols);
200+
unknown_symbols += get_mentioned_symbols(edge->second.data.guard, ntta.symbols + ntta.external_symbols);
202201
}
203202
spdlog::trace("finding {0} mentioned symbols in {1} tta instances took {2}ms", unknown_symbols.size(), instances.size(), t.milliseconds_elapsed());
204203

@@ -209,7 +208,7 @@ void find_deadlocks(const std::unique_ptr<aaltitoad::ntta_t>& ntta, const std::v
209208
aaltitoad::expression_driver d{known_symbols, unknown_symbols};
210209
for(auto& instance : instances) {
211210
spdlog::trace("looking for '{0}' in components", instance);
212-
for(auto& location : ntta->components.at(instance).graph->nodes) {
211+
for(auto& location : ntta.components.at(instance).graph->nodes) {
213212
t.start();
214213
if(location.second.outgoing_edges.empty())
215214
continue;

src/cli/simulator/main.cpp

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -126,9 +126,9 @@ int main(int argc, char** argv) {
126126

127127
/// Inject tockers - CLI Format: "name(argument)"
128128
for(auto& arg : tockers) {
129-
auto tocker = instantiate_tocker(arg, available_plugins, *automata);
129+
auto tocker = instantiate_tocker(arg, available_plugins, automata);
130130
if(tocker.has_value())
131-
automata->tockers.emplace_back(std::move(tocker.value()));
131+
automata.tockers.emplace_back(std::move(tocker.value()));
132132
}
133133

134134
/// Run
@@ -141,15 +141,15 @@ int main(int argc, char** argv) {
141141
for (; i < ticks || ticks < 0; i++) {
142142
if(spdlog::get_level() <= spdlog::level::trace) {
143143
std::stringstream ss{};
144-
ss << "state:\n" << *automata;
144+
ss << "state:\n" << automata;
145145
spdlog::trace(ss.str());
146146
}
147-
auto tock_changes = automata->tock();
147+
auto tock_changes = automata.tock();
148148
if(!tock_changes.empty())
149-
automata->apply(tock_changes[0]);
150-
auto tick_changes = automata->tick();
149+
automata.apply(tock_changes[0]);
150+
auto tick_changes = automata.tick();
151151
if(!tick_changes.empty())
152-
automata->apply(tick_changes[0]);
152+
automata.apply(tick_changes[0]);
153153
}
154154
#ifdef NDEBUG
155155
} catch (std::exception& e) {

src/cli/verifier/main.cpp

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -139,13 +139,13 @@ int main(int argc, char** argv) {
139139
return 1;
140140
}
141141

142-
auto n = std::move(parse_result.value().ntta);
143-
trace_log_ntta(*n);
142+
auto n = parse_result.value().ntta;
143+
trace_log_ntta(n);
144144
spdlog::debug("model parsing took {0}ms", t.milliseconds_elapsed());
145145

146146
t.start();
147147
std::vector<ctl::syntax_tree_t> queries{};
148-
aaltitoad::ctl_interpreter ctl_compiler{n->symbols, n->external_symbols};
148+
aaltitoad::ctl_interpreter ctl_compiler{n.symbols, n.external_symbols};
149149
for(auto& q : query) {
150150
spdlog::trace("compiling query '{0}'", q);
151151
auto qq = ctl_compiler.compile(q);
@@ -155,19 +155,19 @@ int main(int argc, char** argv) {
155155
}
156156
for(auto& f : query_files) {
157157
spdlog::trace("loading queries in file {0}", f);
158-
auto json_queries = aaltitoad::load_query_json_file(f, {n->symbols, n->external_symbols});
158+
auto json_queries = aaltitoad::load_query_json_file(f, {n.symbols, n.external_symbols});
159159
queries.insert(queries.end(), json_queries.begin(), json_queries.end());
160160
}
161161
spdlog::debug("query parsing took {0}ms", t.milliseconds_elapsed());
162162

163163
auto strategy = magic_enum::enum_cast<aaltitoad::pick_strategy>(pick_strategy).value_or(aaltitoad::pick_strategy::first);
164164
spdlog::debug("using pick strategy '{0}'", magic_enum::enum_name(strategy));
165165

166-
n->add_tocker(std::make_unique<aaltitoad::interesting_tocker>());
166+
n.add_tocker(std::make_unique<aaltitoad::interesting_tocker>());
167167
spdlog::trace("starting reachability search for {0} queries", queries.size());
168168
t.start();
169169
aaltitoad::forward_reachability_searcher frs{strategy};
170-
auto results = frs.is_reachable(*n, queries);
170+
auto results = frs.is_reachable(n, queries);
171171
spdlog::info("reachability search took {0}ms", t.milliseconds_elapsed());
172172

173173
// open the results file (std::cout by default)

src/parser/hawk/compiler.cpp

Lines changed: 19 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -12,17 +12,17 @@ namespace aaltitoad::hawk {
1212
}
1313

1414
compiler::compiler(
15-
std::unique_ptr<scanner>&& _scanner,
16-
std::unique_ptr<parser>&& _parser,
17-
std::unique_ptr<semantic_analyzer>&& _analyzer,
18-
std::unique_ptr<optimizer>&& _optimizer,
19-
std::unique_ptr<generator>&& _generator)
15+
scanner& _scanner,
16+
parser& _parser,
17+
semantic_analyzer& _analyzer,
18+
optimizer& _optimizer,
19+
generator& _generator)
2020
:
21-
_scanner{std::move(_scanner)},
22-
_parser{std::move(_parser)},
23-
_analyzer{std::move(_analyzer)},
24-
_optimizer{std::move(_optimizer)},
25-
_generator{std::move(_generator)},
21+
_scanner{_scanner},
22+
_parser{_parser},
23+
_analyzer{_analyzer},
24+
_optimizer{_optimizer},
25+
_generator{_generator},
2626
symbols{},
2727
_diagnostic_factory{} {
2828
}
@@ -36,18 +36,18 @@ namespace aaltitoad::hawk {
3636
}
3737

3838
auto compiler::compile(const std::vector<std::string>& paths, const std::vector<std::string>& ignore_list) -> std::expected<ok, error_t> {
39-
auto stream = _scanner->scan(*this, paths, ignore_list);
39+
auto stream = _scanner.scan(*this, paths, ignore_list);
4040
if(!stream)
4141
return std::unexpected{stream.error()};
42-
auto ast = _parser->parse(*this, stream.value());
42+
auto ast = _parser.parse(*this, stream.value());
4343
if(!ast)
4444
return std::unexpected{ast.error()};
45-
auto dast_r = _analyzer->analyze(*this, ast.value());
45+
auto dast_r = _analyzer.analyze(*this, ast.value());
4646
if(!dast_r)
4747
return std::unexpected{dast_r.error()};
4848
auto dast = dast_r.value();
49-
_optimizer->optimize(*this, dast);
50-
auto ntta = _generator->generate(*this, dast);
49+
_optimizer.optimize(*this, dast);
50+
auto ntta = _generator.generate(*this, dast);
5151
if(!ntta)
5252
return std::unexpected(ntta.error());
5353
return ok{
@@ -67,4 +67,8 @@ namespace aaltitoad::hawk {
6767
error_t::error_t() : diagnostics{} {}
6868

6969
error_t::error_t(const std::vector<Diagnostic>& diagnostics) : diagnostics{diagnostics} {}
70+
71+
void nothing_optimizer::optimize(compiler& ctx, parser::ok& ast) const {
72+
73+
}
7074
}

src/parser/hawk/compiler.h

Lines changed: 13 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,12 @@ namespace aaltitoad::hawk {
5858
virtual void optimize(compiler& ctx, parser::ok& ast) const = 0;
5959
};
6060

61+
class nothing_optimizer : public optimizer {
62+
public:
63+
~nothing_optimizer() override = default;
64+
void optimize(compiler& ctx, parser::ok& ast) const override;
65+
};
66+
6167
struct generator {
6268
generator() = default;
6369
virtual ~generator() = default;
@@ -71,24 +77,20 @@ namespace aaltitoad::hawk {
7177
std::vector<Diagnostic> diagnostics;
7278
};
7379

74-
compiler(
75-
std::unique_ptr<scanner>&& scanner,
76-
std::unique_ptr<parser>&& parser,
77-
std::unique_ptr<semantic_analyzer>&& analyzer,
78-
std::unique_ptr<optimizer>&& optimizer,
79-
std::unique_ptr<generator>&& generator);
80+
compiler(scanner& scanner);
81+
compiler(scanner& scanner, parser& parser, semantic_analyzer& analyzer, optimizer& optimizer, generator& generator);
8082
void add_symbols(const expr::symbol_table_t& symbols);
8183
void clear_symbols();
8284
auto get_diagnostic_factory() -> diagnostic_factory&;
8385
auto diag(const diagnostic& d) -> Diagnostic;
8486
auto compile(const std::vector<std::string>& paths, const std::vector<std::string>& ignore_list) -> std::expected<ok, error_t>;
8587

8688
private:
87-
std::unique_ptr<scanner> _scanner;
88-
std::unique_ptr<parser> _parser;
89-
std::unique_ptr<semantic_analyzer> _analyzer;
90-
std::unique_ptr<optimizer> _optimizer;
91-
std::unique_ptr<generator> _generator;
89+
scanner& _scanner;
90+
parser& _parser;
91+
semantic_analyzer& _analyzer;
92+
optimizer& _optimizer;
93+
generator& _generator;
9294
expr::symbol_table_t symbols;
9395
diagnostic_factory _diagnostic_factory;
9496
};

src/parser/hawk/huppaal/parser.cpp

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -69,19 +69,21 @@ namespace aaltitoad::hawk::huppaal {
6969
return std::unexpected(error_t({ctx.diag(not_implemented_yet())}));
7070
}
7171

72-
parser::parser() : compiler{} {
73-
74-
}
75-
7672
auto parser::parse_files(const std::vector<std::string>& files, const std::vector<std::string>& ignore_patterns) -> plugin::parse_result {
77-
auto compile_result = compiler->compile(files, ignore_patterns);
73+
auto compiler = create_compiler();
74+
auto compile_result = compiler.compile(files, ignore_patterns);
7875
if(!compile_result.has_value())
7976
return std::unexpected(plugin::parse_error{compile_result.error().diagnostics});
8077
return plugin::parse_ok{compile_result.value().ntta, compile_result.value().diagnostics};
8178
}
8279

8380
auto parser::parse_model(const Buffer& buffer) -> plugin::parse_result {
84-
return std::unexpected(plugin::parse_error({compiler->diag(not_implemented_yet())}));
81+
auto compiler = create_compiler();
82+
return std::unexpected(plugin::parse_error{std::vector<Diagnostic>{compiler.diag(not_implemented_yet())}});
83+
}
84+
85+
auto parser::create_compiler() -> compiler {
86+
return compiler{_scanner, _parser, _semantic_analyzer, _optimizer, _generator};
8587
}
8688
}
8789

src/parser/hawk/huppaal/parser.h

Lines changed: 20 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@
2424
namespace aaltitoad::hawk::huppaal {
2525
auto create_parser() -> plugin::parser*;
2626

27-
class huppaal_scanner : public aaltitoad::hawk::scanner{
27+
class huppaal_scanner : public aaltitoad::hawk::scanner {
2828
public:
2929
~huppaal_scanner() override = default;
3030
auto scan(compiler& ctx,
@@ -41,14 +41,31 @@ namespace aaltitoad::hawk::huppaal {
4141
auto parse(compiler& ctx, const scanner::ok& stream) const noexcept -> std::expected<parser::ok, error_t> override;
4242
};
4343

44+
class huppaal_semantic_analyzer : public aaltitoad::hawk::semantic_analyzer {
45+
public:
46+
~huppaal_semantic_analyzer() override = default;
47+
auto analyze(compiler& ctx, const parser::ok& ast) const noexcept -> std::expected<parser::ok, error_t> override;
48+
};
49+
50+
class huppaal_generator : public aaltitoad::hawk::generator {
51+
public:
52+
~huppaal_generator() override = default;
53+
auto generate(compiler& ctx, const parser::ok& ast) const noexcept -> std::expected<ntta_t, error_t> override;
54+
};
55+
4456
class parser : public plugin::parser {
4557
public:
46-
parser();
4758
~parser() override = default;
4859
auto parse_files(const std::vector<std::string>& files, const std::vector<std::string>& ignore_patterns) -> plugin::parse_result override;
4960
auto parse_model(const Buffer& buffer) -> plugin::parse_result override;
5061
private:
51-
std::unique_ptr<compiler> compiler;
62+
auto create_compiler() -> compiler;
63+
64+
huppaal_scanner _scanner;
65+
huppaal_parser _parser;
66+
huppaal_semantic_analyzer _semantic_analyzer;
67+
nothing_optimizer _optimizer;
68+
huppaal_generator _generator;
5269
};
5370
}
5471

src/parser/hawk/scoped_template_builder/scoped_template_builder.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -256,7 +256,7 @@ namespace aaltitoad::hawk {
256256
builder.add_symbols(internal_symbols);
257257
builder.add_external_symbols(external_symbols);
258258
return plugin::parse_ok{
259-
.ntta=std::unique_ptr<ntta_t>{builder.build_heap()},
259+
.ntta=builder.build(),
260260
.diagnostics=diagnostics
261261
};
262262
}

src/plugin_system/parser.h

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,6 @@
22
#define AALTITOAD_PARSER_H
33
#include "lsp.pb.h"
44
#include "ntta/tta.h"
5-
#include <memory>
65
#include <expected>
76

87
namespace aaltitoad::plugin {

test/verification/parser_tests.cpp

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -34,9 +34,9 @@ SCENARIO("parsing fischer-n suite", "[hawk_parser]") {
3434
REQUIRE(parse_result.has_value());
3535
CHECK(parse_result.value().diagnostics.size() == 1); // TODO: The success state should not result in diagnostics
3636
auto n = std::move(parse_result.value().ntta);
37-
std::cout << *n << std::endl;
37+
std::cout << n << std::endl;
3838
THEN("three TTAs are constructed (Main, fischer1, and fischer2)") {
39-
REQUIRE(n->components.size() == 3);
39+
REQUIRE(n.components.size() == 3);
4040
}
4141
}
4242
}
@@ -47,9 +47,9 @@ SCENARIO("parsing fischer-n suite", "[hawk_parser]") {
4747
REQUIRE(parse_result.has_value());
4848
CHECK(parse_result.value().diagnostics.size() == 4); // TODO: The success state should not result in diagnostics
4949
auto n = std::move(parse_result.value().ntta);
50-
std::cout << *n << std::endl;
50+
std::cout << n << std::endl;
5151
THEN("six TTAs are constructed (fischer instances + main)") {
52-
REQUIRE(n->components.size() == 6);
52+
REQUIRE(n.components.size() == 6);
5353
}
5454
}
5555
}
@@ -60,9 +60,9 @@ SCENARIO("parsing fischer-n suite", "[hawk_parser]") {
6060
CHECK(parse_result.value().diagnostics.size() == 9); // TODO: The success state should not result in diagnostics
6161
REQUIRE(parse_result.has_value());
6262
auto n = std::move(parse_result.value().ntta);
63-
std::cout << *n << std::endl;
63+
std::cout << n << std::endl;
6464
THEN("eleven TTAs are constructed (fischer instances + main)") {
65-
REQUIRE(n->components.size() == 11);
65+
REQUIRE(n.components.size() == 11);
6666
}
6767
}
6868
}

0 commit comments

Comments
 (0)