Merge remote-tracking branch 'origin/develop'

Author: rv-auditor

include/kllvm/codegen/CreateTerm.h

@@ -124,6 +124,8 @@ std::string make_side_condition_function(
     kore_axiom_declaration *axiom, kore_definition *definition,
     llvm::Module *module);
 
+bool can_tail_call(llvm::Type *type);
+
 extern std::string map_struct;
 extern std::string list_struct;
 extern std::string set_struct;

lib/codegen/CreateTerm.cpp

@@ -1038,6 +1038,19 @@ void add_abort(llvm::BasicBlock *block, llvm::Module *module) {
   new llvm::UnreachableInst(module->getContext(), block);
 }
 
+bool can_tail_call(llvm::Type *type) {
+  if (type->isVoidTy()) {
+    return false;
+  }
+  if (!type->isIntegerTy()) {
+    return true;
+  }
+  auto *int_type = dyn_cast<llvm::IntegerType>(type);
+  // integer types that cannot fit in 3 64-bit registers cannot be tail
+  // called on X86
+  return int_type->getBitWidth() <= 192;
+}
+
 bool make_function(
     std::string const &name, kore_pattern *pattern, kore_definition *definition,
     llvm::Module *module, bool tailcc, bool big_step, bool apply,
@@ -1142,8 +1155,9 @@ bool make_function(
       // 2. Return returns return value of call (guaranteed)
       // 3. Calling convention is tailcc
       // 4. Function is not sret (here approximated by checking if return type is void)
+      // 5. Function is not "sret demoted" (here approximated by checking that it is not an MInt of size >192)
       if (call->getCallingConv() == llvm::CallingConv::Tail
-          && call->getType() != llvm::Type::getVoidTy(module->getContext())) {
+          && can_tail_call(call->getType())) {
         call->setTailCallKind(llvm::CallInst::TCK_MustTail);
       }
     }

lib/codegen/Decision.cpp

@@ -621,7 +621,9 @@ void leaf_node::codegen(decision *d) {
   call->setCallingConv(llvm::CallingConv::Tail);
 
   if (child_ == nullptr) {
-    call->setTailCallKind(llvm::CallInst::TCK_MustTail);
+    if (can_tail_call(call->getType())) {
+      call->setTailCallKind(llvm::CallInst::TCK_MustTail);
+    }
     llvm::ReturnInst::Create(d->ctx_, call, d->current_block_);
   } else {
     new llvm::StoreInst(

test/defn/k-files/sret-demotion.k

@@ -0,0 +1,6 @@
+module TEST
+  imports MINT
+
+  syntax MInt{256}
+
+endmodule