// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
//! this module lazily declares builtin functions in CBMC
use self::BuiltinFn::*;
use super::{Expr, Location, Symbol, Type};

#[derive(Debug, Clone, Copy)]
pub enum BuiltinFn {
    Abort,
    Assert,
    CProverAssume,
    CProverCover,
    Calloc,
    Ceil,
    Ceilf,
    Copysign,
    Copysignf,
    Cos,
    Cosf,
    Error,
    ErrorNoLocation,
    Exp,
    Exp2,
    Exp2f,
    Expf,
    Fabs,
    Fabsf,
    Floor,
    Floorf,
    Fma,
    Fmaf,
    Fmax,
    Fmaxf,
    Fmin,
    Fminf,
    Free,
    Log,
    Log10,
    Log10f,
    Log2,
    Log2f,
    Logf,
    Malloc,
    Memcmp,
    Memcpy,
    Memmove,
    Memset,
    Nearbyint,
    Nearbyintf,
    Posixmemalign,
    Pow,
    Powf,
    Powi,
    Powif,
    Realloc,
    Rint,
    Rintf,
    Round,
    Roundf,
    Sin,
    Sinf,
    Sqrt,
    Sqrtf,
    Sysconf,
    Trunc,
    Truncf,
    Unlink,
}

impl ToString for BuiltinFn {
    fn to_string(&self) -> String {
        match self {
            Abort => "abort",
            Assert => "assert",
            CProverAssume => "__CPROVER_assume",
            CProverCover => "__CPROVER_cover",
            Calloc => "calloc",
            Ceil => "ceil",
            Ceilf => "ceilf",
            Copysign => "copysign",
            Copysignf => "copysignf",
            Cos => "cos",
            Cosf => "cosf",
            Error => "__error",
            ErrorNoLocation => "__errno_location",
            Exp => "exp",
            Exp2 => "exp2",
            Exp2f => "exp2f",
            Expf => "expf",
            Fabs => "fabs",
            Fabsf => "fabsf",
            Floor => "floor",
            Floorf => "floorf",
            Fma => "fma",
            Fmaf => "fmaf",
            Fmax => "fmax",
            Fmaxf => "fmaxf",
            Fmin => "fmin",
            Fminf => "fminf",
            Free => "free",
            Log => "log",
            Log10 => "log10",
            Log10f => "log10f",
            Log2 => "log2",
            Log2f => "log2f",
            Logf => "logf",
            Malloc => "malloc",
            Memcmp => "memcmp",
            Memcpy => "memcpy",
            Memmove => "memmove",
            Memset => "memset",
            Nearbyint => "nearbyint",
            Nearbyintf => "nearbyintf",
            Posixmemalign => "posix_memalign",
            Pow => "pow",
            Powf => "powf",
            Powi => "__builtin_powi",
            Powif => "__builtin_powif",
            Realloc => "realloc",
            Rint => "rint",
            Rintf => "rintf",
            Round => "round",
            Roundf => "roundf",
            Sin => "sin",
            Sinf => "sinf",
            Sqrt => "sqrt",
            Sqrtf => "sqrtf",
            Sysconf => "sysconf",
            Trunc => "trunc",
            Truncf => "truncf",
            Unlink => "unlink",
        }
        .to_string()
    }
}

/// Utility functions for declaring builtins when creating a symbol table
impl BuiltinFn {
    pub fn param_types(&self) -> Vec<Type> {
        match self {
            Abort => vec![],
            Assert => vec![Type::bool()],
            CProverAssume => vec![Type::bool()],
            CProverCover => vec![Type::bool()],
            Calloc => vec![Type::size_t(), Type::size_t()],
            Ceil => vec![Type::double()],
            Ceilf => vec![Type::float()],
            Copysign | Fmax | Fmin | Pow => vec![Type::double(), Type::double()],
            Copysignf => vec![Type::float(), Type::float()],
            Cos => vec![Type::double()],
            Cosf => vec![Type::float()],
            Error => vec![],
            ErrorNoLocation => vec![],
            Exp => vec![Type::double()],
            Exp2 => vec![Type::double()],
            Exp2f => vec![Type::float()],
            Expf => vec![Type::float()],
            Fabs => vec![Type::double()],
            Fabsf => vec![Type::float()],
            Floor => vec![Type::double()],
            Floorf => vec![Type::float()],
            Fma => vec![Type::double(), Type::double(), Type::double()],
            Fmaf => vec![Type::float(), Type::float(), Type::float()],
            Fmaxf => vec![Type::float(), Type::float()],
            Fminf => vec![Type::float(), Type::float()],
            Free => vec![Type::void_pointer()],
            Log => vec![Type::double()],
            Log10 => vec![Type::double()],
            Log10f => vec![Type::float()],
            Log2 => vec![Type::double()],
            Log2f => vec![Type::float()],
            Logf => vec![Type::float()],
            Malloc => vec![Type::size_t()],
            Memcmp => vec![Type::void_pointer(), Type::void_pointer(), Type::size_t()],
            Memcpy => vec![Type::void_pointer(), Type::void_pointer(), Type::size_t()],
            Memmove => vec![Type::void_pointer(), Type::void_pointer(), Type::size_t()],
            Memset => vec![Type::void_pointer(), Type::c_int(), Type::size_t()],
            Nearbyint => vec![Type::double()],
            Nearbyintf => vec![Type::float()],
            Posixmemalign => vec![Type::void_pointer(), Type::size_t(), Type::size_t()],
            Powf => vec![Type::float(), Type::float()],
            Powi => vec![Type::double(), Type::c_int()],
            Powif => vec![Type::float(), Type::c_int()],
            Realloc => vec![Type::void_pointer(), Type::size_t()],
            Rint => vec![Type::double()],
            Rintf => vec![Type::float()],
            Round => vec![Type::double()],
            Roundf => vec![Type::float()],
            Sin => vec![Type::double()],
            Sinf => vec![Type::float()],
            Sqrt => vec![Type::double()],
            Sqrtf => vec![Type::float()],
            Sysconf => vec![Type::c_int()],
            Trunc => vec![Type::double()],
            Truncf => vec![Type::float()],
            Unlink => vec![Type::c_char().to_pointer()],
        }
    }

