c_builtins.h

Go to the documentation of this file.

#pragma once
 
#include <string_view>
#include <util/base/prefix.h>

constexpr int esbmc_object_size_whole = 4;

enum class bit_scan_endt
{
  none,
  leading,
  trailing,
  first_set,
  redundant_sign
};

inline bit_scan_endt bit_scan_builtin(std::string_view symname)
{
  constexpr std::string_view prefix = "c:@F@__builtin_";
  if (!has_prefix(symname, prefix))
    return bit_scan_endt::none;
  symname.remove_prefix(prefix.size());
 
  bit_scan_endt end = bit_scan_endt::none;
  std::size_t stem = 3;
  if (has_prefix(symname, "clz"))
    end = bit_scan_endt::leading;
  else if (has_prefix(symname, "ctz"))
    end = bit_scan_endt::trailing;
  else if (has_prefix(symname, "ffs"))
    end = bit_scan_endt::first_set;
  else if (has_prefix(symname, "clrsb"))
  {
    end = bit_scan_endt::redundant_sign;
    stem = 5;
  }
  else
    return bit_scan_endt::none;
  symname.remove_prefix(stem);
 
  for (const std::string_view width : {"", "l", "ll"})
    if (symname == width)
      return end;
 
  // Only clz/ctz have the 16-bit and type-generic spellings.
  if (end != bit_scan_endt::leading && end != bit_scan_endt::trailing)
    return bit_scan_endt::none;
 
  for (const std::string_view width : {"s", "g"})
    if (symname == width)
      return end;
  return bit_scan_endt::none;
}