Skip to content

Zeta611/prospect-analyzer

BranchesTags

Folders and files

NameName
Last commit message
Last commit date

Latest commit

Β 

History

72 Commits
bin
bin
Β 
Β 
doc
doc
Β 
Β 
lib
lib
Β 
Β 
tests
tests
Β 
Β 
.gitignore
.gitignore
Β 
Β 
.ocamlformat
.ocamlformat
Β 
Β 
README.md
README.md
Β 
Β 
capture.png
capture.png
Β 
Β 
dune-project
dune-project
Β 
Β 
prospect_analyzer.opam
prospect_analyzer.opam
Β 
Β 

Repository files navigation

Prospect Analyzer

See the documentation for the target language syntax and semantics.

The shape analyzer determines which paths are "shape-safe", and the value analyzer checks if each path can indeed yield the provided output value. The shape analysis uses a non-deterministic Damas-Milner type inference, since the target language is not statically typed. The value analysis utilizes the Z3 theorem prover to prune branches as early as possible, as well as to unify with the output value.

Usage

To run, execute

./_build/default/bin/main.exe -all test.l

after dune build.

When the flag -all is omitted, only shape analysis is done.

Sample code

# lang 1
# (0, 0) 1
# (1, 1) 0
let h []
let a h.1
let b h.2
if (a + b)
  if (a + b) (a + a + 1) b
  if (a + b) b (a + a + 1)

should output

