#pragma once

#include "common.hpp"
#include "lattice_climb.hpp"

DIVINE_RELAX_WARNINGS
#include <llvm/IR/Value.h>
#include <llvm/IR/Function.h>
#include <llvm/IR/Type.h>
#include <llvm/IR/DerivedTypes.h>
#include <llvm/IR/Module.h>
DIVINE_UNRELAX_WARNINGS

namespace shoop
{

template < typename T >
llvm::Type *get_int_type( llvm::LLVMContext &ctx )
{
    return llvm::IntegerType::get( ctx, sizeof( T ) * CHAR_BIT );
}

// Ensure that a given value is a function or die. This exists because
// llvm::Module::getOrInsertFunction returns either the correct function or,
// in case of signature conflict, the existing function wrapped in a bitcast.
llvm::Function *as_function( llvm::Value *val );
llvm::Function *as_function( llvm::FunctionCallee fc );

// We need the following functions in the module given to DIVINE:
// int  main( ... )
// void __tester() (called by DiOS `static` config as an entrypoint)
// yyy  __lamp_xxx_yyy (abstract value constructors)
// void __lamp_set_precondition( i8 *, int )
// void __assert_precondition( bool );

// We need to appease the runtime by providing the main function if it is not provided
// by user before running Divine on 'mod'. A dummy with 'return 0;' suffices. It won't
// be used by our Divine run either way, as our DiOS configuration ensures that the OS
// invokes the correct function (see `generate_test_wrapper` in `function_verifier.cpp`).
void ensure_main_exists( llvm::Module &mod );

// This returns a function with return type 'return_type' that creates abstract values in domain
// 'domain' within module 'module'. If this function does not exist yet, it is created in the module.
// Example: for dom ~ sunit, return_type ~ i64 returns 'uint64_t __lamp_sunit_i64()'.
llvm::Function *get_abstract_constructor( parameter_domain domain, llvm::Module *module, llvm::Type *return_type );

// void __lamp_set_precondition( const uint8_t *cond, int size )
llvm::Function *get_set_precondition( llvm::Module &mod );

// void __assert_precondition( bool v )
llvm::Function *get_assert_precondition( llvm::Module &mod );

}