Lua Implementation Verification

wiki

Debugging macros in the source

See LUA_USE_APICHECK and lua_assert macros in the source code.

Testing suites

See UnitTesting, which links to test suites for Lua 5.0 - 5.2beta.

Valgrid

Various people have used tools like Valgrid for dynamic analysis ([search lua-l]).

Gimpel PC lint

Here's an initial set of definitions to lint Lua with [Gimpel PC-lint]. Many improvements could be made. Unfortunately, Lua's source code with all its casting and things make linting a challenge, and doing this effectively likely requires many changes to the source code.

// lua.lnt
// gimpel lint 9.00h on Lua 5.2.0rc1.
// David Manura, 2011-11.

// safe to ignore
-e537 // repeated include file (superfluous warnings)
-e801 // use of goto is deprecated
-e834 // operator '-' followed by operator '+' is confusing.  Use parentheses.
-esym(438,argp) // last value assigned to variable not used (debug.c vararg)
-esym(123,gch,luai_num*,luaL_checkint) // macro defined with arguments
-esym(750,LUA_LIB) // local macro not referenced
-esym(750,l*_c) // local macro not referenced
-e845 // the right argument to operator is certain to  be 0
-e778 // constant expression evaluates to 0 in operation
-e835 // a zero has been given as right argument to operator
-e730 // boolean argument to function

// functions that don't return
-sem(cannot, r_no)
-sem(luaL_error, r_no)
-sem(luaL_argerror, r_no)
-sem(luaX_syntaxerror, r_no)
-sem(tag_error, r_no)
-sem(error_expected, r_no)
-sem(errorlimit, r_no)
-sem(escerror, r_no)
-sem(fileerror, r_no)
-sem(lexerror, r_no)
-sem(semerror, r_no)
-sem(typeerror, r_no)
// all below are marked 'l_noret' in the code
-sem(luaD_throw, r_no)
-sem(luaB_error, r_no)
-sem(luaG_typeerror, r_no)
-sem(luaG_concaterror, r_no)
-sem(luaG_aritherror, r_no)
-sem(luaG_ordererror, r_no)
-sem(luaG_errormsg, r_no)
-sem(luaG_runerror, r_no)
-sem(resume_error, r_no)


-esym(767,setnvalue,TValuefields,NILCONSTANT,numfield,
          val_,num_,rttype,ttisnumber,ttisequal,checktag,settt_,setobj)
          // macro defined differently in another module
          // http://lua-users.org/lists/lua-l/2011-10/msg00007.html
-e546 // suspicious use of &

// check these later (these are numerous)
-e534 // ignoring return value of function
-e648 // overflow in computing constant for operation
-e508 // extern used with definition
-e641 // converting enum to int
-e679 // suspicious truncation in arithmetic expression
-e818 // Pointer parameter could be declared as pointing to const
-e826 // suspicious pointer-to-pointer conversion
-e661 // possible access of out-of-bounds pointer
-e662 // possible creation of out-of-bounds pointer
-e613 // possible use of null pointer
-e416 // likely creation of out-of-bounds pointer
-e420 // apparent access beyond array for function
-e670 // possible access beyond array for function
-e669 // possible data overrun for function
-e419 // apparent data overrun for function
-e415 // likely access of out-of-bounds pointer
-e732 // loss of sign
-e737 // loss of sign in promotion
-e506 // constant value Boolean
// note: other warnings (less numerous) also remain

// Avoids assembly code not understood by lint (MS_ASMTRICK)
-u_M_IX86  // WARNING: undefining this causes problems in setjmp.h

-esym(750, _FILE_OFFSET_BITS) // local macro not referenced
   // This macro not used on non-POSIX systems

// TO FIX
-esym(760,LUA_FILEHANDLE)
/*
#define LUA_FILEHANDLE		"FILE*"
src\lualib.h(15) : Info 760: Redundant macro 'LUA_FILEHANDLE' defined
    identically at line 183, file src\lauxlib.h, module src\lauxlib.c
src\lauxlib.h(183) : Info 830: Location cited in prior message
*/


//-passes(3)

-header(lint.h)

src/lapi.c
src/lauxlib.c
src/lbaselib.c
src/lbitlib.c
src/lcode.c
src/lcorolib.c
src/lctype.c
src/ldblib.c
src/ldebug.c
src/ldo.c
src/ldump.c
src/lfunc.c
src/lgc.c
src/linit.c
src/liolib.c
src/llex.c
src/lmathlib.c
src/lmem.c
src/loadlib.c
src/lobject.c
src/lopcodes.c
src/loslib.c
src/lparser.c
src/lstate.c
src/lstring.c
src/lstrlib.c
src/ltable.c
src/ltablib.c
src/ltm.c
src/lua.c
src/luac.c
src/lundump.c
src/lvm.c
src/lzio.c

.

//lint.h

//lint -sem(myexit, r_no)
extern int myexit(void);
#define LUA_LINT_FALLTHROUGH /*lint -fallthrough*/
  // NOTE: edit the Lua source code to add this macro at the end of
  // switch cases labeled "/* go through */"
#define lua_assert(p) ((p) ? 0 : myexit())

#define LUA_LINT_UNREACHABLE /*lint --e{527} */
  // NOTE: edit the Lua source code to add this macro at end of
  // all lines that are unreachable

#define LUA_LINT_LOOPVARCHANGED(x) /*lint --e{850} */
  // NOTE: edit the Lua source to add add this macro inside any
  // loop that modifies variable x.

.

usage: lint lua.lnt

Lua Manual (HTML) validation

The Lua manual in HTML format can be checked in tools like the [w3c validator]. grep techniques can also be helpful.

Formal verification techniques

Has anyone tried this? [1]