[Date Prev][Date Next][Thread Prev][Thread Next]
[Date Index]
[Thread Index]
- Subject: Re: verification and linting of lua implementations
- From: David Manura <dm.lua@...>
- Date: Thu, 24 Nov 2011 21:53:05 -0500
On Tue, Oct 25, 2011 at 12:59 AM, David Manura <dm.lua@math2.org> wrote:
> However, to really maximize [Gimpel lint's] potential can be a lot of
> work and involves code changes (e.g. lint comments and const usage),
> perhaps extensive, that I'm not sure will be accepted by the Lua
> upstream. The same might apply to Coverty.
On Wed, Oct 26, 2011 at 3:20 PM, Roberto Ierusalimschy
<roberto@inf.puc-rio.br> wrote:
>> On Tue, Oct 25, 2011 at 7:01 PM, Florian Weimer <fw@deneb.enyo.de> wrote:
>> >> Perhaps it might be worth to register Lua for Coverity Scan[1]?
> The main problem is that, for most of these tools, patching real bugs is
> not enough. For a program to be "clean", it must include a plethora of
> annotations peculiar to each particular tool. (Maybe Coverity Scan
> does not require such annotations; that would be great.)
[ http://lua-users.org/lists/lua-l/2011-10/msg01031.html ]
The attached patch on 5.2.0rc1 is an example of the type of changes
that can help linting on Gimpel. Two basic examples are
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
--- lua-5.2.0-orig/src/llex.c 2011-08-15 15:41:58.000000000 -0400
+++ lua-5.2.0/src/llex.c 2011-11-24 20:52:11.953228300 -0500
@@ -461,8 +461,7 @@
else return TK_CONCAT; /* '..' */
}
else if (!lisdigit(ls->current)) return '.';
- /* else go through */
- }
+ } LUA_LINT_FALLTHROUGH
case '0': case '1': case '2': case '3': case '4':
case '5': case '6': case '7': case '8': case '9': {
read_numeral(ls, seminfo);
diff -ur lua-5.2.0-orig/src/lgc.c lua-5.2.0/src/lgc.c
--- lua-5.2.0-orig/src/lgc.c 2011-10-03 13:54:25.000000000 -0400
+++ lua-5.2.0/src/lgc.c 2011-11-24 20:52:53.915556900 -0500
@@ -529,7 +529,7 @@
g->gray = p->gclist;
return traverseproto(g, p);
}
- default: lua_assert(0); return 0;
+ default: LUA_LINT_UNREACHABLE lua_assert(0); return 0;
}
}
<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<
Note that the linting commands were wrapped in regular C macros
(LUA_LINT_FALLTHROUGH and LUA_LINT_UNREACHABLE), which you are free to
redefine. Under normal compiles, those macros may be left empty. Is
it possible for Coverty and other tools to provide suitable
definitions of their own for these macros without otherwise resorting
to any source code changes? Lint can be finicky about the placement
of these annotations--e.g. for optimal specificity,
LUA_LINT_FALLTHROUGH should be outside not inside the "}" and
LUA_LINT_UNREACHABLE should be placed before not after the unreachable
statement. I'm not sure if other tools have the same preferences, but
at least something is better than nothing.
In both examples that were given, the code is already specially
annotating suspicious code via comments ("/* else go through */") or
asserts ("lua_assert(0);"). However, these LUA_LINT_* macros make the
intention explicit. Moreover, you might move the "lua_assert(0)" into
LUA_LINT_UNREACHABLE:
#ifndef LUA_LINT_UNREACHABLE
#define LUA_LINT_UNREACHABLE lua_assert(0)
#endif
diff -ur lua-5.2.0-orig/src/lapi.c lua-5.2.0/src/lapi.c
--- lua-5.2.0-orig/src/lapi.c 2011-11-16 13:51:36.000000000 -0500
+++ lua-5.2.0/src/lapi.c 2011-11-24 20:53:20.339912300 -0500
@@ -1103,8 +1103,8 @@
lua_lock(L);
api_checknelems(L, 1);
luaG_errormsg(L);
- lua_unlock(L);
- return 0; /* to avoid warnings */
+ LUA_LINT_UNREACHABLE lua_unlock(L);
+ LUA_LINT_UNREACHABLE return 0;
}
@@ -1264,7 +1264,7 @@
}
default: {
api_check(L, 0, "closure expected");
- return NULL;
+ LUA_LINT_UNREACHABLE return NULL;
}
}
}
diff -ur lua-5.2.0-orig/src/lbaselib.c lua-5.2.0/src/lbaselib.c
--- lua-5.2.0-orig/src/lbaselib.c 2011-11-23 12:29:04.000000000 -0500
+++ lua-5.2.0/src/lbaselib.c 2011-11-24 20:53:04.816441100 -0500
@@ -327,7 +327,7 @@
}
else {
luaL_error(L, "reader function must return a string");
- return NULL; /* to avoid warnings */
+ LUA_LINT_UNREACHABLE return NULL;
}
}
diff -ur lua-5.2.0-orig/src/lcode.c lua-5.2.0/src/lcode.c
--- lua-5.2.0-orig/src/lcode.c 2011-08-30 12:26:41.000000000 -0400
+++ lua-5.2.0/src/lcode.c 2011-11-24 20:53:00.153349000 -0500
@@ -542,8 +542,7 @@
case VKNUM: {
e->u.info = luaK_numberK(fs, e->u.nval);
e->k = VK;
- /* go through */
- }
+ } LUA_LINT_FALLTHROUGH
case VK: {
if (e->u.info <= MAXINDEXRK) /* constant fits in argC? */
return RKASK(e->u.info);
diff -ur lua-5.2.0-orig/src/ldebug.c lua-5.2.0/src/ldebug.c
--- lua-5.2.0-orig/src/ldebug.c 2011-10-07 16:45:19.000000000 -0400
+++ lua-5.2.0/src/ldebug.c 2011-11-24 21:02:52.990129700 -0500
@@ -367,7 +367,7 @@
setreg = pc;
break;
}
- }
+ } LUA_LINT_LOOPVARCHANGED(pc)
return setreg;
}
diff -ur lua-5.2.0-orig/src/lgc.c lua-5.2.0/src/lgc.c
--- lua-5.2.0-orig/src/lgc.c 2011-10-03 13:54:25.000000000 -0400
+++ lua-5.2.0/src/lgc.c 2011-11-24 20:52:53.915556900 -0500
@@ -529,7 +529,7 @@
g->gray = p->gclist;
return traverseproto(g, p);
}
- default: lua_assert(0); return 0;
+ default: LUA_LINT_UNREACHABLE lua_assert(0); return 0;
}
}
@@ -994,7 +994,7 @@
return GCSWEEPCOST;
}
}
- default: lua_assert(0); return 0;
+ default: LUA_LINT_UNREACHABLE lua_assert(0); return 0;
}
}
diff -ur lua-5.2.0-orig/src/llex.c lua-5.2.0/src/llex.c
--- lua-5.2.0-orig/src/llex.c 2011-08-15 15:41:58.000000000 -0400
+++ lua-5.2.0/src/llex.c 2011-11-24 20:52:11.953228300 -0500
@@ -461,8 +461,7 @@
else return TK_CONCAT; /* '..' */
}
else if (!lisdigit(ls->current)) return '.';
- /* else go through */
- }
+ } LUA_LINT_FALLTHROUGH
case '0': case '1': case '2': case '3': case '4':
case '5': case '6': case '7': case '8': case '9': {
read_numeral(ls, seminfo);
diff -ur lua-5.2.0-orig/src/lmem.c lua-5.2.0/src/lmem.c
--- lua-5.2.0-orig/src/lmem.c 2011-09-20 15:25:23.000000000 -0400
+++ lua-5.2.0/src/lmem.c 2011-11-24 20:52:01.333379800 -0500
@@ -65,7 +65,7 @@
void *luaM_toobig (lua_State *L) {
luaG_runerror(L, "memory allocation error: block too big");
- return NULL; /* to avoid warnings */
+ LUA_LINT_UNREACHABLE return NULL;
}
diff -ur lua-5.2.0-orig/src/loadlib.c lua-5.2.0/src/loadlib.c
--- lua-5.2.0-orig/src/loadlib.c 2011-11-10 06:42:58.000000000 -0500
+++ lua-5.2.0/src/loadlib.c 2011-11-24 19:31:11.089977100 -0500
@@ -12,10 +12,6 @@
/*
** if needed, includes windows header before everything else
*/
-#if defined(LUA_DL_DLL)
-#include <windows.h>
-#endif
-
#include <stdlib.h>
#include <string.h>
@@ -26,6 +22,10 @@
#include "lua.h"
+#if defined(LUA_DL_DLL)
+#include <windows.h>
+#endif
+
#include "lauxlib.h"
#include "lualib.h"
diff -ur lua-5.2.0-orig/src/luaconf.h lua-5.2.0/src/luaconf.h
--- lua-5.2.0-orig/src/luaconf.h 2011-11-09 09:47:14.000000000 -0500
+++ lua-5.2.0/src/luaconf.h 2011-11-24 21:08:19.113542100 -0500
@@ -518,7 +518,16 @@
#endif /* } */
-
+/* May be redefined for linting */
+#ifndef LUA_LINT_UNREACHABLE
+#define LUA_LINT_UNREACHABLE
+#endif
+#ifndef LUA_LINT_FALLTHROUGH
+#define LUA_LINT_FALLTHROUGH
+#endif
+#ifndef LUA_LINT_LOOPVARCHANGED
+#define LUA_LINT_LOOPVARCHANGED(x)
+#endif
/* =================================================================== */
