Skip to content

A simple programming language for program verification using Z3, ANTLR4 & Parser Combinators written using Scala

License

Notifications You must be signed in to change notification settings

codersguild/simplr

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

76 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Build Status Scala

Project

Demonstrate parsing, and constraint solving on a new programming language simplr using scala, z3, ANTLR4 and LLVM.

Run

Folder simpl is the base folder for all scala code.

$ cd code
$ sbt
(wait for build to complete...)

$ ~run ./samples/simple.simpl

~ for re-run on file changes.

Grammar

The grammar for simplr, is in parser/grammar folder.

assert (x + y * 90 > 500);

Parse Tree

Parse-Tree

Sample Output

We pass simple.simpl file to our lexer-parser and run parsing to generate constraints as per assert statements. Conditional Statements not covered yet.

Z3 run on dummy constraints using scala z3 api . See function ExampleZ3Solving() in parser.scala.

For simple.simplr file program.

        Assign : x = 90
        AssignRuleAdded
        Assign : y = 7898
        AssignRuleAdded
        Assign : m = 1
        AssignRuleAdded
        Assign : z = 27717
        AssignRuleAdded
        GreaterThanRuleAdded
        LessThanRuleAdded
        Print : 39600
        GreaterThanRuleAdded
        Print : 90
        Print : 23
        Print : 7898
        Print : 27717
        NotEqualRuleAdded
        NotEqualRuleAdded
        Assign : n = 0
        AssignRuleAdded
        Print : 2154118
        LessThanRuleAdded
        Print : 7988

        No of Z3 Assertions : 11
        __m = 1
        __x > 0
        __z > 90
        __n = 0
        __z < 0
        __x = 90
        __z != 420462
        __y != 616
        __y = 7898
        __z = 27717
        __x < 218908866

        Not Satisfiable

TO-DO

  1. Convert the processing into passes.
  2. Check and Print Z3 Model.
  3. Handle Function Calls.
  4. Improve the token matching.

Working

  1. Z3 Modelling.
  2. New Grammar definition for functions & multi-line block statements.
  3. Fix Z3 Linking errors.
  4. Add Z3 Symbolic Equations

About

A simple programming language for program verification using Z3, ANTLR4 & Parser Combinators written using Scala

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published