proofs: initial commit with infrastructure

The patch adds an infrastructure for CBMC proofs and a single
proof for the Lua C function `luaL_makeseed()`. Checking has
failed due to arithmetic overflow on unsigned in `luai_makeseed()`.

Currently, the PUC Rio Lua is supported, LuaJIT is not.

Tested with CBMC 6.7.1

Author: ligurio

CMakeLists.txt

@@ -21,6 +21,7 @@ option(ENABLE_BUILD_PROTOBUF "Enable building Protobuf library" ON)
 option(ENABLE_BONUS_TESTS "Enable bonus tests" OFF)
 option(ENABLE_INTERNAL_TESTS "Enable internal tests" OFF)
 option(ENABLE_LAPI_TESTS "Enable Lua API tests" OFF)
+option(ENABLE_PROOFS "Enable CBMC proofs" OFF)
 
 set(CMAKE_MODULE_PATH "${CMAKE_CURRENT_SOURCE_DIR}/cmake" ${CMAKE_MODULE_PATH})
 set(CMAKE_INCLUDE_PATH "${CMAKE_CURRENT_SOURCE_DIR}/cmake" ${CMAKE_INCLUDE_PATH})
@@ -43,6 +44,13 @@ if (USE_LUAJIT AND NOT LUA_VERSION)
   set(LUA_VERSION "v2.1")
 endif()
 
+if(ENABLE_PROOFS)
+  # The latest PUC Rio Lua version checked by CBMC.
+  if (USE_LUA)
+    set(LUA_VERSION "a5522f06d2679b8f18534fd6a9968f7eb539dc31")
+  endif()
+endif()
+
 if (USE_LUA)
   include(BuildLua)
   build_lua(${LUA_VERSION})
@@ -73,6 +81,13 @@ if (ENABLE_LUAJIT_RANDOM_RA AND NOT IS_LUAJIT)
   message(FATAL_ERROR "Option ENABLE_LUAJIT_RANDOM_RA is LuaJIT-specific.")
 endif()
 