    pub fn return_type(&self) -> Type {
        match self {
            Abort => Type::empty(),
            Assert => Type::empty(),
            CProverAssume => Type::empty(),
            CProverCover => Type::empty(),
            Calloc => Type::void_pointer(),
            Ceil => Type::double(),
            Ceilf => Type::float(),
            Copysign => Type::double(),
            Copysignf => Type::float(),
            Cos => Type::double(),
            Cosf => Type::float(),
            Error => Type::c_int().to_pointer(),
            ErrorNoLocation => Type::c_int().to_pointer(),
            Exp => Type::double(),
            Exp2 => Type::double(),
            Exp2f => Type::float(),
            Expf => Type::float(),
            Fabs => Type::double(),
            Fabsf => Type::float(),
            Floor => Type::double(),
            Floorf => Type::float(),
            Fma => Type::double(),
            Fmaf => Type::float(),
            Fmax => Type::double(),
            Fmaxf => Type::float(),
            Fmin => Type::double(),
            Fminf => Type::float(),
            Free => Type::empty(),
            Log => Type::double(),
            Log10 => Type::double(),
            Log10f => Type::float(),
            Log2 => Type::double(),
            Log2f => Type::float(),
            Logf => Type::float(),
            Malloc => Type::void_pointer(),
            Memcmp => Type::c_int(),
            Memcpy => Type::void_pointer(),
            Memmove => Type::void_pointer(),
            Memset => Type::void_pointer(),
            Nearbyint => Type::double(),
            Nearbyintf => Type::float(),
            Posixmemalign => Type::c_int(),
            Pow => Type::double(),
            Powf => Type::float(),
            Powi => Type::double(),
            Powif => Type::float(),
            Realloc => Type::void_pointer(),
            Rint => Type::double(),
            Rintf => Type::float(),
            Round => Type::double(),
            Roundf => Type::float(),
            Sin => Type::double(),
            Sinf => Type::float(),
            Sqrt => Type::double(),
            Sqrtf => Type::float(),
            Sysconf => Type::c_long_int(),
            Trunc => Type::double(),
            Truncf => Type::float(),
            Unlink => Type::c_int(),
        }
    }

    pub fn list_all() -> Vec<BuiltinFn> {
        vec![
            Abort,
            Assert,
            CProverAssume,
            CProverCover,
            Calloc,
            Ceil,
            Ceilf,
            Copysign,
            Copysignf,
            Cos,
            Cosf,
            Error,
            ErrorNoLocation,
            Exp,
            Exp2,
            Exp2f,
            Expf,
            Fabs,
            Fabsf,
            Floor,
            Floorf,
            Fma,
            Fmaf,
            Fmax,
            Fmaxf,
            Fmin,
            Fminf,
            Free,
            Log,
            Log10,
            Log10f,
            Log2,
            Log2f,
            Logf,
            Malloc,
            Memcmp,
            Memcpy,
            Memmove,
            Memset,
            Nearbyint,
            Nearbyintf,
            Posixmemalign,
            Pow,
            Powf,
            Powi,
            Powif,
            Realloc,
            Rint,
            Rintf,
            Round,
            Roundf,
            Sin,
            Sinf,
            Sqrt,
            Sqrtf,
            Sysconf,
            Trunc,
            Truncf,
            Unlink,
        ]
    }
}

/// Converters: build symbols and expressions from Builtins
impl BuiltinFn {
    pub fn as_symbol(&self) -> Symbol {
        Symbol::builtin_function(&self.to_string(), self.param_types(), self.return_type())
    }

    pub fn as_expr(&self) -> Expr {
        self.as_symbol().to_expr()
    }

    pub fn call(&self, arguments: Vec<Expr>, loc: Location) -> Expr {
        self.as_expr().with_location(loc).call(arguments).with_location(loc)
    }
}