From af2c82cfd7f2318fcd81da2ea4cf3fd695db3b40 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 28 Apr 2021 18:14:53 +0200 Subject: start the new "BTL" IR. --- Makefile | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 62635d70..90c39907 100644 --- a/Makefile +++ b/Makefile @@ -82,6 +82,7 @@ VLIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \ Iteration.v Zbits.v Integers.v Archi.v IEEE754_extra.v Floats.v \ Parmov.v UnionFind.v Wfsimpl.v \ Postorder.v FSetAVLplus.v IntvSets.v Decidableplus.v BoolEqual.v \ + OptionMonad.v \ ImpConfig.v ImpExtern.v ImpIO.v ImpMonads.v \ ImpCore.v ImpHCons.v ImpLoops.v ImpPrelude.v @@ -141,7 +142,8 @@ SCHEDULING= \ RTLpathLivegen.v RTLpathSE_impl.v \ RTLpathproof.v RTLpathSE_theory.v \ RTLpathSchedulerproof.v RTLpath.v \ - RTLpathScheduler.v RTLpathWFcheck.v + RTLpathScheduler.v RTLpathWFcheck.v \ + BTL.v BTLtoRTL.v BTLtoRTLproof.v \ # C front-end modules (in cfrontend/) -- cgit From c7bc74b1860f30df678bf384a32cd9c6eb113beb Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 6 May 2021 09:07:07 +0200 Subject: start RTL -> BTL --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 90c39907..934b8586 100644 --- a/Makefile +++ b/Makefile @@ -143,7 +143,7 @@ SCHEDULING= \ RTLpathproof.v RTLpathSE_theory.v \ RTLpathSchedulerproof.v RTLpath.v \ RTLpathScheduler.v RTLpathWFcheck.v \ - BTL.v BTLtoRTL.v BTLtoRTLproof.v \ + BTL.v BTLtoRTL.v BTLtoRTLproof.v RTLtoBTL.v RTLtoBTLproof.v # C front-end modules (in cfrontend/) -- cgit From 5757c5a377b54464b37bdce6a6f9630caefef826 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 6 May 2021 17:28:07 +0200 Subject: init BTL_SEtheory (by copy/paste from RTLpathSE_theory) --- Makefile | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 934b8586..29c1816f 100644 --- a/Makefile +++ b/Makefile @@ -143,7 +143,8 @@ SCHEDULING= \ RTLpathproof.v RTLpathSE_theory.v \ RTLpathSchedulerproof.v RTLpath.v \ RTLpathScheduler.v RTLpathWFcheck.v \ - BTL.v BTLtoRTL.v BTLtoRTLproof.v RTLtoBTL.v RTLtoBTLproof.v + BTL.v BTLtoRTL.v BTLtoRTLproof.v RTLtoBTL.v RTLtoBTLproof.v \ + BTL_SEtheory.v # C front-end modules (in cfrontend/) -- cgit From 25595a7b34b70011dcb77aae277ee1cdb8920c60 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 28 May 2021 14:28:56 +0200 Subject: splitting BTL by introducing BTLmatchRTL reduce also copy-paste between BTLtoRTLproof and RTLtoBTLproof sharing is done in BTLmatchRTL --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 29c1816f..3d9e8bdd 100644 --- a/Makefile +++ b/Makefile @@ -143,7 +143,7 @@ SCHEDULING= \ RTLpathproof.v RTLpathSE_theory.v \ RTLpathSchedulerproof.v RTLpath.v \ RTLpathScheduler.v RTLpathWFcheck.v \ - BTL.v BTLtoRTL.v BTLtoRTLproof.v RTLtoBTL.v RTLtoBTLproof.v \ + BTL.v BTLmatchRTL.v BTLtoRTL.v BTLtoRTLproof.v RTLtoBTL.v RTLtoBTLproof.v \ BTL_SEtheory.v # C front-end modules (in cfrontend/) -- cgit From b79d0a04787d9234cf580841bf58e592fe4ab3ee Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 28 May 2021 15:24:16 +0200 Subject: starting to extend RTLtoBTL with Liveness checking (on BTL side) --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 3d9e8bdd..60cf380b 100644 --- a/Makefile +++ b/Makefile @@ -144,7 +144,7 @@ SCHEDULING= \ RTLpathSchedulerproof.v RTLpath.v \ RTLpathScheduler.v RTLpathWFcheck.v \ BTL.v BTLmatchRTL.v BTLtoRTL.v BTLtoRTLproof.v RTLtoBTL.v RTLtoBTLproof.v \ - BTL_SEtheory.v + BTL_Livecheck.v BTL_Scheduler.v BTL_Schedulerproof.v BTL_SEtheory.v # C front-end modules (in cfrontend/) -- cgit From f6a3483c7dcac5ed56a349361a19dc1f4c985de3 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Tue, 1 Jun 2021 17:16:06 +0200 Subject: starting BTL_SEsimuref --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 60cf380b..a5cc8895 100644 --- a/Makefile +++ b/Makefile @@ -144,7 +144,7 @@ SCHEDULING= \ RTLpathSchedulerproof.v RTLpath.v \ RTLpathScheduler.v RTLpathWFcheck.v \ BTL.v BTLmatchRTL.v BTLtoRTL.v BTLtoRTLproof.v RTLtoBTL.v RTLtoBTLproof.v \ - BTL_Livecheck.v BTL_Scheduler.v BTL_Schedulerproof.v BTL_SEtheory.v + BTL_Livecheck.v BTL_Scheduler.v BTL_Schedulerproof.v BTL_SEtheory.v BTL_SEsimuref.v # C front-end modules (in cfrontend/) -- cgit From f59ff208a301bf3f04aab350d9f0b3b217ddeac3 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 19 Jul 2021 14:20:53 +0200 Subject: Finish implem proof, need to adapt scheduler proof --- Makefile | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index ef1048b3..c4c45291 100644 --- a/Makefile +++ b/Makefile @@ -162,7 +162,8 @@ SCHEDULING= \ RTLpathSchedulerproof.v RTLpath.v \ RTLpathScheduler.v RTLpathWFcheck.v \ BTL.v BTLmatchRTL.v BTLtoRTL.v BTLtoRTLproof.v RTLtoBTL.v RTLtoBTLproof.v \ - BTL_Livecheck.v BTL_Scheduler.v BTL_Schedulerproof.v BTL_SEtheory.v BTL_SEsimuref.v + BTL_Livecheck.v BTL_Scheduler.v BTL_Schedulerproof.v\ + BTL_SEtheory.v BTL_SEsimuref.v BTL_SEimpl.v # C front-end modules (in cfrontend/) -- cgit From c3ce32da7d431069ef355296bef66b112a302b78 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 20 Jul 2021 12:32:21 +0200 Subject: op simplify BTL intro --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index c4c45291..c9255fdb 100644 --- a/Makefile +++ b/Makefile @@ -152,7 +152,7 @@ BACKEND=\ Mach.v \ Bounds.v Stacklayout.v Stacking.v Stackingproof.v \ Asm.v Asmgen.v Asmgenproof.v Asmaux.v \ - RTLpathSE_simplify.v \ + RTLpathSE_simplify.v BTL_SEsimplify.v \ $(BACKENDLIB) SCHEDULING= \ -- cgit From a3319eb05543930844dedd9ac31ed1beaac3047e Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 20 Jul 2021 15:21:29 +0200 Subject: Fix compile on ARM/x86 backends --- Makefile | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index c9255fdb..10c4f4bf 100644 --- a/Makefile +++ b/Makefile @@ -152,15 +152,10 @@ BACKEND=\ Mach.v \ Bounds.v Stacklayout.v Stacking.v Stackingproof.v \ Asm.v Asmgen.v Asmgenproof.v Asmaux.v \ - RTLpathSE_simplify.v BTL_SEsimplify.v \ + BTL_SEsimplify.v \ $(BACKENDLIB) SCHEDULING= \ - RTLpathLivegenproof.v RTLpathSE_simu_specs.v \ - RTLpathLivegen.v RTLpathSE_impl.v \ - RTLpathproof.v RTLpathSE_theory.v \ - RTLpathSchedulerproof.v RTLpath.v \ - RTLpathScheduler.v RTLpathWFcheck.v \ BTL.v BTLmatchRTL.v BTLtoRTL.v BTLtoRTLproof.v RTLtoBTL.v RTLtoBTLproof.v \ BTL_Livecheck.v BTL_Scheduler.v BTL_Schedulerproof.v\ BTL_SEtheory.v BTL_SEsimuref.v BTL_SEimpl.v -- cgit