+enable_testing()
+
+if(ENABLE_PROOFS)
+  add_subdirectory(proofs)
+  return()
+endif()
+
 if(NOT CMAKE_CXX_COMPILER_ID STREQUAL "Clang" OR
    NOT CMAKE_C_COMPILER_ID STREQUAL "Clang")
   message(FATAL_ERROR
@@ -95,8 +110,6 @@ if(ENABLE_COV)
     include(CodeCoverage)
 endif()
 
-enable_testing()
-
 add_subdirectory(extra)
 add_subdirectory(libluamut)
 add_subdirectory(tests)

README.md

@@ -19,8 +19,8 @@
 
 # lunapark
 
-is a set of fuzzing tests for C implementations of Lua runtime (PUC Rio Lua and
-LuaJIT).
+is a set of fuzzing tests and CBMC proofs for C implementations
+of Lua runtimes (PUC Rio Lua and LuaJIT).
 
 <details>
 <summary>If you are interested to know why it is called Lunapark</summary>
@@ -63,6 +63,7 @@ is LuaJIT-specific.
   library is used.
 - `ENABLE_INTERNAL_TESTS` enables internal tests.
 - `ENABLE_LAPI_TESTS` enables Lua API tests.
+- `ENABLE_PROOFS` enables building CBMC proofs instead tests.
 
 ### Running
 

cmake/BuildLua.cmake

@@ -11,8 +11,10 @@ macro(build_lua LUA_VERSION)
     if (ENABLE_LUA_APICHECK)
         set(CFLAGS "${CFLAGS} -DLUA_USE_APICHECK")
     endif (ENABLE_LUA_APICHECK)
-    set(CFLAGS "${CFLAGS} -fsanitize=fuzzer-no-link")
-    set(LDFLAGS "-fsanitize=fuzzer-no-link")
+    if(NOT ENABLE_PROOFS)
+        set(CFLAGS "${CFLAGS} -fsanitize=fuzzer-no-link")
+        set(LDFLAGS "-fsanitize=fuzzer-no-link")
+    endif()
     if (OSS_FUZZ)
         set(LDFLAGS "${CFLAGS} ${LDFLAGS}")
     endif (OSS_FUZZ)

proofs/CMakeLists.txt

@@ -0,0 +1,98 @@
+find_program(CBMC_BIN cbmc)
+
+list(APPEND GENERAL_CBMC_OPTS
+  --bounds-check
+  --conversion-check
+  --div-by-zero-check
+  --drop-unused-functions
+  --float-overflow-check
+  --flush
+  --fpa
+  --malloc-fail-null
+  --malloc-may-fail
+  --memory-cleanup-check
+  --memory-leak-check
+  --nan-check
+  --object-bits 16
+  --pointer-check
+  --pointer-overflow-check
+  --pointer-primitive-check
+  --refine
+  --signed-overflow-check
+  --stack-trace
+  --trace
+  --undefined-shift-check
+  --unsigned-overflow-check
+  --verbosity 10
+  --z3
+)
+
+set(DEFAULT_TIMEOUT 30)
+
+list(APPEND DEFAULT_LUA_CBMC_OPTS
+  ${GENERAL_CBMC_OPTS}
+)
+
+list(APPEND DEFAULT_LUAJIT_CBMC_OPTS
+  ${GENERAL_CBMC_OPTS}
+)
+
+if(USE_LUA)
+  set(DEFAULT_CBMC_OPTS ${DEFAULT_LUA_CBMC_OPTS})
+elseif (USE_LUAJIT)
+  set(DEFAULT_CBMC_OPTS ${DEFAULT_LUAJIT_CBMC_OPTS})
+endif()
+
+set(PROOF_TARGETS "")
+
+function(create_proof)
+  cmake_parse_arguments(
+    CBMC
+    ""
+    "FILENAME"
+    ""
+    ${ARGN}
+  )
+
+  get_filename_component(test_name ${CBMC_FILENAME} NAME_WE)
+  message(STATUS "Building a proof ${test_name}")
+
+  # Build a CBMC proof binary.
+  add_executable(${test_name} ${CBMC_FILENAME})
+  target_link_libraries(${test_name} PUBLIC ${LUA_LIBRARIES})
+  target_include_directories(${test_name} PRIVATE
+    ${LUA_INCLUDE_DIR} ${CMAKE_CURRENT_SOURCE_DIR})
+  target_compile_options(${test_name} PRIVATE
+    -Wall -Wextra -Wpedantic -Wno-unused-parameter -g)
+  add_dependencies(${test_name} ${LUA_LIBRARIES})
+
+  # Create a CTest-based test.
+  set(proof_name "${test_name}_proof")
+  string(JOIN " " CBMC_COMMAND
+    ${CBMC_BIN}
+    $<TARGET_FILE:${test_name}>
+    ${DEFAULT_CBMC_OPTS}
+    # Notice that `--cover location` cannot be used together
+    # with `--unwinding-assertions`.)
+    --unwinding-assertions
+  )
+  add_test(NAME ${proof_name}
+    COMMAND ${SHELL} -c "${CBMC_COMMAND}"
+  )
+  set_tests_properties(${proof_name} PROPERTIES
+    LABELS proof
+    TIMEOUT ${DEFAULT_TIMEOUT}
+  )
+  set(PROOF_TARGETS ${PROOF_TARGETS} ${test_name} PARENT_SCOPE)
+endfunction()
+
+##################################################################
+# Lua C API functions
+##################################################################
+
+create_proof(FILENAME luaL_makeseed.c)
+
+add_custom_target(build_cbmc_proofs
+  DEPENDS ${PROOF_TARGETS}
+  COMMENT "Building CBMC proofs"
+)

proofs/README.md

@@ -0,0 +1,10 @@
+## CBMC proofs
+
+### Usage
+
+```
+nix-shell -p cbmc
+cmake -S . -B build -DUSE_LUA=ON -DCMAKE_BUILD_TYPE=Debug -DCMAKE_C_COMPILER=goto-cc -DENABLE_PROOFS=ON -DENABLE_LUA_APICHECK=ON -DENABLE_LUA_ASSERT=ON
+cmake --build build --target build_proofs --parallel
+ctest --test-dir build --output-on-failure --timeout 15 --tests-regex luaL_makeseed --verbose
+```

proofs/luaL_makeseed.c

@@ -0,0 +1,24 @@
+/*
+ * SPDX-License-Identifier: ISC
+ *
+ * Copyright 2023-2026, Sergey Bronnikov.
+ */
+
+#include "lua.h"
+#include "lauxlib.h"
+
+/* unsigned int luaL_makeseed (lua_State *L); */
+/* [-0, +0, -] */
+static void
+__luaL_makeseed(lua_State *L)
+{
+	luaL_makeseed(L);
+}
+
+int
+main()
+{
+	__luaL_makeseed(NULL);
+
+	return 0;
+}