Giter Club home page Giter Club logo

luata-quickcheck's Introduction

LuaTA : Lua Type Analysis and corresponding QuickCheck code

This is a static analysis for conservatively inferring run-time types of Lua programs. It forms the case study contained in the paper

QuickChecking Static Analysis Properties
Jan Midtgaard and Anders Møller
Proceedings of ICST'15
http://janmidtgaard.dk/papers/Midtgaard-Moeller:ICST15.pdf

which focuses on testing properties related to static analyses (lattice properties, and monotonicity, strictness, and invariance of operations) using the increasingly popular QuickCheck methodology.

Note: the present analysis has been updated since the publication of the above paper.

The full source code of the analysis is available from this very URL https://github.com/jmid/luata-quickcheck

The analysis can be built as a command line client or as a web client available at http://jmid.github.io/luata-quickcheck/

The coverage reports mentioned in the paper are available in the sub-directories:

Requirements:

  • OCaml, version 4.01.0 or newer
    • ocamlp4-extra (for 'camlp4of', required by bisect below)
  • OCaml libraries/tools (through OPAM):
  • GNU Make

The web interface further requires:

  • Js_of_ocaml (available through OPAM)
  • CodeMirror (included)
  • TextHover addon to CodeMirror (also included)

License:

The analysis is released under a BSD license. The visualizer builds on CodeMirror which is MIT licensed, and the TextHover addon by Angelo Zerr.

Analysis instructions:

The file doc/luata-doc.md provides a basic description of the analysis architecture as well as an explanation of its output.

The analysis comes with both a command line interface and a web client.

To build the command line client, run:

$ make

To run the analysis on a Lua program, for example (see examples/ directory for other examples):

$ ./luata examples/table06.lua

The result will now be printed to the console.

To reduce the amount of console output passing the option -no-heap will just emit the warnings:

$ ./luata -no-heap examples/table06.lua

Alternatively you can build the web client with

$ make js

The web client is now available as an HTML page with overlays in index.html (view with a web browser and shrink fontsize).

Quickcheck instructions:

The source code for the QuickCheck LCheck module is included in src/lCheck.ml for convenience, but is also separately available from http://github.com/jmid/lcheck

The source code applying LCheck to the Lua type analyses is available in src/edslcheck.ml

To rerun our quickchecking on the type analysis:

$ make -B edslcheck
$ ./edslcheck

Warning: the last step takes a full lunchbreak! You can comment out some tests at the bottom of src/edslcheck.ml to run fewer tests.

Report instructions:

To reproduce the numbers in the paper's Table 1, regarding QuickCheck, test suite, and combined coverage, follow the below instructions.

  • To reproduce the QuickCheck coverage numbers:

    Run:

    $ make -B edslcheckcov
$ make -B runedslcheckcov
$ make -B checkreport

    (Warning: the second step takes a full lunchbreak) The resulting report is now available in HTML format in cov-report-qcheck/index.html

  • To reproduce the original test suite coverage numbers:

    Run:

    $ make -B testcov
$ make -B runtestcov
$ make -B testreport

    The resulting report is now available in HTML format in cov-report-test/index.html

  • To reproduce the combined coverage numbers:

    First run both the above (which will generate cov-report-qcheck.out and cov-report-test.out). Then

    $ make -B combinedreport

    The resulting report is now available in HTML format in cov-report-combined/index.html

luata-quickcheck's People

Contributors

jmid avatar

Stargazers

avatar avatar avatar avatar avatar avatar

Watchers

avatar avatar avatar avatar avatar

Forkers

algobardo

luata-quickcheck's Issues

Uncertainty in function return types is lost

The analysis seems to be confident that c is going to have a number type instead of the actual nil type. The analysis correctly identifies that the second return value might have number type (based on my understanding of the question mark) ? { number: Top } however the analysis seems to give the wrong confidence to the type of b with ! { number: Top }

local function f(x)
        if x > 10 then
                return 1,2 
        else
                return 3
        end 
end

a,b=f(0)
c=type(b)
print(c)

Expected output:

$ lua mytest.lua
nil

__metatable is considered when resolving metamethods

It appears that the __metatable field of a metatable is considered when resolving metamethods. (At least in Lua 5.1, 5.2 and 5.3) it is the case that __metatable is only consulted when calling the getmetatable built-in from Lua code. It is not consulted when resolving actual metamethods. It exists only as a protection mechanism for metatables, and not for overloading them from the point of view of Lua.

This discrepancy causes luata to produce incorrect output for code using the __metatable metamethod.

local complexMt = { __metatable = "Complex number metatable protected" }

local function Complex(real,imag)
   local n = {real = real, imag = imag}
   setmetatable(n, complexMt)
   return n
end

function complexMt.__add(x,y)
   return Complex(x.real + y.real, x.imag + y.imag)
end

function complexMt:__tostring()
   return self.real .. "+" .. self.imag .. "i" 
end

z = Complex(1,0) + Complex(0,2)
print(z)

Expected output

$ lua mytest.lua
1+2i

License is missing

Hi!

I'm working on an editor plugin for Lua (atom-autocomplete-lua) and I would like to rewrite it using proper lattices. It would be really helpful to be able to use some of the code from this repo (especially the lexer and parser), but I can't do that because there is no license on this repo. Might you consider adding a LICENSE file? Maybe something permissive like the MIT license?

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.