Read papers by Gabriel
Talk on MLTS
Coffee with everyone there
Finished reading papers
The source language is the pattern match section of the code:
match x with
| p1 -> e1
| p2 | p3 -> e2
| p4 when c1 -> e3
while the target language is the lambda representation given by ocamlc -dlambda (or rawlambda):
(let (match/1215 =a (field 0 lt/1210))
case tag 2:
(if (field 1 lt/1210) (exit 1)
(if (== (field 0 match/1215) 2) "K3 2" (exit 1)))
default: (exit 1)))
with (1) "[_, _]")))
Three cases not considered: (x>0, _) -> e1 with constraint (x>0, y>0) -> e1. Come si vede, il secondo rispetta il primo ma non viceversa, eppure per come lo ho formulato andiamo a controllare che tutti i costraint delle variabili simboliche rispettino i patterns dati, quindi sarebbe stato definito corretto quando non lo e`.
Secondo caso, costraint non validi: x>0 and x<0, possono succedere nel compilatore, nel mio caso dovrei eliminarli.
Terzo ed ultimo caso, pattern non raggiungibili: | A -> "a" | B -> "b" | _ -> "_" | C -> "c";; "c" non e` raggiungibile ma il mio test fallirebbe in quanto e4 non e` espressa in lambda.
Plan for the next days:
* open a repo
* describe the grammar of the source language
* describe the grammar of the target language
* write the algorithm, almost formally
Drafted a first version of the grammar for the source and target language.
Opened a github repository, with Gabriel as collaborator
Conference about delta-caml in the morning. Felt sick and spent the afternoon resting.
Applied Gabriel's fixes to the grammar file.
Drafted the algorithm.
Version of the algorithm to be discussed with Gabriel
Read and discussed the work of Steve Dolan. Wrote a mail to him noting the differences.
Discussed with Gabriel his notes, merged them into the repo
Applied fixes to algorithm.md
Started to think about a better formulation for equivalence of ρ-constraints and ι-constraints
Sent a mail to Gabriel with a paper, a doubt on how compiler optimization could impact our work and a proposal for the the formulation of the equivalence checking.
The doubt is the following:
the compiler could optimize for assertions outside of the function scope.
In that case propositions in the lambda code could cover only parts of the domain of the values but our tool would fail.
Read the paper in order to grasp the math behind it and investigated for a better formulation of equivalence between rho-constraints and iota-constraints.
Gabriel and I discussed the mail.
We noted the following:
1. We would hook exactly around the pattern-matching compiler, not the
further optimizations, so that's not an issue. (If later the
pattern-matching compiler starts taking global-optimization-knowledge
into account, we can extend our verifier to do the same.)
2. The paper I sent is interesting, but our work, even if it shares a lot of theoretical ground, aims at the ocaml compiler and wants to cover more ground than what described on the paper.
3. We discussed how to represent patterns as a tree of concrete value and accessors.
Asked Gabriel for help in providing a matemathical notation.
Wrote to Moreau for a follow up on the formal verifier for the TOM language.
Spent the day with Gabriel working on the mathematical notation of the problem at the blackboard.
Talked about the implementation;
did pair programming and wrote the types for the symbolic engine
Read a "Survey of Symbolic Execution Techniques".
worked on the implementation a little bit more.
Replied to Moreau;
still working on implementation.