Shape & value analyzer. tests/test_7.l (L1)
Sample: ((0, 0), 1)
[let x = [([0 : β„“3], [0 : β„“4]) : β„“2] in [let h = [[] : β„“6] in [let a = [[h : β„“9].1 : β„“8] in [let b = [[h : β„“12].2 : β„“11] in [if [[a : β„“15] + [b : β„“16] : β„“14] [if [[a : β„“19] + [b : β„“20] : β„“18] [[[a : β„“23] + [a : β„“24] : β„“22] + [1 : β„“25] : β„“21] [b : β„“26] : β„“17] [if [[a : β„“29] + [b : β„“30] : β„“28] [b : β„“31] [[[a : β„“34] + [a : β„“35] : β„“33] + [1 : β„“36] : β„“32] : β„“27] : β„“13] : β„“10] : β„“7] : β„“5] : β„“1]
| []: (ΞΉ, ΞΉ), O: ΞΉ, Trace: let . = (.) in (let . = (.) in (let . = (.) in (if (. + .) β‰  0 if (. + .) β‰  0 . + . + .))); β„“1-β„“2-β„“3-β„“4-β„“5-β„“6-β„“7-β„“8-β„“9-β„“10-β„“11-β„“12-β„“13-β„“14-β„“15-β„“16-β„“17-β„“18-β„“19-β„“20-β„“21-β„“22-β„“23-β„“24-β„“25
| Eval: 1 + 2[2]
[let x = [([0 : β„“3], [0 : β„“4]) : β„“2] in [let h = [[] : β„“6] in [let a = [[h : β„“9].1 : β„“8] in [let b = [[h : β„“12].2 : β„“11] in [if [[a : β„“15] + [b : β„“16] : β„“14] [if [[a : β„“19] + [b : β„“20] : β„“18] [[[a : β„“23] + [a : β„“24] : β„“22] + [1 : β„“25] : β„“21] [b : β„“26] : β„“17] [if [[a : β„“29] + [b : β„“30] : β„“28] [b : β„“31] [[[a : β„“34] + [a : β„“35] : β„“33] + [1 : β„“36] : β„“32] : β„“27] : β„“13] : β„“10] : β„“7] : β„“5] : β„“1]
| []: (ΞΉ, ΞΉ), O: ΞΉ, Trace: let . = (.) in (let . = (.) in (let . = (.) in (if (. + .) β‰  0 if (. + .) = 0 .))); β„“1-β„“2-β„“3-β„“4-β„“5-β„“6-β„“7-β„“8-β„“9-β„“10-β„“11-β„“12-β„“13-β„“14-β„“15-β„“16-β„“17-β„“18-β„“19-β„“20-β„“26
| Falsy value found when guide_path expected a truthy value
[let x = [([0 : β„“3], [0 : β„“4]) : β„“2] in [let h = [[] : β„“6] in [let a = [[h : β„“9].1 : β„“8] in [let b = [[h : β„“12].2 : β„“11] in [if [[a : β„“15] + [b : β„“16] : β„“14] [if [[a : β„“19] + [b : β„“20] : β„“18] [[[a : β„“23] + [a : β„“24] : β„“22] + [1 : β„“25] : β„“21] [b : β„“26] : β„“17] [if [[a : β„“29] + [b : β„“30] : β„“28] [b : β„“31] [[[a : β„“34] + [a : β„“35] : β„“33] + [1 : β„“36] : β„“32] : β„“27] : β„“13] : β„“10] : β„“7] : β„“5] : β„“1]
| []: (ΞΉ, ΞΉ), O: ΞΉ, Trace: let . = (.) in (let . = (.) in (let . = (.) in (if (. + .) = 0 if (. + .) β‰  0 .))); β„“1-β„“2-β„“3-β„“4-β„“5-β„“6-β„“7-β„“8-β„“9-β„“10-β„“11-β„“12-β„“13-β„“14-β„“15-β„“16-β„“27-β„“28-β„“29-β„“30-β„“31
| Falsy value found when guide_path expected a truthy value
[let x = [([0 : β„“3], [0 : β„“4]) : β„“2] in [let h = [[] : β„“6] in [let a = [[h : β„“9].1 : β„“8] in [let b = [[h : β„“12].2 : β„“11] in [if [[a : β„“15] + [b : β„“16] : β„“14] [if [[a : β„“19] + [b : β„“20] : β„“18] [[[a : β„“23] + [a : β„“24] : β„“22] + [1 : β„“25] : β„“21] [b : β„“26] : β„“17] [if [[a : β„“29] + [b : β„“30] : β„“28] [b : β„“31] [[[a : β„“34] + [a : β„“35] : β„“33] + [1 : β„“36] : β„“32] : β„“27] : β„“13] : β„“10] : β„“7] : β„“5] : β„“1]
| []: (ΞΉ, ΞΉ), O: ΞΉ, Trace: let . = (.) in (let . = (.) in (let . = (.) in (if (. + .) = 0 if (. + .) = 0 . + . + .))); β„“1-β„“2-β„“3-β„“4-β„“5-β„“6-β„“7-β„“8-β„“9-β„“10-β„“11-β„“12-β„“13-β„“14-β„“15-β„“16-β„“27-β„“28-β„“29-β„“30-β„“32-β„“33-β„“34-β„“35-β„“36
| Eval: 1 + 2[2]
Sample: ((1, 1), 0)
[let x = [([1 : β„“3], [1 : β„“4]) : β„“2] in [let h = [[] : β„“6] in [let a = [[h : β„“9].1 : β„“8] in [let b = [[h : β„“12].2 : β„“11] in [if [[a : β„“15] + [b : β„“16] : β„“14] [if [[a : β„“19] + [b : β„“20] : β„“18] [[[a : β„“23] + [a : β„“24] : β„“22] + [1 : β„“25] : β„“21] [b : β„“26] : β„“17] [if [[a : β„“29] + [b : β„“30] : β„“28] [b : β„“31] [[[a : β„“34] + [a : β„“35] : β„“33] + [1 : β„“36] : β„“32] : β„“27] : β„“13] : β„“10] : β„“7] : β„“5] : β„“1]
| []: (ΞΉ, ΞΉ), O: ΞΉ, Trace: let . = (.) in (let . = (.) in (let . = (.) in (if (. + .) β‰  0 if (. + .) β‰  0 . + . + .))); β„“1-β„“2-β„“3-β„“4-β„“5-β„“6-β„“7-β„“8-β„“9-β„“10-β„“11-β„“12-β„“13-β„“14-β„“15-β„“16-β„“17-β„“18-β„“19-β„“20-β„“21-β„“22-β„“23-β„“24-β„“25
| Eval: 1 + 2[2] failed to unify with the output
[let x = [([1 : β„“3], [1 : β„“4]) : β„“2] in [let h = [[] : β„“6] in [let a = [[h : β„“9].1 : β„“8] in [let b = [[h : β„“12].2 : β„“11] in [if [[a : β„“15] + [b : β„“16] : β„“14] [if [[a : β„“19] + [b : β„“20] : β„“18] [[[a : β„“23] + [a : β„“24] : β„“22] + [1 : β„“25] : β„“21] [b : β„“26] : β„“17] [if [[a : β„“29] + [b : β„“30] : β„“28] [b : β„“31] [[[a : β„“34] + [a : β„“35] : β„“33] + [1 : β„“36] : β„“32] : β„“27] : β„“13] : β„“10] : β„“7] : β„“5] : β„“1]
| []: (ΞΉ, ΞΉ), O: ΞΉ, Trace: let . = (.) in (let . = (.) in (let . = (.) in (if (. + .) β‰  0 if (. + .) = 0 .))); β„“1-β„“2-β„“3-β„“4-β„“5-β„“6-β„“7-β„“8-β„“9-β„“10-β„“11-β„“12-β„“13-β„“14-β„“15-β„“16-β„“17-β„“18-β„“19-β„“20-β„“26
| Falsy value found when guide_path expected a truthy value
[let x = [([1 : β„“3], [1 : β„“4]) : β„“2] in [let h = [[] : β„“6] in [let a = [[h : β„“9].1 : β„“8] in [let b = [[h : β„“12].2 : β„“11] in [if [[a : β„“15] + [b : β„“16] : β„“14] [if [[a : β„“19] + [b : β„“20] : β„“18] [[[a : β„“23] + [a : β„“24] : β„“22] + [1 : β„“25] : β„“21] [b : β„“26] : β„“17] [if [[a : β„“29] + [b : β„“30] : β„“28] [b : β„“31] [[[a : β„“34] + [a : β„“35] : β„“33] + [1 : β„“36] : β„“32] : β„“27] : β„“13] : β„“10] : β„“7] : β„“5] : β„“1]
| []: (ΞΉ, ΞΉ), O: ΞΉ, Trace: let . = (.) in (let . = (.) in (let . = (.) in (if (. + .) = 0 if (. + .) β‰  0 .))); β„“1-β„“2-β„“3-β„“4-β„“5-β„“6-β„“7-β„“8-β„“9-β„“10-β„“11-β„“12-β„“13-β„“14-β„“15-β„“16-β„“27-β„“28-β„“29-β„“30-β„“31
| Falsy value found when guide_path expected a truthy value
[let x = [([1 : β„“3], [1 : β„“4]) : β„“2] in [let h = [[] : β„“6] in [let a = [[h : β„“9].1 : β„“8] in [let b = [[h : β„“12].2 : β„“11] in [if [[a : β„“15] + [b : β„“16] : β„“14] [if [[a : β„“19] + [b : β„“20] : β„“18] [[[a : β„“23] + [a : β„“24] : β„“22] + [1 : β„“25] : β„“21] [b : β„“26] : β„“17] [if [[a : β„“29] + [b : β„“30] : β„“28] [b : β„“31] [[[a : β„“34] + [a : β„“35] : β„“33] + [1 : β„“36] : β„“32] : β„“27] : β„“13] : β„“10] : β„“7] : β„“5] : β„“1]
| []: (ΞΉ, ΞΉ), O: ΞΉ, Trace: let . = (.) in (let . = (.) in (let . = (.) in (if (. + .) = 0 if (. + .) = 0 . + . + .))); β„“1-β„“2-β„“3-β„“4-β„“5-β„“6-β„“7-β„“8-β„“9-β„“10-β„“11-β„“12-β„“13-β„“14-β„“15-β„“16-β„“27-β„“28-β„“29-β„“30-β„“32-β„“33-β„“34-β„“35-β„“36
| Eval: 1 + 2[2] failed to unify with the output

The output is xterm-256 colorized: Capture

About

πŸ•³οΈ Prospect analysis

Topics

static-analysis

Resources

Readme
Activity

Stars

6 stars

Watchers

2 watching

Forks

0 forks
Report repository

Releases

No releases published

Packages

No packages published

Contributors 2

  •  
  •  

Languages