Mass reformat

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(

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_<kore_axiom_declaration, std::shared_ptr<kore_axiom_declaration>>(
       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_<kore_definition, std::shared_ptr<kore_definition>>(ast, "Definition")
+  py::class_<kore_definition, std::shared_ptr<kore_definition>>(
+      ast, "Definition")
       .def(py::init(&kore_definition::create))
       .def("__repr__", print_repr_adapter<kore_definition>())
       .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_<kore_variable_pattern, std::shared_ptr<kore_variable_pattern>>(
       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_<llvm_step_event, std::shared_ptr<llvm_step_event>>(
-                        proof_trace, "llvm_step_event")
-                        .def("__repr__", print_repr_adapter<llvm_step_event>());
+  auto step_event
+      = py::class_<llvm_step_event, std::shared_ptr<llvm_step_event>>(
+            proof_trace, "llvm_step_event")
+            .def("__repr__", print_repr_adapter<llvm_step_event>());
 
   auto rewrite_event
       = py::class_<llvm_rewrite_event, std::shared_ptr<llvm_rewrite_event>>(
@@ -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>>(
+      llvm_side_condition_end_event,
+      std::shared_ptr<llvm_side_condition_end_event>>(
       proof_trace, "llvm_side_condition_end_event", step_event)
       .def_property_readonly(
           "rule_ordinal", &llvm_side_condition_end_event::get_rule_ordinal)

include/kllvm/ast/AST.h

@@ -159,7 +159,8 @@ class kore_composite_sort : public kore_sort {
 
 public:
   static sptr<kore_composite_sort> 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<kore_composite_sort>(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<sptr<kore_sort>> const &get_arguments() const { return arguments_; }
+  std::vector<sptr<kore_sort>> 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<sptr<kore_sort>> const &get_arguments() const {
     return arguments_;
   }
-  [[nodiscard]] std::vector<sptr<kore_sort>> const &get_formal_arguments() const {
+  [[nodiscard]] std::vector<sptr<kore_sort>> const &
+  get_formal_arguments() const {
     return formal_arguments_;
   }
   [[nodiscard]] sptr<kore_sort> get_sort() const { return sort_; }
@@ -399,7 +403,8 @@ class kore_pattern : public std::enable_shared_from_this<kore_pattern> {
 
   virtual void pretty_print(std::ostream &, pretty_print_data const &data) const
       = 0;
-  virtual sptr<kore_pattern> sort_collections(pretty_print_data const &data) = 0;
+  virtual sptr<kore_pattern> sort_collections(pretty_print_data const &data)
+      = 0;
   std::set<std::string> gather_singleton_vars();
   virtual std::map<std::string, int> gather_var_counts() = 0;
   virtual sptr<kore_pattern> filter_substitution(
@@ -438,7 +443,8 @@ class kore_pattern : public std::enable_shared_from_this<kore_pattern> {
   virtual sptr<kore_pattern> expand_macros(
       SubsortMap const &subsorts, SymbolMap const &overloads,
       std::vector<ptr<kore_declaration>> const &axioms, bool reverse,
-      std::set<size_t> &applied_rules, std::set<std::string> const &macro_symbols)
+      std::set<size_t> &applied_rules,
+      std::set<std::string> const &macro_symbols)
       = 0;
 };
 
@@ -530,10 +536,12 @@ class kore_composite_pattern : public kore_pattern {
 public:
   static ptr<kore_composite_pattern> create(std::string const &name) {
     ptr<kore_symbol> sym = kore_symbol::create(name);
-    return ptr<kore_composite_pattern>(new kore_composite_pattern(std::move(sym)));
+    return ptr<kore_composite_pattern>(
+        new kore_composite_pattern(std::move(sym)));
   }
   static ptr<kore_composite_pattern> create(ptr<kore_symbol> sym) {
-    return ptr<kore_composite_pattern>(new kore_composite_pattern(std::move(sym)));
+    return ptr<kore_composite_pattern>(
+        new kore_composite_pattern(std::move(sym)));
   }
   static ptr<kore_composite_pattern> create(kore_symbol *sym) {
     ptr<kore_symbol> 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<std::string, std::vector<kore_symbol *>> &) override;
-  void mark_variables(std::map<std::string, kore_variable_pattern *> &) override;
+  void
+  mark_variables(std::map<std::string, kore_variable_pattern *> &) override;
   sptr<kore_pattern> substitute(substitution const &) override;
   sptr<kore_pattern> expand_aliases(kore_definition *) override;
   sptr<kore_pattern> sort_collections(pretty_print_data const &data) override;
@@ -589,7 +598,8 @@ class kore_composite_pattern : public kore_pattern {
       std::set<size_t> &applied_rules,
       std::set<std::string> const &macro_symbols) override;
 
-  friend void ::kllvm::deallocate_s_ptr_kore_pattern(sptr<kore_pattern> pattern);
+  friend void ::kllvm::deallocate_s_ptr_kore_pattern(
+      sptr<kore_pattern> pattern);
 
   kore_composite_pattern(ptr<kore_symbol> 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<std::string, std::vector<kore_symbol *>> &) override { }
-  void mark_variables(std::map<std::string, kore_variable_pattern *> &) override {
-  }
+  void
+  mark_variables(std::map<std::string, kore_variable_pattern *> &) override { }
   sptr<kore_sort> get_sort() const override { abort(); }
   sptr<kore_pattern> 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;
 

include/kllvm/ast/attribute_set.h

@@ -29,8 +29,8 @@ class kore_composite_pattern;
  */
 class attribute_set {
 public:
-  using storage_t
-      = std::unordered_map<std::string, std::shared_ptr<kore_composite_pattern>>;
+  using storage_t = std::unordered_map<
+      std::string, std::shared_ptr<kore_composite_pattern>>;
 
   enum class key {
     Alias,

include/kllvm/ast/pattern_matching.h

@@ -239,7 +239,8 @@ class pattern {
    */
   [[nodiscard]] match_result
   match(std::shared_ptr<kore_pattern> const &term) const {
-    if (auto composite = std::dynamic_pointer_cast<kore_composite_pattern>(term);
+    if (auto composite
+        = std::dynamic_pointer_cast<kore_composite_pattern>(term);
         composite && composite->get_arguments().size() == arity()
         && composite->get_constructor()->get_name() == constructor_) {
       auto results = std::vector<match_result>{};

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<llvm_step_event> get_step_event() const { return step_event_; }
+  [[nodiscard]] sptr<llvm_step_event> get_step_event() const {
+    return step_event_;
+  }
   [[nodiscard]] sptr<kore_pattern> getkore_pattern() const {
     return kore_pattern_;
   }
@@ -235,7 +237,9 @@ class llvm_rewrite_trace {
   [[nodiscard]] std::vector<llvm_event> 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<llvm_event> 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;

include/kllvm/codegen/CreateTerm.h

@@ -21,7 +21,8 @@ class create_term {
   std::set<kore_pattern *> 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<llvm::Value *> &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<llvm::Module>
 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. */

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();

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`.

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);