Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

L6 ANF from L6 CPS #10

Closed
wants to merge 82 commits into from
Closed

L6 ANF from L6 CPS #10

wants to merge 82 commits into from

Conversation

zoep
Copy link
Member

@zoep zoep commented Oct 30, 2019

This is a "dummy" pull request so we can comment and discuss about the L6 changes and what's needed to patch the proofs.

The state of the L6 pipeline is:

  • Uncurring : needs patching
  • Beta contraction (i.e. inlining) : unproved
  • Shrink reduction : needs patching
  • Lambda lifting: needs patching
  • Closure conversion + hoisting : needs patching
  • Dead param elim: unproved

End-to-end proof (including sep. compilation): unproved

Olivier Savary Belanger and others added 30 commits September 29, 2019 15:05
Rolled back compute_fEnv_fds since it only worked for known functions…
577d81c 
…. Fixed timePhase L0
Added benchmarks target to the benchmarks/Makefile, with benchmarks/b…
b1db5c8 
…enchmarks.expected as expected output when run with T2. Added sha256 benchmark from VST, removed for now the header generation from L6_to_Clight as name collision were causing bigger benchmarks to fail
Added a README in the benchmarks folder documenting the use of timePhase
3f0c167
@mzweav
Name shadowing fix and removed Focus warnings
dfede3e
@mzweav
added 6 fun param version of code gen
59fc45c
@zoep
CP in ANF
8495334
@mzweav
Merge remote-tracking branch 'origin/zoe_lambda-lifting' into code_ge…
d98fee7 
…n_opt
@mzweav
Removed redundant files/parameterized function arguments
0d72a3b
@joom
Progress on generating printers: constructor names can be printed now
c79247c
@joom
More comments on printing
88dc9f9
@mzweav
progress on proof
22bf94a
Some progress on Eapp case
d17244e
(stub of) Proof progressed to end of Eapp case
5973944
Fix repr_asgn_fun_entry for expected Hlenv_new'''_asgn_i
852630a
@mzweav
progress on proof
a58b2fe
@joom
Move glue code generation to a different module
2e4920e
@joom
Progress on glue code generation: printers and constructor name arrays
48b01e3
@zoep
Fixed bug in dead param elim that resulted in empty C file
3efe0cc
@zoep
error support in L6 state
e149590
@zoep
Two different L6 pipelines (CPS and ANF)
63f0ade
@zoep
solved merge conflit
4ad4a14
@zoep
CP in code extraction
1b127e7
@joom
Progress using L1 constructor types in glue code generation
91baba2
@zoep
CP in code generation
f75f70b
@zoep
C code generation for ANF
91a242c
@joom
Getting glue code generation ready for parametrized types, and moving…
dc3f271 
… some code from L6_to_Clight to Glue
@zoep
WIP in GC with shadow stack
3c655b4
@zoep
Fixed some bus in shadow stack GC
1906f1c
@zoep
CP before fix
7b81584
@zoep
Big fix in inline letapp in shrink reduction and beta contruction
59288c3
zoep and others added 29 commits November 4, 2019 19:54
@zoep
WIP in parameterizing CC proof with bounds (as opposed to showing the…
d8a4f48 
… theorem for conctrete bounds)
@zoep
Progress in proofs
76cf277
@john-ml
WIP correctness of inlining
9524e02
@john-ml
Start app/letapp inlining cases
1a9f409
@zoep
More tweaks in CC proof
989bbbd
@zoep
Merge branch 'zoe-ANF' of github.com:PrincetonUniversity/certicoq int…
aa2882a 
…o zoe-ANF
@zoep
Updated hoisting proof
035b5f0
@zoep
Updated compat lemmas
3aec56d
@zoep
Commented out alpha_conv proof currently (needs update for bounds and…
2749c03 
… new compat lemmas
@zoep
Fixed compat lemmmas in hoisting proof
6156092
@zoep
Some cleanup in hoisting
a581928
@zoep
Updated bound_stem
2f95636
@zoep
CP
1d7e8a3
@joom
Correct print functions generated for monomorphic types
2188e50
Merge remote-tracking branch 'remotes/origin/timing' into code_gen_opt
0d760bf
@joom
Rudimentary polymorphic print functions done, needs some cleanup
33aaf34
@zoep
Compositionality experiments
7d7f0c4
@zoep
WIP in updating alpha_conv proof
8a6507e
@joom
Polymorphic print functions + moved constructor generation to glue.v
3fe127c
@zoep
WIP in alpha_conv, and removed dead_param_elim from pipeline again
7eb8d73
@zoep
Removed alpha_conv from build for now
202dd46
@john-ml
WIP Inlining proof
0a9b683
@john-ml
Merge branch 'zoe-ANF' of https://github.com/PrincetonUniversity/cert…
a5931a1 
…icoq into HEAD
@joom
Merge remote-tracking branch 'origin/code_gen_opt'
69f3c04
@joom
Fix compile error and styling in L6_to_Clight.v
9a4ff61
@zoep
Finished with the Alpha_conv proof
6b849fe
@zoep
Merged with Joomy
00413ea
@zoep
Fix after merge
8c73622
@joom
Some changes in tests etc after merge
f4128c6
@zoep zoep closed this Dec 10, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@zoep @mzweav @joom @john-ml