From 56defe3f637bf3760b0b24346b5f35b8f1ce1fe7 Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Mon, 4 Mar 2024 17:20:14 +0000 Subject: [PATCH] Mass reformat --- bindings/c/lib.cpp | 3 +- bindings/python/ast.cpp | 23 +++++--- include/kllvm/ast/AST.h | 40 ++++++++----- include/kllvm/ast/attribute_set.h | 4 +- include/kllvm/ast/pattern_matching.h | 3 +- include/kllvm/binary/ProofTraceParser.h | 12 +++- include/kllvm/codegen/CreateTerm.h | 13 +++-- include/kllvm/codegen/Debug.h | 3 +- include/kllvm/codegen/ProofEvent.h | 3 +- include/runtime/header.h | 3 +- lib/ast/definition.cpp | 43 ++++++++------ lib/codegen/CreateStaticTerm.cpp | 33 ++++++----- lib/codegen/Debug.cpp | 35 +++++++----- lib/codegen/ProofEvent.cpp | 19 ++++--- lib/printer/addBrackets.cpp | 19 ++++--- lib/printer/printer.cpp | 2 +- runtime/alloc/arena.cpp | 6 +- runtime/arithmetic/float.cpp | 15 +++-- runtime/collections/maps.cpp | 3 +- runtime/collections/rangemaps.cpp | 3 +- runtime/io/io.cpp | 7 ++- runtime/json/json.cpp | 9 +-- runtime/strings/bytes.cpp | 5 +- runtime/strings/strings.cpp | 7 ++- runtime/util/ConfigurationParser.cpp | 6 +- runtime/util/ConfigurationPrinter.cpp | 10 ++-- runtime/util/ConfigurationSerializer.cpp | 9 ++- runtime/util/match_log.cpp | 7 ++- tools/k-rule-apply/auxiliar.h | 6 +- tools/k-rule-apply/main.cpp | 6 +- tools/k-rule-find/main.cpp | 8 +-- tools/llvm-kompile-codegen/main.cpp | 3 +- unittests/runtime-io/io.cpp | 72 +++++++++++++++--------- unittests/runtime-strings/stringtest.cpp | 10 ++-- 34 files changed, 278 insertions(+), 172 deletions(-) diff --git a/bindings/c/lib.cpp b/bindings/c/lib.cpp index cdbdbadaa..546124273 100644 --- a/bindings/c/lib.cpp +++ b/bindings/c/lib.cpp @@ -340,7 +340,8 @@ kore_pattern *kore_composite_pattern_new(char const *name) { } kore_pattern *kore_composite_pattern_from_symbol(kore_symbol *sym) { - return new kore_pattern{kllvm::kore_composite_pattern::create(sym->ptr.get())}; + return new kore_pattern{ + kllvm::kore_composite_pattern::create(sym->ptr.get())}; } void kore_composite_pattern_add_argument( diff --git a/bindings/python/ast.cpp b/bindings/python/ast.cpp index c3931b419..7960faedb 100644 --- a/bindings/python/ast.cpp +++ b/bindings/python/ast.cpp @@ -145,7 +145,8 @@ void bind_ast(py::module_ &m) { py::arg("is_hooked") = false) .def_property_readonly( "is_hooked", &kore_composite_sort_declaration::is_hooked) - .def_property_readonly("name", &kore_composite_sort_declaration::get_name); + .def_property_readonly( + "name", &kore_composite_sort_declaration::get_name); auto symbol_alias_decl_base = py::class_< @@ -173,7 +174,9 @@ void bind_ast(py::module_ &m) { py::class_>( ast, "AxiomDeclaration", decl_base) - .def(py::init(&kore_axiom_declaration::create), py::arg("is_claim") = false) + .def( + py::init(&kore_axiom_declaration::create), + py::arg("is_claim") = false) .def_property_readonly("is_claim", &kore_axiom_declaration::is_claim) .def("add_pattern", &kore_axiom_declaration::add_pattern) .def_property_readonly("pattern", &kore_axiom_declaration::get_pattern); @@ -202,7 +205,8 @@ void bind_ast(py::module_ &m) { return decl.attributes().underlying(); }); - py::class_>(ast, "Definition") + py::class_>( + ast, "Definition") .def(py::init(&kore_definition::create)) .def("__repr__", print_repr_adapter()) .def("add_module", &kore_definition::add_module) @@ -340,7 +344,8 @@ void bind_ast(py::module_ &m) { "constructor", &kore_composite_pattern::get_constructor) .def("desugar_associative", &kore_composite_pattern::desugar_associative) .def("add_argument", &kore_composite_pattern::add_argument) - .def_property_readonly("arguments", &kore_composite_pattern::get_arguments); + .def_property_readonly( + "arguments", &kore_composite_pattern::get_arguments); py::class_>( ast, "VariablePattern", pattern_base) @@ -371,9 +376,10 @@ void bind_parser(py::module_ &mod) { void bind_proof_trace(py::module_ &m) { auto proof_trace = m.def_submodule("prooftrace", "K LLVM backend KORE AST"); - auto step_event = py::class_>( - proof_trace, "llvm_step_event") - .def("__repr__", print_repr_adapter()); + auto step_event + = py::class_>( + proof_trace, "llvm_step_event") + .def("__repr__", print_repr_adapter()); auto rewrite_event = py::class_>( @@ -392,7 +398,8 @@ void bind_proof_trace(py::module_ &m) { proof_trace, "llvm_side_condition_event", rewrite_event); py::class_< - llvm_side_condition_end_event, std::shared_ptr>( + llvm_side_condition_end_event, + std::shared_ptr>( proof_trace, "llvm_side_condition_end_event", step_event) .def_property_readonly( "rule_ordinal", &llvm_side_condition_end_event::get_rule_ordinal) diff --git a/include/kllvm/ast/AST.h b/include/kllvm/ast/AST.h index 9cbc3e1c1..dd19251be 100644 --- a/include/kllvm/ast/AST.h +++ b/include/kllvm/ast/AST.h @@ -159,7 +159,8 @@ class kore_composite_sort : public kore_sort { public: static sptr create( - std::string const &name, value_type cat = {sort_category::Uncomputed, 0}) { + std::string const &name, + value_type cat = {sort_category::Uncomputed, 0}) { return sptr(new kore_composite_sort(name, cat)); } @@ -177,7 +178,9 @@ class kore_composite_sort : public kore_sort { void serialize_to(serializer &s) const override; bool operator==(kore_sort const &other) const override; - std::vector> const &get_arguments() const { return arguments_; } + std::vector> const &get_arguments() const { + return arguments_; + } private: kore_composite_sort(std::string name, value_type category) @@ -234,7 +237,8 @@ class kore_symbol { [[nodiscard]] std::vector> const &get_arguments() const { return arguments_; } - [[nodiscard]] std::vector> const &get_formal_arguments() const { + [[nodiscard]] std::vector> const & + get_formal_arguments() const { return formal_arguments_; } [[nodiscard]] sptr get_sort() const { return sort_; } @@ -399,7 +403,8 @@ class kore_pattern : public std::enable_shared_from_this { virtual void pretty_print(std::ostream &, pretty_print_data const &data) const = 0; - virtual sptr sort_collections(pretty_print_data const &data) = 0; + virtual sptr sort_collections(pretty_print_data const &data) + = 0; std::set gather_singleton_vars(); virtual std::map gather_var_counts() = 0; virtual sptr filter_substitution( @@ -438,7 +443,8 @@ class kore_pattern : public std::enable_shared_from_this { virtual sptr expand_macros( SubsortMap const &subsorts, SymbolMap const &overloads, std::vector> const &axioms, bool reverse, - std::set &applied_rules, std::set const ¯o_symbols) + std::set &applied_rules, + std::set const ¯o_symbols) = 0; }; @@ -530,10 +536,12 @@ class kore_composite_pattern : public kore_pattern { public: static ptr create(std::string const &name) { ptr sym = kore_symbol::create(name); - return ptr(new kore_composite_pattern(std::move(sym))); + return ptr( + new kore_composite_pattern(std::move(sym))); } static ptr create(ptr sym) { - return ptr(new kore_composite_pattern(std::move(sym))); + return ptr( + new kore_composite_pattern(std::move(sym))); } static ptr create(kore_symbol *sym) { ptr new_sym = kore_symbol::create(sym->get_name()); @@ -567,7 +575,8 @@ class kore_composite_pattern : public kore_pattern { pretty_print(std::ostream &out, pretty_print_data const &data) const override; void mark_symbols(std::map> &) override; - void mark_variables(std::map &) override; + void + mark_variables(std::map &) override; sptr substitute(substitution const &) override; sptr expand_aliases(kore_definition *) override; sptr sort_collections(pretty_print_data const &data) override; @@ -589,7 +598,8 @@ class kore_composite_pattern : public kore_pattern { std::set &applied_rules, std::set const ¯o_symbols) override; - friend void ::kllvm::deallocate_s_ptr_kore_pattern(sptr pattern); + friend void ::kllvm::deallocate_s_ptr_kore_pattern( + sptr pattern); kore_composite_pattern(ptr constructor) : constructor_(std::move(constructor)) { } @@ -608,15 +618,15 @@ class kore_string_pattern : public kore_pattern { void print(std::ostream &out, unsigned indent = 0) const override; void serialize_to(serializer &s) const override; - void - pretty_print(std::ostream &out, pretty_print_data const &data) const override { + void pretty_print( + std::ostream &out, pretty_print_data const &data) const override { abort(); } void mark_symbols(std::map> &) override { } - void mark_variables(std::map &) override { - } + void + mark_variables(std::map &) override { } sptr get_sort() const override { abort(); } sptr substitute(substitution const &) override { return shared_from_this(); @@ -811,7 +821,9 @@ class kore_module_import_declaration : public kore_declaration { new kore_module_import_declaration(name)); } - [[nodiscard]] std::string const &get_module_name() const { return module_name_; } + [[nodiscard]] std::string const &get_module_name() const { + return module_name_; + } void print(std::ostream &out, unsigned indent = 0) const override; diff --git a/include/kllvm/ast/attribute_set.h b/include/kllvm/ast/attribute_set.h index a76110f95..82739c722 100644 --- a/include/kllvm/ast/attribute_set.h +++ b/include/kllvm/ast/attribute_set.h @@ -29,8 +29,8 @@ class kore_composite_pattern; */ class attribute_set { public: - using storage_t - = std::unordered_map>; + using storage_t = std::unordered_map< + std::string, std::shared_ptr>; enum class key { Alias, diff --git a/include/kllvm/ast/pattern_matching.h b/include/kllvm/ast/pattern_matching.h index 43b55b5ff..03f1ee5a9 100644 --- a/include/kllvm/ast/pattern_matching.h +++ b/include/kllvm/ast/pattern_matching.h @@ -239,7 +239,8 @@ class pattern { */ [[nodiscard]] match_result match(std::shared_ptr const &term) const { - if (auto composite = std::dynamic_pointer_cast(term); + if (auto composite + = std::dynamic_pointer_cast(term); composite && composite->get_arguments().size() == arity() && composite->get_constructor()->get_name() == constructor_) { auto results = std::vector{}; diff --git a/include/kllvm/binary/ProofTraceParser.h b/include/kllvm/binary/ProofTraceParser.h index 759d5a788..c36c78d9b 100644 --- a/include/kllvm/binary/ProofTraceParser.h +++ b/include/kllvm/binary/ProofTraceParser.h @@ -205,7 +205,9 @@ class llvm_event { public: [[nodiscard]] bool is_step() const { return is_step_event_; } [[nodiscard]] bool is_pattern() const { return !is_step(); } - [[nodiscard]] sptr get_step_event() const { return step_event_; } + [[nodiscard]] sptr get_step_event() const { + return step_event_; + } [[nodiscard]] sptr getkore_pattern() const { return kore_pattern_; } @@ -235,7 +237,9 @@ class llvm_rewrite_trace { [[nodiscard]] std::vector const &get_pre_trace() const { return pre_trace_; } - [[nodiscard]] llvm_event get_initial_config() const { return initial_config_; } + [[nodiscard]] llvm_event get_initial_config() const { + return initial_config_; + } [[nodiscard]] std::vector const &get_trace() const { return trace_; } @@ -244,7 +248,9 @@ class llvm_rewrite_trace { initial_config_ = std::move(initial_config); } - void add_pre_trace_event(llvm_event const &event) { pre_trace_.push_back(event); } + void add_pre_trace_event(llvm_event const &event) { + pre_trace_.push_back(event); + } void add_trace_event(llvm_event const &event) { trace_.push_back(event); } void print(std::ostream &out, unsigned indent = 0U) const; diff --git a/include/kllvm/codegen/CreateTerm.h b/include/kllvm/codegen/CreateTerm.h index 918697fe6..c764ee765 100644 --- a/include/kllvm/codegen/CreateTerm.h +++ b/include/kllvm/codegen/CreateTerm.h @@ -21,7 +21,8 @@ class create_term { std::set static_terms_; llvm::Value *alloc_arg( - kore_composite_pattern *pattern, int idx, std::string const &location_stack); + kore_composite_pattern *pattern, int idx, + std::string const &location_stack); llvm::Value *create_hook( kore_composite_pattern *hook_att, kore_composite_pattern *pattern, std::string const &location_stack = "0"); @@ -38,7 +39,8 @@ class create_term { public: create_term( llvm::StringMap &substitution, kore_definition *definition, - llvm::BasicBlock *entry_block, llvm::Module *module, bool is_anywhere_owise) + llvm::BasicBlock *entry_block, llvm::Module *module, + bool is_anywhere_owise) : substitution_(substitution) , definition_(definition) , current_block_(entry_block) @@ -85,12 +87,13 @@ std::unique_ptr new_module(std::string const &name, llvm::LLVMContext &context); llvm::StructType *get_block_type( - llvm::Module *module, kore_definition *definition, kore_symbol const *symbol); + llvm::Module *module, kore_definition *definition, + kore_symbol const *symbol); uint64_t get_block_header_val( llvm::Module *module, kore_symbol const *symbol, llvm::Type *block_type); llvm::Value *get_block_header( - llvm::Module *module, kore_definition *definition, kore_symbol const *symbol, - llvm::Type *block_type); + llvm::Module *module, kore_definition *definition, + kore_symbol const *symbol, llvm::Type *block_type); /* returns the llvm::Type corresponding to the type of the result of calling createTerm on the specified pattern. */ diff --git a/include/kllvm/codegen/Debug.h b/include/kllvm/codegen/Debug.h index 48e3be823..3a7a38345 100644 --- a/include/kllvm/codegen/Debug.h +++ b/include/kllvm/codegen/Debug.h @@ -38,7 +38,8 @@ llvm::DIType *get_long_debug_type(); llvm::DIType *get_void_debug_type(); llvm::DIType *get_bool_debug_type(); llvm::DIType *get_short_debug_type(); -llvm::DIType *get_pointer_debug_type(llvm::DIType *, std::string const &type_name); +llvm::DIType * +get_pointer_debug_type(llvm::DIType *, std::string const &type_name); llvm::DIType * get_array_debug_type(llvm::DIType *ty, size_t len, llvm::Align align); llvm::DIType *get_char_ptr_debug_type(); diff --git a/include/kllvm/codegen/ProofEvent.h b/include/kllvm/codegen/ProofEvent.h index 9c156cf9a..647ecea26 100644 --- a/include/kllvm/codegen/ProofEvent.h +++ b/include/kllvm/codegen/ProofEvent.h @@ -65,7 +65,8 @@ class proof_event { * Emit a call that will serialize `value` to the specified `outputFile`. */ llvm::CallInst *emit_write_uint64( - llvm::Value *output_file, uint64_t value, llvm::BasicBlock *insert_at_end); + llvm::Value *output_file, uint64_t value, + llvm::BasicBlock *insert_at_end); /* * Emit a call that will serialize `str` to the specified `outputFile`. diff --git a/include/runtime/header.h b/include/runtime/header.h index 75dcbf8d4..8853f7e5d 100644 --- a/include/runtime/header.h +++ b/include/runtime/header.h @@ -388,7 +388,8 @@ void print_set( writer *, set *, char const *, char const *, char const *, void *); void print_list( writer *, list *, char const *, char const *, char const *, void *); -void visit_children(block *subject, writer *file, visitor *printer, void *state); +void visit_children( + block *subject, writer *file, visitor *printer, void *state); stringbuffer *hook_BUFFER_empty(void); stringbuffer *hook_BUFFER_concat(stringbuffer *buf, string *s); diff --git a/lib/ast/definition.cpp b/lib/ast/definition.cpp index 8125197d4..af7851c7d 100644 --- a/lib/ast/definition.cpp +++ b/lib/ast/definition.cpp @@ -11,8 +11,8 @@ namespace { template std::unordered_map, Hash, Equal> transitive_closure(std::unordered_map< - Elem *, std::unordered_set, Hash, Equal> - relations) { + Elem *, std::unordered_set, Hash, Equal> + relations) { bool dirty = false; do { dirty = false; @@ -54,13 +54,16 @@ void kore_definition::add_module(sptr module) { sort_declarations_.insert({sort_decl->get_name(), sort_decl}); auto sort = kore_composite_sort::create(sort_decl->get_name()); } else if ( - auto *symbol_decl = dynamic_cast(decl.get())) { + auto *symbol_decl + = dynamic_cast(decl.get())) { symbol_declarations_.insert( {symbol_decl->get_symbol()->get_name(), symbol_decl}); } else if ( auto *alias_decl = dynamic_cast(decl.get())) { - alias_declarations_.insert({alias_decl->get_symbol()->get_name(), alias_decl}); - } else if (auto *axiom = dynamic_cast(decl.get())) { + alias_declarations_.insert( + {alias_decl->get_symbol()->get_name(), alias_decl}); + } else if ( + auto *axiom = dynamic_cast(decl.get())) { axioms_.push_back(axiom); } } @@ -85,8 +88,10 @@ SubsortMap kore_definition::get_subsorts() const { for (auto *axiom : axioms_) { if (axiom->attributes().contains(attribute_set::key::Subsort)) { auto const &att = axiom->attributes().get(attribute_set::key::Subsort); - auto const &inner_sort = att->get_constructor()->get_formal_arguments()[0]; - auto const &outer_sort = att->get_constructor()->get_formal_arguments()[1]; + auto const &inner_sort + = att->get_constructor()->get_formal_arguments()[0]; + auto const &outer_sort + = att->get_constructor()->get_formal_arguments()[1]; subsorts[inner_sort.get()].insert(outer_sort.get()); } } @@ -102,11 +107,11 @@ SymbolMap kore_definition::get_overloads() const { auto const &att = axiom->attributes().get(attribute_set::key::SymbolOverload); auto *inner_symbol = std::dynamic_pointer_cast( - att->get_arguments()[1]) - ->get_constructor(); + att->get_arguments()[1]) + ->get_constructor(); auto *outer_symbol = std::dynamic_pointer_cast( - att->get_arguments()[0]) - ->get_constructor(); + att->get_arguments()[0]) + ->get_constructor(); overloads[inner_symbol].insert(outer_symbol); } } @@ -128,7 +133,8 @@ void kore_definition::preprocess() { attribute_set::key::FreshGenerator)) { auto sort = decl.second->get_symbol()->get_sort(); if (sort->is_concrete()) { - fresh_functions_[dynamic_cast(sort.get())->get_name()] + fresh_functions_[dynamic_cast(sort.get()) + ->get_name()] = decl.second->get_symbol(); } } @@ -165,7 +171,8 @@ void kore_definition::preprocess() { } uint32_t next_symbol = 0; uint16_t next_layout = 1; - auto instantiations = std::unordered_map{}; + auto instantiations + = std::unordered_map{}; auto layouts = std::unordered_map{}; auto variables = std::unordered_map>{}; @@ -198,14 +205,16 @@ void kore_definition::preprocess() { for (auto const &sort : symbol->get_arguments()) { if (sort->is_concrete()) { hooked_sorts_[dynamic_cast(sort.get()) - ->get_category(this)] + ->get_category(this)] = std::dynamic_pointer_cast(sort); } } if (symbol->get_sort()->is_concrete()) { - hooked_sorts_[dynamic_cast(symbol->get_sort().get()) - ->get_category(this)] - = std::dynamic_pointer_cast(symbol->get_sort()); + hooked_sorts_[dynamic_cast( + symbol->get_sort().get()) + ->get_category(this)] + = std::dynamic_pointer_cast( + symbol->get_sort()); } if (!symbol->is_concrete()) { if (symbol->is_polymorphic()) { diff --git a/lib/codegen/CreateStaticTerm.cpp b/lib/codegen/CreateStaticTerm.cpp index 3a0c6f0ee..8e224bf47 100644 --- a/lib/codegen/CreateStaticTerm.cpp +++ b/lib/codegen/CreateStaticTerm.cpp @@ -45,16 +45,16 @@ llvm::Constant *create_static_term::not_injection_case( llvm::StructType *block_header_type = llvm::StructType::getTypeByName( module_->getContext(), blockheader_struct); - uint64_t header_val - = get_block_header_val(module_, symbol, block_type) | NOT_YOUNG_OBJECT_BIT; + uint64_t header_val = get_block_header_val(module_, symbol, block_type) + | NOT_YOUNG_OBJECT_BIT; llvm::Constant *block_header = llvm::ConstantStruct::get( block_header_type, llvm::ConstantInt::get( llvm::Type::getInt64Ty(module_->getContext()), header_val)); block_vals.push_back(block_header); - llvm::ArrayType *empty_array_type - = llvm::ArrayType::get(llvm::Type::getInt64Ty(module_->getContext()), 0); + llvm::ArrayType *empty_array_type = llvm::ArrayType::get( + llvm::Type::getInt64Ty(module_->getContext()), 0); block_vals.push_back(llvm::ConstantArray::get( empty_array_type, llvm::ArrayRef())); @@ -76,9 +76,10 @@ llvm::Constant *create_static_term::not_injection_case( std::vector idxs = {llvm::ConstantInt::get(llvm::Type::getInt64Ty(ctx_), 0)}; return llvm::ConstantExpr::getBitCast( - llvm::ConstantExpr::getInBoundsGetElementPtr(block_type, global_var, idxs), - llvm::PointerType::getUnqual( - llvm::StructType::getTypeByName(module_->getContext(), block_struct))); + llvm::ConstantExpr::getInBoundsGetElementPtr( + block_type, global_var, idxs), + llvm::PointerType::getUnqual(llvm::StructType::getTypeByName( + module_->getContext(), block_struct))); } std::pair @@ -92,12 +93,13 @@ create_static_term::operator()(kore_pattern *pattern) { auto *str_pattern = dynamic_cast( constructor->get_arguments()[0].get()); return std::make_pair( - create_token(sort->get_category(definition_), str_pattern->get_contents()), + create_token( + sort->get_category(definition_), str_pattern->get_contents()), false); } if (symbol->get_arguments().empty()) { - llvm::StructType *block_type - = llvm::StructType::getTypeByName(module_->getContext(), block_struct); + llvm::StructType *block_type = llvm::StructType::getTypeByName( + module_->getContext(), block_struct); llvm::Constant *cast = llvm::ConstantExpr::getIntToPtr( llvm::ConstantInt::get( llvm::Type::getInt64Ty(ctx_), @@ -154,8 +156,8 @@ create_static_term::create_token(value_type sort, std::string contents) { int sign = mpz_sgn(value); llvm::ArrayType *limbs_type = llvm::ArrayType::get(llvm::Type::getInt64Ty(ctx_), size); - llvm::Constant *limbs - = module_->getOrInsertGlobal("int_" + contents + "_limbs", limbs_type); + llvm::Constant *limbs = module_->getOrInsertGlobal( + "int_" + contents + "_limbs", limbs_type); auto *limbs_var = llvm::dyn_cast(limbs); std::vector allocd_limbs; for (size_t i = 0; i < size; i++) { @@ -180,7 +182,8 @@ create_static_term::create_token(value_type sort, std::string contents) { module_->getContext(), int_wrapper_struct), hdr, llvm::ConstantStruct::get( - llvm::StructType::getTypeByName(module_->getContext(), int_struct), + llvm::StructType::getTypeByName( + module_->getContext(), int_struct), num_limbs, mp_size, llvm::ConstantExpr::getPointerCast( limbs_var, llvm::Type::getInt64PtrTy(ctx_))))); @@ -319,8 +322,8 @@ create_static_term::create_token(value_type sort, std::string contents) { // the correct gc bit. llvm::Constant *block_header = llvm::ConstantStruct::get( block_header_type, llvm::ConstantInt::get( - llvm::Type::getInt64Ty(ctx_), - contents.size() | NOT_YOUNG_OBJECT_BIT)); + llvm::Type::getInt64Ty(ctx_), + contents.size() | NOT_YOUNG_OBJECT_BIT)); global_var->setInitializer(llvm::ConstantStruct::get( string_type, block_header, llvm::ConstantDataArray::getString(ctx_, contents, false))); diff --git a/lib/codegen/Debug.cpp b/lib/codegen/Debug.cpp index 717cf01dd..a18b681fc 100644 --- a/lib/codegen/Debug.cpp +++ b/lib/codegen/Debug.cpp @@ -48,8 +48,8 @@ void init_debug_info(llvm::Module *module, std::string const &filename) { // https://github.com/runtimeverification/k/issues/2637 // https://llvm.org/doxygen/classllvm_1_1DIBuilder.html dbg_cu = dbg->createCompileUnit( - llvm::dwarf::DW_LANG_C, dbg_file, "llvm-kompile-codegen", false, "", 0, "", - llvm::DICompileUnit::DebugEmissionKind::FullDebug, 0, false, false, + llvm::dwarf::DW_LANG_C, dbg_file, "llvm-kompile-codegen", false, "", 0, + "", llvm::DICompileUnit::DebugEmissionKind::FullDebug, 0, false, false, llvm::DICompileUnit::DebugNameTableKind::None); } @@ -64,7 +64,8 @@ void init_debug_function( if (!dbg) { return; } - auto *unit = dbg->createFile(dbg_file->getFilename(), dbg_file->getDirectory()); + auto *unit + = dbg->createFile(dbg_file->getFilename(), dbg_file->getDirectory()); llvm::DIScope *f_context = unit; dbg_sp = dbg->createFunction( f_context, name, name, unit, dbg_line, type, dbg_line, @@ -79,8 +80,8 @@ void init_debug_param( return; } llvm::DILocalVariable *dbg_var = dbg->createParameterVariable( - dbg_sp, name, arg_no + 1, dbg_file, dbg_line, get_debug_type(type, type_name), - true); + dbg_sp, name, arg_no + 1, dbg_file, dbg_line, + get_debug_type(type, type_name), true); dbg->insertDbgValueIntrinsic( func->arg_begin() + arg_no, dbg_var, dbg->createExpression(), llvm::DILocation::get(func->getContext(), dbg_line, dbg_column, dbg_sp), @@ -106,10 +107,11 @@ void init_debug_axiom(attribute_set const &att) { reset_debug_loc(); return; } - kore_composite_pattern *source_att = att.get(attribute_set::key::Source).get(); + kore_composite_pattern *source_att + = att.get(attribute_set::key::Source).get(); assert(source_att->get_arguments().size() == 1); - auto *str_pattern - = dynamic_cast(source_att->get_arguments()[0].get()); + auto *str_pattern = dynamic_cast( + source_att->get_arguments()[0].get()); std::string source = str_pattern->get_contents(); if (!att.contains(attribute_set::key::Location)) { reset_debug_loc(); @@ -118,8 +120,8 @@ void init_debug_axiom(attribute_set const &att) { kore_composite_pattern *location_att = att.get(attribute_set::key::Location).get(); assert(location_att->get_arguments().size() == 1); - auto *str_pattern2 - = dynamic_cast(location_att->get_arguments()[0].get()); + auto *str_pattern2 = dynamic_cast( + location_att->get_arguments()[0].get()); std::string location = str_pattern2->get_contents(); source = source.substr(7, source.length() - 8); size_t first_comma = location.find_first_of(','); @@ -143,7 +145,8 @@ llvm::DIType *get_forward_decl(std::string const &name) { if (!dbg) { return nullptr; } - auto *unit = dbg->createFile(dbg_file->getFilename(), dbg_file->getDirectory()); + auto *unit + = dbg->createFile(dbg_file->getFilename(), dbg_file->getDirectory()); return dbg->createForwardDecl( llvm::dwarf::DW_TAG_structure_type, name, dbg_cu, unit, 0); } @@ -181,7 +184,8 @@ llvm::DIType *get_debug_type(value_type type, std::string const &type_name) { types[type_name] = map; return map; case sort_category::RangeMap: - rangemap = get_pointer_debug_type(get_forward_decl(rangemap_struct), type_name); + rangemap + = get_pointer_debug_type(get_forward_decl(rangemap_struct), type_name); types[type_name] = rangemap; return rangemap; case sort_category::List: @@ -197,7 +201,8 @@ llvm::DIType *get_debug_type(value_type type, std::string const &type_name) { types[type_name] = integer; return integer; case sort_category::Float: - floating = get_pointer_debug_type(get_forward_decl(float_struct), type_name); + floating + = get_pointer_debug_type(get_forward_decl(float_struct), type_name); types[type_name] = floating; return floating; case sort_category::StringBuffer: @@ -302,7 +307,7 @@ void set_debug_loc(llvm::Instruction *instr) { if (!dbg) { return; } - instr->setDebugLoc(llvm::DebugLoc( - llvm::DILocation::get(instr->getContext(), dbg_line, dbg_column, dbg_sp))); + instr->setDebugLoc(llvm::DebugLoc(llvm::DILocation::get( + instr->getContext(), dbg_line, dbg_column, dbg_sp))); } } // namespace kllvm diff --git a/lib/codegen/ProofEvent.cpp b/lib/codegen/ProofEvent.cpp index f4a1080b5..3fac99829 100644 --- a/lib/codegen/ProofEvent.cpp +++ b/lib/codegen/ProofEvent.cpp @@ -78,8 +78,8 @@ llvm::CallInst *proof_event::emit_serialize_configuration( auto *func_ty = llvm::FunctionType::get( void_ty, {i8_ptr_ty, block_ty, i1_ty, i1_ty}, false); - auto *serialize - = get_or_insert_function(module_, "serialize_configuration_to_file", func_ty); + auto *serialize = get_or_insert_function( + module_, "serialize_configuration_to_file", func_ty); return llvm::CallInst::Create( serialize, @@ -100,7 +100,8 @@ llvm::CallInst *proof_event::emit_write_uint64( auto *i64_value = llvm::ConstantInt::get(i64_ptr_ty, value); - return llvm::CallInst::Create(func, {output_file, i64_value}, "", insert_at_end); + return llvm::CallInst::Create( + func, {output_file, i64_value}, "", insert_at_end); } llvm::CallInst *proof_event::emit_write_string( @@ -114,7 +115,8 @@ llvm::CallInst *proof_event::emit_write_string( auto *func_ty = llvm::FunctionType::get(void_ty, {i8_ptr_ty, i8_ptr_ty}, false); - auto *print = get_or_insert_function(module_, "print_variable_to_file", func_ty); + auto *print + = get_or_insert_function(module_, "print_variable_to_file", func_ty); auto *varname = b.CreateGlobalStringPtr(str, "", 0, module_); return b.CreateCall(print, {output_file, varname}); @@ -131,8 +133,10 @@ llvm::BinaryOperator *proof_event::emit_no_op(llvm::BasicBlock *insert_at_end) { llvm::LoadInst * proof_event::emit_get_output_file_name(llvm::BasicBlock *insert_at_end) { auto *i8_ptr_ty = llvm::Type::getInt8PtrTy(ctx_); - auto *file_name_pointer = module_->getOrInsertGlobal("output_file", i8_ptr_ty); - return new llvm::LoadInst(i8_ptr_ty, file_name_pointer, "output", insert_at_end); + auto *file_name_pointer + = module_->getOrInsertGlobal("output_file", i8_ptr_ty); + return new llvm::LoadInst( + i8_ptr_ty, file_name_pointer, "output", insert_at_end); } std::pair proof_event::proof_branch( @@ -151,7 +155,8 @@ std::pair proof_event::proof_branch( emit_no_op(merge_block); - llvm::BranchInst::Create(true_block, merge_block, proof_output, insert_at_end); + llvm::BranchInst::Create( + true_block, merge_block, proof_output, insert_at_end); return {true_block, merge_block}; } diff --git a/lib/printer/addBrackets.cpp b/lib/printer/addBrackets.cpp index 13d41d80c..fe3b0fbdb 100644 --- a/lib/printer/addBrackets.cpp +++ b/lib/printer/addBrackets.cpp @@ -198,8 +198,8 @@ bool less_than_eq(pretty_print_data const &data, kore_sort *s1, kore_sort *s2) { || (data.subsorts.contains(s1) && data.subsorts.at(s1).contains(s2)); } -sptr -get_arg_sort(kore_symbol *symbol, int position, sptr first_arg_sort) { +sptr get_arg_sort( + kore_symbol *symbol, int position, sptr first_arg_sort) { if (!symbol->is_builtin()) { return symbol->get_arguments()[position]; } @@ -288,9 +288,9 @@ bool is_priority_wrong( std::string inner_name = inner->get_constructor()->get_name(); kore_sort *inner_sort = get_return_sort(inner).get(); kore_sort *outer_sort = get_arg_sort( - outer->get_constructor(), position, - outer->get_arguments()[0]->get_sort()) - .get(); + outer->get_constructor(), position, + outer->get_arguments()[0]->get_sort()) + .get(); if (!less_than_eq(data, inner_sort, outer_sort)) { return true; } @@ -395,8 +395,10 @@ bool requires_bracket_with_simple_algorithm( } if ((inner_fixity & BareLeft) && left_capture != nullptr) { - bool inverse_priority = is_priority_wrong(composite, left_capture, 0, data); - auto left_capture_fixity = get_fixity(left_capture->get_constructor(), data); + bool inverse_priority + = is_priority_wrong(composite, left_capture, 0, data); + auto left_capture_fixity + = get_fixity(left_capture->get_constructor(), data); if (!inverse_priority && (left_capture_fixity & BareRight)) { return true; } @@ -426,7 +428,8 @@ sptr add_brackets( outer->get_arguments()[0]->get_sort()); sptr inner_sort = get_return_sort(inner.get()); for (auto const &entry : data.brackets) { - bool is_correct_outer_sort = less_than_eq(data, entry.first, outer_sort.get()); + bool is_correct_outer_sort + = less_than_eq(data, entry.first, outer_sort.get()); if (is_correct_outer_sort) { for (kore_symbol *s : entry.second) { bool is_correct_inner_sort = less_than_eq( diff --git a/lib/printer/printer.cpp b/lib/printer/printer.cpp index ba51a27f3..821030a7f 100644 --- a/lib/printer/printer.cpp +++ b/lib/printer/printer.cpp @@ -312,7 +312,7 @@ preprocessed_print_data get_print_data( pretty_print_data data = {formats, colors, terminals, priorities, left_assoc, right_assoc, - hooks, brackets, assocs, comms, subsorts, has_color}; + hooks, brackets, assocs, comms, subsorts, has_color}; return {data, overloads}; } diff --git a/runtime/alloc/arena.cpp b/runtime/alloc/arena.cpp index 5d95cc8e5..284c8fd38 100644 --- a/runtime/alloc/arena.cpp +++ b/runtime/alloc/arena.cpp @@ -42,7 +42,8 @@ get_arena_collection_semispace_id(const struct arena *arena) { return ~arena->allocation_semispace_id; } -__attribute__((always_inline)) char get_arena_semispace_id_of_object(void *ptr) { +__attribute__((always_inline)) char +get_arena_semispace_id_of_object(void *ptr) { return mem_block_header(ptr)->semispace; } @@ -174,7 +175,8 @@ __attribute__((always_inline)) void arena_clear(struct arena *arena) { = arena->first_block ? arena->first_block + BLOCK_SIZE : nullptr; } -__attribute__((always_inline)) char *arena_start_ptr(const struct arena *arena) { +__attribute__((always_inline)) char * +arena_start_ptr(const struct arena *arena) { return arena->first_block ? arena->first_block + sizeof(memory_block_header) : nullptr; } diff --git a/runtime/arithmetic/float.cpp b/runtime/arithmetic/float.cpp index ab336cc16..b79dd1e67 100644 --- a/runtime/arithmetic/float.cpp +++ b/runtime/arithmetic/float.cpp @@ -91,7 +91,8 @@ SortFloat hook_FLOAT_round(SortFloat a, SortInt prec, SortInt exp) { } unsigned long uprec = mpz_get_ui(prec); if (!mpz_fits_ulong_p(exp)) { - KLLVM_HOOK_INVALID_ARGUMENT("Exponent out of range: {}", int_to_string(exp)); + KLLVM_HOOK_INVALID_ARGUMENT( + "Exponent out of range: {}", int_to_string(exp)); } unsigned long uexp = mpz_get_ui(exp); floating result[1]; @@ -118,7 +119,8 @@ SortFloat hook_FLOAT_int2float(SortInt a, SortInt prec, SortInt exp) { } unsigned long uprec = mpz_get_ui(prec); if (!mpz_fits_ulong_p(exp)) { - KLLVM_HOOK_INVALID_ARGUMENT("Exponent out of range: {}", int_to_string(exp)); + KLLVM_HOOK_INVALID_ARGUMENT( + "Exponent out of range: {}", int_to_string(exp)); } unsigned long uexp = mpz_get_ui(exp); floating result[1]; @@ -272,7 +274,8 @@ SortFloat hook_FLOAT_maxValue(SortInt prec, SortInt exp) { } unsigned long uprec = mpz_get_ui(prec); if (!mpz_fits_ulong_p(exp)) { - KLLVM_HOOK_INVALID_ARGUMENT("Exponent out of range: {}", int_to_string(exp)); + KLLVM_HOOK_INVALID_ARGUMENT( + "Exponent out of range: {}", int_to_string(exp)); } unsigned long uexp = mpz_get_ui(exp); floating result[1]; @@ -290,7 +293,8 @@ SortFloat hook_FLOAT_minValue(SortInt prec, SortInt exp) { } unsigned long uprec = mpz_get_ui(prec); if (!mpz_fits_ulong_p(exp)) { - KLLVM_HOOK_INVALID_ARGUMENT("Exponent out of range: {}", int_to_string(exp)); + KLLVM_HOOK_INVALID_ARGUMENT( + "Exponent out of range: {}", int_to_string(exp)); } unsigned long uexp = mpz_get_ui(exp); floating result[1]; @@ -467,7 +471,8 @@ SortFloat hook_FLOAT_rat2float( } unsigned long uprec = mpz_get_ui(prec); if (!mpz_fits_ulong_p(exp)) { - KLLVM_HOOK_INVALID_ARGUMENT("Exponent out of range: {}", int_to_string(exp)); + KLLVM_HOOK_INVALID_ARGUMENT( + "Exponent out of range: {}", int_to_string(exp)); } unsigned long uexp = mpz_get_ui(exp); diff --git a/runtime/collections/maps.cpp b/runtime/collections/maps.cpp index f24fccee4..98afcd0cf 100644 --- a/runtime/collections/maps.cpp +++ b/runtime/collections/maps.cpp @@ -216,7 +216,8 @@ void print_map( auto entry = *iter; print_configuration_internal(file, entry.first, arg_sorts[0], false, state); sfprintf(file, ","); - print_configuration_internal(file, entry.second, arg_sorts[1], false, state); + print_configuration_internal( + file, entry.second, arg_sorts[1], false, state); sfprintf(file, ")"); } sfprintf(file, "))"); diff --git a/runtime/collections/rangemaps.cpp b/runtime/collections/rangemaps.cpp index 64bac7dc8..5e07dda5e 100644 --- a/runtime/collections/rangemaps.cpp +++ b/runtime/collections/rangemaps.cpp @@ -282,7 +282,8 @@ void print_range_map( print_configuration_internal( file, entry.first.end(), "SortKItem{}", false, state); sfprintf(file, "),"); - print_configuration_internal(file, entry.second, arg_sorts[1], false, state); + print_configuration_internal( + file, entry.second, arg_sorts[1], false, state); sfprintf(file, ")"); } sfprintf(file, "))"); diff --git a/runtime/io/io.cpp b/runtime/io/io.cpp index 8018284b0..ddc2837dd 100644 --- a/runtime/io/io.cpp +++ b/runtime/io/io.cpp @@ -28,8 +28,8 @@ extern char kompiled_directory; char *get_terminated_string(string *str); -static blockheader kseq_header - = {get_block_header_for_symbol((uint64_t)get_tag_for_symbol_name("kseq{}"))}; +static blockheader kseq_header = { + get_block_header_for_symbol((uint64_t)get_tag_for_symbol_name("kseq{}"))}; static std::map log_files; @@ -329,7 +329,8 @@ SortIOString hook_IO_read(SortInt i, SortInt len) { int fd = mpz_get_si(i); size_t length = mpz_get_ui(len); - auto *result = static_cast(kore_alloc_token(sizeof(string) + length)); + auto *result + = static_cast(kore_alloc_token(sizeof(string) + length)); int bytes = read(fd, &(result->data), length); if (-1 == bytes) { diff --git a/runtime/json/json.cpp b/runtime/json/json.cpp index 251808061..29c7d03cd 100644 --- a/runtime/json/json.cpp +++ b/runtime/json/json.cpp @@ -55,14 +55,15 @@ struct jsonmember { block *val; }; -static blockheader kseq_header - = {get_block_header_for_symbol((uint64_t)get_tag_for_symbol_name("kseq{}"))}; +static blockheader kseq_header = { + get_block_header_for_symbol((uint64_t)get_tag_for_symbol_name("kseq{}"))}; #define GET_HEADER(name, symbol) \ static struct blockheader name() { \ static struct blockheader hdr = {(uint64_t)-1}; \ if (hdr.hdr == -1) { \ - hdr = get_block_header_for_symbol((uint64_t)get_tag_for_symbol_name(symbol)); \ + hdr = get_block_header_for_symbol( \ + (uint64_t)get_tag_for_symbol_name(symbol)); \ } \ return hdr; \ } @@ -80,7 +81,7 @@ GET_HEADER(listWrapHdr, "LblJSONList{}"); static block *name() { \ static uint64_t tag = (uint64_t)-1; \ if (tag == -1) { \ - tag = (uint64_t)leaf_block(get_tag_for_symbol_name(symbol)); \ + tag = (uint64_t)leaf_block(get_tag_for_symbol_name(symbol)); \ } \ return (block *)tag; \ } diff --git a/runtime/strings/bytes.cpp b/runtime/strings/bytes.cpp index aefb97e23..74cc5ffdc 100644 --- a/runtime/strings/bytes.cpp +++ b/runtime/strings/bytes.cpp @@ -98,8 +98,9 @@ hook_BYTES_int2bytes(SortInt len, SortInt i, SortEndianness endianness_ptr) { mpz_init(twos); extract(twos, i, 0, len_long * 8); size_t size_in_bytes = (mpz_sizeinbase(twos, 2) + 7) / 8; - void *start = result->data - + (endianness == tag_big_endian() ? len_long - size_in_bytes : 0); + void *start + = result->data + + (endianness == tag_big_endian() ? len_long - size_in_bytes : 0); mpz_export(start, nullptr, order, 1, 0, 0, twos); mpz_clear(twos); return result; diff --git a/runtime/strings/strings.cpp b/runtime/strings/strings.cpp index 3227b7ea6..5c142c408 100644 --- a/runtime/strings/strings.cpp +++ b/runtime/strings/strings.cpp @@ -364,7 +364,8 @@ hook_STRING_countAllOccurrences(SortString haystack, SortString needle) { SortString hook_STRING_transcode( SortString input, SortString input_charset, SortString output_charset) { iconv_t converter = iconv_open( - get_terminated_string(output_charset), get_terminated_string(input_charset)); + get_terminated_string(output_charset), + get_terminated_string(input_charset)); char *inbuf = input->data; size_t inbytesleft = len(input); size_t outbytesleft = inbytesleft * 4; @@ -425,8 +426,8 @@ hook_BUFFER_concat_raw(stringbuffer *buf, char const *data, uint64_t n) { new_contents = static_cast( kore_alloc_token_old(sizeof(string) + new_capacity)); } else { - new_contents - = static_cast(kore_alloc_token(sizeof(string) + new_capacity)); + new_contents = static_cast( + kore_alloc_token(sizeof(string) + new_capacity)); } memcpy(new_contents->data, buf->contents->data, buf->strlen); buf->contents = new_contents; diff --git a/runtime/util/ConfigurationParser.cpp b/runtime/util/ConfigurationParser.cpp index 7402c4008..2f74372e2 100644 --- a/runtime/util/ConfigurationParser.cpp +++ b/runtime/util/ConfigurationParser.cpp @@ -57,7 +57,8 @@ static uint32_t get_tag_for_symbol(kore_symbol const &symbol) { return get_tag_for_symbol_name(name.c_str()); } -void *construct_composite_pattern(uint32_t tag, std::vector &arguments) { +void * +construct_composite_pattern(uint32_t tag, std::vector &arguments) { if (is_symbol_a_function(tag)) { return evaluate_function_symbol(tag, arguments.data()); } @@ -266,7 +267,8 @@ block *parse_configuration(char const *filename) { // InitialConfiguration->print(std::cout); // Allocate the llvm KORE datastructures for the configuration - auto *b = (block *)construct_initial_configuration(initial_configuration.get()); + auto *b + = (block *)construct_initial_configuration(initial_configuration.get()); deallocate_s_ptr_kore_pattern(std::move(initial_configuration)); return b; } diff --git a/runtime/util/ConfigurationPrinter.cpp b/runtime/util/ConfigurationPrinter.cpp index 4e02e0f12..a9fd952b7 100644 --- a/runtime/util/ConfigurationPrinter.cpp +++ b/runtime/util/ConfigurationPrinter.cpp @@ -268,9 +268,10 @@ extern "C" void print_match_result( print_sorted_configuration_to_file( subject, (block *)match_log[i].subject, match_log[i].sort); } else { - auto *subject_sort - = debug_print_term((block *)match_log[i].subject, match_log[i].sort); - auto str_subject_sort = std::string(subject_sort->data, len(subject_sort)); + auto *subject_sort = debug_print_term( + (block *)match_log[i].subject, match_log[i].sort); + auto str_subject_sort + = std::string(subject_sort->data, len(subject_sort)); subject_file.ofstream() << str_subject_sort << std::endl; } kllvm::print_kore( @@ -284,7 +285,8 @@ extern "C" void print_match_result( for (int j = 0; j < match_log[i].args.size(); j += 2) { auto *type_name = static_cast(match_log[i].args[j + 1]); - print_value_of_type(os, definition_path, match_log[i].args[j], type_name); + print_value_of_type( + os, definition_path, match_log[i].args[j], type_name); if (j + 2 != match_log[i].args.size()) { os << ", "; } diff --git a/runtime/util/ConfigurationSerializer.cpp b/runtime/util/ConfigurationSerializer.cpp index dc70afb80..8b2b47077 100644 --- a/runtime/util/ConfigurationSerializer.cpp +++ b/runtime/util/ConfigurationSerializer.cpp @@ -367,7 +367,8 @@ void serialize_configuration_internal( } } - emit_symbol(state.instance, name.c_str(), get_symbol_arity(tag), sorts.size()); + emit_symbol( + state.instance, name.c_str(), get_symbol_arity(tag), sorts.size()); } else { emit_symbol(state.instance, symbol, get_symbol_arity(tag)); } @@ -410,7 +411,8 @@ void serialize_configuration_to_file( FILE *file, block *subject, bool emit_size, bool use_intern) { char *data = nullptr; size_t size = 0; - serialize_configuration(subject, nullptr, &data, &size, emit_size, use_intern); + serialize_configuration( + subject, nullptr, &data, &size, emit_size, use_intern); fwrite(data, 1, size, file); @@ -474,7 +476,8 @@ sorted_term_to_kore_pattern(block *subject, char const *sort) { char *data_out = nullptr; size_t size_out = 0; - serialize_configuration(term, "SortKItem{}", &data_out, &size_out, true, true); + serialize_configuration( + term, "SortKItem{}", &data_out, &size_out, true, true); auto result = deserialize_pattern(data_out, data_out + size_out); free(data_out); diff --git a/runtime/util/match_log.cpp b/runtime/util/match_log.cpp index 854d5899d..88c5386a1 100644 --- a/runtime/util/match_log.cpp +++ b/runtime/util/match_log.cpp @@ -40,7 +40,8 @@ void add_match_success(void) { nullptr}); } -void add_match_fail_reason(void *subject, char const *pattern, char const *sort) { +void add_match_fail_reason( + void *subject, char const *pattern, char const *sort) { match_logs.push_back( {match_log::FAIL, nullptr, nullptr, nullptr, {}, pattern, subject, sort}); } @@ -63,8 +64,8 @@ void add_match_function( } match_logs.push_back( - {match_log::FUNCTION, function, debug_name, result, args, nullptr, nullptr, - nullptr}); + {match_log::FUNCTION, function, debug_name, result, args, nullptr, + nullptr, nullptr}); va_end(ap); // NOLINTEND(*-vararg) diff --git a/tools/k-rule-apply/auxiliar.h b/tools/k-rule-apply/auxiliar.h index 34ff87744..36311ab90 100644 --- a/tools/k-rule-apply/auxiliar.h +++ b/tools/k-rule-apply/auxiliar.h @@ -18,11 +18,13 @@ void *construct_initial_configuration(kore_pattern const *); void reset_match_reason(); match_log *getmatch_log(); size_t getmatch_log_size(); -void print_match_result(std::ostream &, match_log *, size_t, std::string const &); +void print_match_result( + std::ostream &, match_log *, size_t, std::string const &); void init_static_objects(); } -void *construct_initial_configuration(kore_pattern const *pattern, void *handle) { +void * +construct_initial_configuration(kore_pattern const *pattern, void *handle) { void *funcPtr = dlsym(handle, "construct_initial_configuration"); if (funcPtr == NULL) { return NULL; diff --git a/tools/k-rule-apply/main.cpp b/tools/k-rule-apply/main.cpp index 9558c6b14..2afbc456d 100644 --- a/tools/k-rule-apply/main.cpp +++ b/tools/k-rule-apply/main.cpp @@ -80,7 +80,8 @@ int main(int argc, char **argv) { reset_match_reason(handle); init_static_objects(handle); - auto *b = construct_initial_configuration(initial_configuration.get(), handle); + auto *b + = construct_initial_configuration(initial_configuration.get(), handle); if (b == nullptr) { std::cerr << "Error: " << dlerror() << "\n"; return EXIT_FAILURE; @@ -99,7 +100,8 @@ int main(int argc, char **argv) { return EXIT_FAILURE; } - print_match_result(std::cout, (match_log *)log, log_size, kompiled_dir, handle); + print_match_result( + std::cout, (match_log *)log, log_size, kompiled_dir, handle); dlclose(handle); return 0; diff --git a/tools/k-rule-find/main.cpp b/tools/k-rule-find/main.cpp index 4af7b68b5..7c741fb14 100644 --- a/tools/k-rule-find/main.cpp +++ b/tools/k-rule-find/main.cpp @@ -32,8 +32,8 @@ std::string get_source(kore_axiom_declaration *axiom) { auto *source_att = axiom->attributes().get(attribute_set::key::Source).get(); assert(source_att->get_arguments().size() == 1); - auto *str_pattern - = dynamic_cast(source_att->get_arguments()[0].get()); + auto *str_pattern = dynamic_cast( + source_att->get_arguments()[0].get()); return str_pattern->get_contents(); } @@ -42,8 +42,8 @@ location get_location(kore_axiom_declaration *axiom) { = axiom->attributes().get(attribute_set::key::Location).get(); assert(location_att->get_arguments().size() == 1); - auto *str_pattern - = dynamic_cast(location_att->get_arguments()[0].get()); + auto *str_pattern = dynamic_cast( + location_att->get_arguments()[0].get()); std::string location = str_pattern->get_contents(); size_t l_paren = location.find_first_of('('); diff --git a/tools/llvm-kompile-codegen/main.cpp b/tools/llvm-kompile-codegen/main.cpp index 0952ae272..852210e29 100644 --- a/tools/llvm-kompile-codegen/main.cpp +++ b/tools/llvm-kompile-codegen/main.cpp @@ -204,7 +204,8 @@ int main(int argc, char **argv) { auto *func_dt = parse_yamldecision_tree( mod.get(), filename, definition->get_all_symbols(), definition->get_hooked_sorts()); - make_eval_function(decl->get_symbol(), definition.get(), mod.get(), func_dt); + make_eval_function( + decl->get_symbol(), definition.get(), mod.get(), func_dt); } else if (decl->is_anywhere()) { auto filename = get_indexed_filename(index, decl); auto *func_dt = parse_yamldecision_tree( diff --git a/unittests/runtime-io/io.cpp b/unittests/runtime-io/io.cpp index 638dc7683..a04a9682e 100644 --- a/unittests/runtime-io/io.cpp +++ b/unittests/runtime-io/io.cpp @@ -14,7 +14,8 @@ #define KCHAR char -void *construct_composite_pattern(uint32_t tag, std::vector &arguments) { +void * +construct_composite_pattern(uint32_t tag, std::vector &arguments) { return nullptr; } @@ -190,7 +191,8 @@ BOOST_AUTO_TEST_CASE(tell) { get_tag_for_symbol_name("inj{SortIOError{}, SortKItem{}}")) .hdr); BOOST_CHECK_EQUAL( - (uint64_t) * (b->children), ERRBLOCK(get_tag_for_symbol_name(GETTAG(EBADF)))); + (uint64_t) * (b->children), + ERRBLOCK(get_tag_for_symbol_name(GETTAG(EBADF)))); } BOOST_AUTO_TEST_CASE(getc) { @@ -242,7 +244,8 @@ BOOST_AUTO_TEST_CASE(getc) { char const *temp = GETTAG(EOF); BOOST_CHECK(std::string(temp) != ""); BOOST_CHECK_EQUAL( - (uint64_t) * (b->children), ERRBLOCK(get_tag_for_symbol_name(GETTAG(EOF)))); + (uint64_t) * (b->children), + ERRBLOCK(get_tag_for_symbol_name(GETTAG(EOF)))); ::close(fd); @@ -253,7 +256,8 @@ BOOST_AUTO_TEST_CASE(getc) { get_tag_for_symbol_name("inj{SortIOError{}, SortKItem{}}")) .hdr); BOOST_CHECK_EQUAL( - (uint64_t) * (b->children), ERRBLOCK(get_tag_for_symbol_name(GETTAG(EBADF)))); + (uint64_t) * (b->children), + ERRBLOCK(get_tag_for_symbol_name(GETTAG(EBADF)))); } BOOST_AUTO_TEST_CASE(read) { @@ -265,18 +269,20 @@ BOOST_AUTO_TEST_CASE(read) { block *b = hook_IO_read(f, length); BOOST_CHECK_EQUAL( - b->h.hdr, get_block_header_for_symbol( - get_tag_for_symbol_name("inj{SortString{}, SortIOString{}}")) - .hdr); + b->h.hdr, + get_block_header_for_symbol( + get_tag_for_symbol_name("inj{SortString{}, SortIOString{}}")) + .hdr); string *str = (string *)*(b->children); BOOST_CHECK_EQUAL(0, strncmp(str->data, "hello ", 6)); b = hook_IO_read(f, length); BOOST_CHECK_EQUAL( - b->h.hdr, get_block_header_for_symbol( - get_tag_for_symbol_name("inj{SortString{}, SortIOString{}}")) - .hdr); + b->h.hdr, + get_block_header_for_symbol( + get_tag_for_symbol_name("inj{SortString{}, SortIOString{}}")) + .hdr); str = (string *)*(b->children); BOOST_CHECK_EQUAL(0, strncmp(str->data, "world!", 6)); @@ -284,9 +290,10 @@ BOOST_AUTO_TEST_CASE(read) { b = hook_IO_read(f, length); BOOST_CHECK_EQUAL( - b->h.hdr, get_block_header_for_symbol( - get_tag_for_symbol_name("inj{SortString{}, SortIOString{}}")) - .hdr); + b->h.hdr, + get_block_header_for_symbol( + get_tag_for_symbol_name("inj{SortString{}, SortIOString{}}")) + .hdr); str = (string *)*(b->children); BOOST_CHECK_EQUAL(0, len(str)); @@ -298,7 +305,8 @@ BOOST_AUTO_TEST_CASE(read) { get_tag_for_symbol_name("inj{SortIOError{}, SortKItem{}}")) .hdr); BOOST_CHECK_EQUAL( - (uint64_t) * (b->children), ERRBLOCK(get_tag_for_symbol_name(GETTAG(EBADF)))); + (uint64_t) * (b->children), + ERRBLOCK(get_tag_for_symbol_name(GETTAG(EBADF)))); } BOOST_AUTO_TEST_CASE(close) { @@ -319,7 +327,8 @@ BOOST_AUTO_TEST_CASE(close) { block *b = hook_IO_close(f1); BOOST_CHECK_EQUAL( - b->h.hdr, get_block_header_for_symbol(get_tag_for_symbol_name("kseq{}")).hdr); + b->h.hdr, + get_block_header_for_symbol(get_tag_for_symbol_name("kseq{}")).hdr); BOOST_CHECK_EQUAL( ((block *)*(b->children))->h.hdr, get_block_header_for_symbol( @@ -330,7 +339,8 @@ BOOST_AUTO_TEST_CASE(close) { ERRBLOCK(get_tag_for_symbol_name(GETTAG(EBADF)))); b = hook_IO_close(f2); BOOST_CHECK_EQUAL( - b->h.hdr, get_block_header_for_symbol(get_tag_for_symbol_name("kseq{}")).hdr); + b->h.hdr, + get_block_header_for_symbol(get_tag_for_symbol_name("kseq{}")).hdr); BOOST_CHECK_EQUAL( ((block *)*(b->children))->h.hdr, get_block_header_for_symbol( @@ -372,7 +382,8 @@ BOOST_AUTO_TEST_CASE(putc) { block *b = hook_IO_putc(f, c); BOOST_CHECK_EQUAL( - b->h.hdr, get_block_header_for_symbol(get_tag_for_symbol_name("kseq{}")).hdr); + b->h.hdr, + get_block_header_for_symbol(get_tag_for_symbol_name("kseq{}")).hdr); BOOST_CHECK_EQUAL( ((block *)*(b->children))->h.hdr, get_block_header_for_symbol( @@ -402,7 +413,8 @@ BOOST_AUTO_TEST_CASE(seek) { mpz_set_si(f, -1); block *b = hook_IO_seek(f, loc); BOOST_CHECK_EQUAL( - b->h.hdr, get_block_header_for_symbol(get_tag_for_symbol_name("kseq{}")).hdr); + b->h.hdr, + get_block_header_for_symbol(get_tag_for_symbol_name("kseq{}")).hdr); BOOST_CHECK_EQUAL( ((block *)*(b->children))->h.hdr, get_block_header_for_symbol( @@ -434,7 +446,8 @@ BOOST_AUTO_TEST_CASE(seekEnd) { mpz_set_si(f, -1); block *b = hook_IO_seekEnd(f, loc); BOOST_CHECK_EQUAL( - b->h.hdr, get_block_header_for_symbol(get_tag_for_symbol_name("kseq{}")).hdr); + b->h.hdr, + get_block_header_for_symbol(get_tag_for_symbol_name("kseq{}")).hdr); BOOST_CHECK_EQUAL( ((block *)*(b->children))->h.hdr, get_block_header_for_symbol( @@ -463,7 +476,8 @@ BOOST_AUTO_TEST_CASE(write) { mpz_set_si(f, -1); block *b = hook_IO_write(f, msg); BOOST_CHECK_EQUAL( - b->h.hdr, get_block_header_for_symbol(get_tag_for_symbol_name("kseq{}")).hdr); + b->h.hdr, + get_block_header_for_symbol(get_tag_for_symbol_name("kseq{}")).hdr); BOOST_CHECK_EQUAL( ((block *)*(b->children))->h.hdr, get_block_header_for_symbol( @@ -494,7 +508,8 @@ BOOST_AUTO_TEST_CASE(lock) { mpz_set_si(f, -1); b = hook_IO_lock(f, len); BOOST_CHECK_EQUAL( - b->h.hdr, get_block_header_for_symbol(get_tag_for_symbol_name("kseq{}")).hdr); + b->h.hdr, + get_block_header_for_symbol(get_tag_for_symbol_name("kseq{}")).hdr); BOOST_CHECK_EQUAL( ((block *)*(b->children))->h.hdr, get_block_header_for_symbol( @@ -525,7 +540,8 @@ BOOST_AUTO_TEST_CASE(unlock) { mpz_set_si(f, -1); b = hook_IO_unlock(f, len); BOOST_CHECK_EQUAL( - b->h.hdr, get_block_header_for_symbol(get_tag_for_symbol_name("kseq{}")).hdr); + b->h.hdr, + get_block_header_for_symbol(get_tag_for_symbol_name("kseq{}")).hdr); BOOST_CHECK_EQUAL( ((block *)*(b->children))->h.hdr, get_block_header_for_symbol( @@ -569,7 +585,8 @@ BOOST_AUTO_TEST_CASE(system) { BOOST_CHECK_EQUAL( ret->h.hdr, - get_block_header_for_symbol(get_tag_for_symbol_name(GETTAG(systemResult))).hdr); + get_block_header_for_symbol(get_tag_for_symbol_name(GETTAG(systemResult))) + .hdr); BOOST_CHECK_EQUAL(0, mpz_cmp_si((mpz_ptr) * (ret->children), 0)); string *out = (string *)*(ret->children + 1); @@ -587,7 +604,8 @@ BOOST_AUTO_TEST_CASE(system) { BOOST_CHECK((ret->children + 2) != NULL); BOOST_CHECK_EQUAL( ret->h.hdr, - get_block_header_for_symbol(get_tag_for_symbol_name(GETTAG(systemResult))).hdr); + get_block_header_for_symbol(get_tag_for_symbol_name(GETTAG(systemResult))) + .hdr); BOOST_CHECK(mpz_cmp_si((mpz_ptr) * (ret->children), 0) > 0); /* Execute program that segfaults */ @@ -601,7 +619,8 @@ BOOST_AUTO_TEST_CASE(system) { BOOST_CHECK((ret->children + 2) != NULL); BOOST_CHECK_EQUAL( ret->h.hdr, - get_block_header_for_symbol(get_tag_for_symbol_name(GETTAG(systemResult))).hdr); + get_block_header_for_symbol(get_tag_for_symbol_name(GETTAG(systemResult))) + .hdr); // this assertion fails on some platforms // BOOST_CHECK_EQUAL(0, mpz_cmp_si((mpz_ptr) *(ret->children), 139)); @@ -616,7 +635,8 @@ BOOST_AUTO_TEST_CASE(system) { BOOST_CHECK((ret->children + 2) != NULL); BOOST_CHECK_EQUAL( ret->h.hdr, - get_block_header_for_symbol(get_tag_for_symbol_name(GETTAG(systemResult))).hdr); + get_block_header_for_symbol(get_tag_for_symbol_name(GETTAG(systemResult))) + .hdr); BOOST_CHECK_EQUAL(0, mpz_cmp_si((mpz_ptr) * (ret->children), 0)); string *err = (string *)*(ret->children + 2); diff --git a/unittests/runtime-strings/stringtest.cpp b/unittests/runtime-strings/stringtest.cpp index cd9478811..83c226928 100644 --- a/unittests/runtime-strings/stringtest.cpp +++ b/unittests/runtime-strings/stringtest.cpp @@ -12,7 +12,8 @@ #define KCHAR char -void *construct_composite_pattern(uint32_t tag, std::vector &arguments) { +void * +construct_composite_pattern(uint32_t tag, std::vector &arguments) { return nullptr; } @@ -507,9 +508,10 @@ BOOST_AUTO_TEST_CASE(replace) { hook_STRING_replace(replacee, matcher, replacer, b), make_string("goodbye world hello world hello world he worl"))); BOOST_CHECK_EQUAL( - true, hook_STRING_eq( - hook_STRING_replace(replacee, matcher, replacer, c), - make_string("goodbye world goodbye world hello world he worl"))); + true, + hook_STRING_eq( + hook_STRING_replace(replacee, matcher, replacer, c), + make_string("goodbye world goodbye world hello world he worl"))); BOOST_CHECK_EQUAL( true, hook_STRING_eq(