Skip to content

Commit b2ea1db

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

File tree

10 files changed

+138
-65
lines changed

10 files changed

+138
-65
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: 36 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,20 @@
1+
/**
2+
* aaltitoad - a verification engine for tick tock automata models
3+
Copyright (C) 2023 Asger Gitz-Johansen
4+
5+
This program is free software: you can redistribute it and/or modify
6+
it under the terms of the GNU General Public License as published by
7+
the Free Software Foundation, either version 3 of the License, or
8+
(at your option) any later version.
9+
10+
This program is distributed in the hope that it will be useful,
11+
but WITHOUT ANY WARRANTY; without even the implied warranty of
12+
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13+
GNU General Public License for more details.
14+
15+
You should have received a copy of the GNU General Public License
16+
along with this program. If not, see <https://www.gnu.org/licenses/>.
17+
*/
118
#include "compiler.h"
219
#include <overload>
320

@@ -12,17 +29,17 @@ namespace aaltitoad::hawk {
1229
}
1330

1431
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)
32+
scanner& _scanner,
33+
parser& _parser,
34+
semantic_analyzer& _analyzer,
35+
optimizer& _optimizer,
36+
generator& _generator)
2037
:
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)},
38+
_scanner{_scanner},
39+
_parser{_parser},
40+
_analyzer{_analyzer},
41+
_optimizer{_optimizer},
42+
_generator{_generator},
2643
symbols{},
2744
_diagnostic_factory{} {
2845
}
@@ -36,18 +53,18 @@ namespace aaltitoad::hawk {
3653
}
3754

3855
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);
56+
auto stream = _scanner.scan(*this, paths, ignore_list);
4057
if(!stream)
4158
return std::unexpected{stream.error()};
42-
auto ast = _parser->parse(*this, stream.value());
59+
auto ast = _parser.parse(*this, stream.value());
4360
if(!ast)
4461
return std::unexpected{ast.error()};
45-
auto dast_r = _analyzer->analyze(*this, ast.value());
62+
auto dast_r = _analyzer.analyze(*this, ast.value());
4663
if(!dast_r)
4764
return std::unexpected{dast_r.error()};
4865
auto dast = dast_r.value();
49-
_optimizer->optimize(*this, dast);
50-
auto ntta = _generator->generate(*this, dast);
66+
_optimizer.optimize(*this, dast);
67+
auto ntta = _generator.generate(*this, dast);
5168
if(!ntta)
5269
return std::unexpected(ntta.error());
5370
return ok{
@@ -67,4 +84,8 @@ namespace aaltitoad::hawk {
6784
error_t::error_t() : diagnostics{} {}
6885

6986
error_t::error_t(const std::vector<Diagnostic>& diagnostics) : diagnostics{diagnostics} {}
87+
88+
void nothing_optimizer::optimize(compiler& ctx, parser::ok& ast) const {
89+
90+
}
7091
}

src/parser/hawk/compiler.h

Lines changed: 30 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,20 @@
1+
/**
2+
* aaltitoad - a verification engine for tick tock automata models
3+
Copyright (C) 2023 Asger Gitz-Johansen
4+
5+
This program is free software: you can redistribute it and/or modify
6+
it under the terms of the GNU General Public License as published by
7+
the Free Software Foundation, either version 3 of the License, or
8+
(at your option) any later version.
9+
10+
This program is distributed in the hope that it will be useful,
11+
but WITHOUT ANY WARRANTY; without even the implied warranty of
12+
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13+
GNU General Public License for more details.
14+
15+
You should have received a copy of the GNU General Public License
16+
along with this program. If not, see <https://www.gnu.org/licenses/>.
17+
*/
118
#ifndef AALTITOAD_HAWK_COMPILER_H
219
#define AALTITOAD_HAWK_COMPILER_H
320
#include "ntta/tta.h"
@@ -58,6 +75,12 @@ namespace aaltitoad::hawk {
5875
virtual void optimize(compiler& ctx, parser::ok& ast) const = 0;
5976
};
6077

78+
class nothing_optimizer : public optimizer {
79+
public:
80+
~nothing_optimizer() override = default;
81+
void optimize(compiler& ctx, parser::ok& ast) const override;
82+
};
83+
6184
struct generator {
6285
generator() = default;
6386
virtual ~generator() = default;
@@ -71,24 +94,20 @@ namespace aaltitoad::hawk {
7194
std::vector<Diagnostic> diagnostics;
7295
};
7396

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);
97+
compiler(scanner& scanner);
98+
compiler(scanner& scanner, parser& parser, semantic_analyzer& analyzer, optimizer& optimizer, generator& generator);
8099
void add_symbols(const expr::symbol_table_t& symbols);
81100
void clear_symbols();
82101
auto get_diagnostic_factory() -> diagnostic_factory&;
83102
auto diag(const diagnostic& d) -> Diagnostic;
84103
auto compile(const std::vector<std::string>& paths, const std::vector<std::string>& ignore_list) -> std::expected<ok, error_t>;
85104

86105
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;
106+
scanner& _scanner;
107+
parser& _parser;
108+
semantic_analyzer& _analyzer;
109+
optimizer& _optimizer;
110+
generator& _generator;
92111
expr::symbol_table_t symbols;
93112
diagnostic_factory _diagnostic_factory;
94113
};

src/parser/hawk/huppaal/parser.cpp

Lines changed: 22 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -65,23 +65,41 @@ namespace aaltitoad::hawk::huppaal {
6565
return std::regex_match(entry.path().c_str(), std::regex{ignore_regex});
6666
}
6767

68+
/* =========== */
69+
6870
auto huppaal_parser::parse(compiler& ctx, const scanner::ok& stream) const noexcept -> std::expected<parser::ok, error_t> {
6971
return std::unexpected(error_t({ctx.diag(not_implemented_yet())}));
7072
}
7173

72-
parser::parser() : compiler{} {
73-
74+
/* =========== */
75+
76+
auto huppaal_semantic_analyzer::analyze(compiler& ctx, const aaltitoad::hawk::parser::ok& ast) const noexcept -> std::expected<aaltitoad::hawk::parser::ok, error_t> {
77+
return std::unexpected(error_t({ctx.diag(not_implemented_yet())}));
78+
}
79+
80+
/* =========== */
81+
82+
auto huppaal_generator::generate(compiler& ctx, const aaltitoad::hawk::parser::ok& ast) const noexcept -> std::expected<ntta_t, error_t> {
83+
return std::unexpected(error_t({ctx.diag(not_implemented_yet())}));
7484
}
7585

86+
/* =========== */
87+
7688
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);
89+
auto compiler = create_compiler();
90+
auto compile_result = compiler.compile(files, ignore_patterns);
7891
if(!compile_result.has_value())
7992
return std::unexpected(plugin::parse_error{compile_result.error().diagnostics});
8093
return plugin::parse_ok{compile_result.value().ntta, compile_result.value().diagnostics};
8194
}
8295

8396
auto parser::parse_model(const Buffer& buffer) -> plugin::parse_result {
84-
return std::unexpected(plugin::parse_error({compiler->diag(not_implemented_yet())}));
97+
auto compiler = create_compiler();
98+
return std::unexpected(plugin::parse_error{std::vector<Diagnostic>{compiler.diag(not_implemented_yet())}});
99+
}
100+
101+
auto parser::create_compiler() -> compiler {
102+
return compiler{_scanner, _parser, _semantic_analyzer, _optimizer, _generator};
85103
}
86104
}
87105

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 {

0 commit comments

Comments
 (0)