Merge remote-tracking branch 'origin/develop'

Author: rv-auditor

docs/proof-trace.md

@@ -39,13 +39,7 @@ event             ::= hook
                     | config
                     | pattern_matching_failure
 
-argument          ::= hook
-                    | function
-                    | rule
-                    | side_cond_entry
-                    | side_cond_exit
-                    | kore_term
-                    | pattern_matching_failure
+arg               ::= kore_term
 
 name              ::= string
 location          ::= string
@@ -81,7 +75,7 @@ uint64            ::= <64-bit unsigned little endian integer>
 - The `relative_position` is a null terminated string of positive integers
   separated by `:` (ie. `0:1:1`)
 - The `arg*` in the `function` and `hook` event is a list of arguments that
-  are either `hook`, `function`, `rule`, `side_cond_entry`, `side_cond_exit`, or `kore_term`.
+  are `kore_term`s passed to the function or hook.
 
 
 ## Tools

include/kllvm/binary/ProofTraceParser.h

@@ -319,7 +319,7 @@ class llvm_rewrite_trace {
 
 class proof_trace_parser {
 public:
-  static constexpr uint32_t expected_version = 12U;
+  static constexpr uint32_t expected_version = 13U;
 
 private:
   bool verbose_;
@@ -585,80 +585,18 @@ class proof_trace_parser {
   }
 
   bool parse_argument(proof_trace_buffer &buffer, llvm_event &event) {
-    if (!buffer.eof() && buffer.peek() == '\x7F') {
-      uint64_t pattern_len = 0;
-      auto kore_term = parse_kore_term(buffer, pattern_len);
-      if (!kore_term) {
-        return false;
-      }
-      event.setkore_pattern(kore_term, pattern_len);
-
-      return true;
-    }
-
-    if (!buffer.has_word()) {
+    if (buffer.eof() || buffer.peek() != '\x7F') {
       return false;
     }
 
-    switch (buffer.peek_word()) {
-
-    case hook_event_sentinel: {
-      auto hook_event = parse_hook(buffer);
-      if (!hook_event) {
-        return false;
-      }
-      event.set_step_event(hook_event);
-      return true;
-    }
-
-    case function_event_sentinel: {
-      auto function_event = parse_function(buffer);
-      if (!function_event) {
-        return false;
-      }
-      event.set_step_event(function_event);
-      return true;
-    }
-
-    case rule_event_sentinel: {
-      auto rule_event = parse_rule(buffer);
-      if (!rule_event) {
-        return false;
-      }
-      event.set_step_event(rule_event);
-      return true;
-    }
-
-    case side_condition_event_sentinel: {
-      auto side_condition_event = parse_side_condition(buffer);
-      if (!side_condition_event) {
-        return false;
-      }
-      event.set_step_event(side_condition_event);
-      return true;
-    }
-
-    case side_condition_end_sentinel: {
-      auto side_condition_end_event = parse_side_condition_end(buffer);
-      if (!side_condition_end_event) {
-        return false;
-      }
-      event.set_step_event(side_condition_end_event);
-      return true;
-    }
-
-    case pattern_matching_failure_sentinel: {
-      auto pattern_matching_failure_event
-          = parse_pattern_matching_failure(buffer);
-      if (!pattern_matching_failure_event) {
-        return false;
-      }
-      event.set_step_event(pattern_matching_failure_event);
-      return true;
+    uint64_t pattern_len = 0;
+    auto kore_term = parse_kore_term(buffer, pattern_len);
+    if (!kore_term) {
+      return false;
     }
+    event.setkore_pattern(kore_term, pattern_len);
 
-    default: return false;
-    }
+    return true;
   }
 
   sptr<llvm_step_event> parse_step_event(proof_trace_buffer &buffer) {

include/kllvm/codegen/CreateTerm.h

@@ -26,14 +26,18 @@ class create_term {
   std::set<kore_pattern *> static_terms_;
 
   llvm::Value *alloc_arg(
-      kore_composite_pattern *pattern, int idx, bool is_hook_arg,
+      kore_composite_pattern *pattern, int idx,
       std::string const &location_stack);
+  llvm::Value *create_hardcoded_hook(
+      std::string const &name, kore_composite_pattern *pattern,
+      std::vector<llvm::Value *> &args, std::string const &location_stack);
   llvm::Value *create_hook(
       kore_composite_pattern *hook_att, kore_composite_pattern *pattern,
       std::string const &location_stack = "");
   llvm::Value *create_function_call(
       std::string const &name, kore_composite_pattern *pattern, bool sret,
-      bool tailcc, bool is_hook, std::string const &location_stack = "");
+      bool tailcc, bool is_hook, std::vector<llvm::Value *> &args,
+      std::string const &location_stack = "");
   llvm::Value *not_injection_case(
       kore_composite_pattern *constructor, llvm::Value *val,
       std::string const &location_stack = "");

include/kllvm/codegen/ProofEvent.h

@@ -155,6 +155,15 @@ class proof_event {
       llvm::Value *val, kore_composite_sort *sort, bool is_hook_arg,
       llvm::BasicBlock *current_block);
 
+  [[nodiscard]] llvm::BasicBlock *short_circuit_hook_argument(
+      llvm::Value *val, llvm::Value *short_circuit_cond, bool invert_cond,
+      kore_composite_sort *sort, llvm::BasicBlock *current_block);
+
+  [[nodiscard]] llvm::BasicBlock *short_circuit_hook_argument(
+      llvm::Value *val_first, llvm::Value *val_second, llvm::Value *select_cond,
+      kore_composite_sort *sort_first, kore_composite_sort *sort_second,
+      llvm::BasicBlock *current_block);
+
   [[nodiscard]] llvm::BasicBlock *rewrite_event_pre(
       kore_axiom_declaration const &axiom, uint64_t arity,
       std::map<std::string, kore_variable_pattern *> vars,