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]