Skip to content

Commit e3f64d9

Browse files
Dongjoo-KimDongjoo-Kim
committed
Fix scripts
1 parent 8b67c36 commit e3f64d9

File tree

2 files changed

+67
-34
lines changed

2 files changed

+67
-34
lines changed

‎scripts/line_count/CompCertM-linking-tex.rb

+32-17
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,10 @@ def print_result(result)
1515
puts
1616

1717
UNREADGLOBPROOFS=["UnreadglobproofC"]
18-
UNREADGLOBPROOFS
18+
19+
MUTRECPROOFS=["MutrecAproof", "MutrecBproof", "MutrecABproof"]
20+
21+
UTODPROOFS=["DemoSpecProof"]
1922

2023
PASS_PROOFS=["cfrontend/Cstrategyproof", "cfrontend/SimplExprproof", "cfrontend/SimplLocalsproof", "cfrontend/Cshmgenproof", "cfrontend/Cminorgenproof",
2124
"backend/Selectionproof", "backend/RTLgenproof", "backend/Tailcallproof", "backend/Inliningproof", "backend/Renumberproof", "backend/Constpropproof",
@@ -24,7 +27,17 @@ def print_result(result)
2427

2528
PASS_PROOFS.map!{|i| i + "C.v"}
2629

27-
loc=`find . ! -path '*demo/*' -name '*.v' ! -name 'UpperBound_AExtra.v' ! -name 'UpperBound_A.v' ! -name 'UpperBound_B.v' | xargs coqwc`.split("\n")[-1].split(" ")
30+
UPPERBOUNDS=["UpperBound_AExtra", "UpperBound_A", "UpperBound_B"]
31+
32+
INTERACTIONS=["SemProps", "ModSemProps"]
33+
34+
LANGUAGE=["cfrontend/CsemC", "cfrontend/CstrategyC", "cfrontend/ClightC", "cfrontend/CsharpminorC",
35+
"backend/CminorC", "backend/CminorSelC", "backend/RTLC", "backend/LTLC", "backend/LinearC",
36+
"backend/MachC", "backend/MachExtra", "x86/AsmC", "x86/AsmExtra"]
37+
38+
LOWERBOUNDS=["LinkingC2", "LowerBoundExtra", "LowerBound"]
39+
40+
loc=`find . ! -path '*demo/*' #{UPPERBOUNDS.inject(""){|sum, i| sum + "! -name \'" + i + ".v\' "}} -name '*.v' | xargs coqwc`.split("\n")[-1].split(" ")
2841
loc=loc[0].to_i + loc[1].to_i
2942
tex3=tex3 + loc.to_s + "(+" + (((loc/119993.0)*100).round(2)).to_s + "\\\%) & 2102 & "
3043

@@ -45,7 +58,7 @@ def print_result(result)
4558
puts
4659
puts "<<Unreadglob-rest>>"
4760
puts
48-
temp=print_result(`find demo/mutrec #{UNREADGLOBPROOFS.inject(""){|sum, i| sum + "! -name \'" + i + ".v\' "}} -name '*.v' | xargs coqwc`)
61+
temp=print_result(`find demo/unreadglob #{UNREADGLOBPROOFS.inject(""){|sum, i| sum + "! -name \'" + i + ".v\' "}} -name '*.v' | xargs coqwc`)
4962
tex2=tex2 + temp.to_s + " & "
5063

5164
puts
@@ -54,8 +67,6 @@ def print_result(result)
5467
temp=print_result(`coqwc demo/unreadglob/*.v`)
5568
tex3=tex3 + temp.to_s + " & "
5669

57-
MUTRECPROOFS=["MutrecAproof", "MutrecBproof", "MutrecABproof"]
58-
5970
puts
6071
puts "<<Mutrec-PASS PROOF>>"
6172
puts
@@ -74,8 +85,6 @@ def print_result(result)
7485
temp=print_result(`coqwc demo/mutrec/*.v`)
7586
tex3=tex3 + temp.to_s + " & "
7687

77-
UTODPROOFS=["DemoSpecProof"]
78-
7988
puts
8089
puts "<<Utod-PASS PROOF>>"
8190
puts
@@ -97,23 +106,22 @@ def print_result(result)
97106
puts
98107
puts "<<Adq. w.r.t. C>>"
99108
puts
100-
temp=print_result(`coqwc bound/UpperBound_AExtra.v bound/UpperBound_A.v bound/UpperBound_B.v`)
109+
temp=print_result(`coqwc #{UPPERBOUNDS.map{|i| "bound/" + i + ".v"}.join(" ")}`)
101110
tex3=tex3 + temp.to_s + " \\\\ "
102111

103112
breakdown = "Interaction Semantics & "
104113
puts
105114
puts "<<Interation Semantics>>"
106115
puts
107-
temp=print_result(`coqwc compose/*.v`)
116+
temp=print_result(`coqwc compose/*.v #{INTERACTIONS.map{|i| "proof/" + i + ".v"}.join(" ")}`)
108117
loc=loc-temp
109118
breakdown = breakdown + temp.to_s + " \\\\ \n"
110119

111120
breakdown = breakdown + "Language Semantics & "
112121
puts
113122
puts "<<Language Semantics>>"
114123
puts
115-
temp=print_result(`coqwc cfrontend/CsemC.v cfrontend/CstrategyC.v cfrontend/ClightC.v cfrontend/CsharpminorC.v \
116-
backend/CminorC.v backend/CminorSelC.v backend/RTLC.v backend/LTLC.v backend/LinearC.v backend/MachC.v x86/AsmC.v`)
124+
temp=print_result(`coqwc #{LANGUAGE.map{|i| i + ".v"}.join(" ")}`)
117125
loc=loc-temp
118126
breakdown = breakdown + temp.to_s + " \\\\ \n"
119127

@@ -125,16 +133,22 @@ def print_result(result)
125133
loc=loc-temp
126134
breakdown = breakdown + temp.to_s + " \\\\ \n"
127135

128-
breakdown = breakdown + "CompCert Meta & FILL_THIS \\\\ \n"
136+
137+
breakdown = breakdown + "CompCert Meta & "
129138
puts
130-
puts "<<CompCert Meta: the Rest>>"
139+
puts "<<CompCert Meta>>"
131140
puts
141+
temp=print_result(`find . ! -path '*demo/*' ! -path '*compose/*' ! -path '*proof/*' ! -path '*bound/*' ! -path '*selfsim/*' -name '*.v' \
142+
#{PASS_PROOFS.inject(""){|sum, i| sum + "! -wholename \'\*" + i + "\' "}} #{INTERACTIONS.inject(""){|sum, i| sum + "! -name \'" + i + ".v\' "}} \
143+
#{LANGUAGE.inject(""){|sum, i| sum + "! -wholename \'\*" + i + ".v\' "}} #{LOWERBOUNDS.inject(""){|sum, i| sum + "! -name \'" + i + ".v\' "}} | xargs coqwc`)
144+
loc=loc-temp
145+
breakdown = breakdown + temp.to_s + " \\\\ \n"
132146

133147
breakdown = breakdown + "CompCertM Meta & "
134148
puts
135149
puts "<<CompCertM meta>>"
136150
puts
137-
temp=print_result(`find proof -name '*.v' ! -name 'Simulation.v' | xargs coqwc`)
151+
temp=print_result(`find proof -name '*.v' ! -name 'Simulation.v' ! -name 'SemProps.v' ! -name 'ModSemProps.v' | xargs coqwc`)
138152
loc=loc-temp
139153
breakdown = breakdown + temp.to_s + " \\\\ \n"
140154

@@ -150,16 +164,15 @@ def print_result(result)
150164
puts
151165
puts "<<Adq. w.r.t. Asm>>"
152166
puts
153-
temp=print_result(`coqwc bound/LinkingC2.v bound/LowerBoundExtra.v bound/LowerBound.v`)
167+
temp=print_result(`coqwc #{LOWERBOUNDS.map{|i| "bound/" + i + ".v"}.join(" ")}`)
154168
loc=loc-temp
155169
breakdown = breakdown + temp.to_s + " \\\\ \n"
156170

157171
puts
158172
puts "<<WHOLE>>"
159173
puts
160-
print_result(`find . ! -path '*demo/*' -name '*.v' ! -name 'UpperBound_AExtra.v' ! -name 'UpperBound_A.v' ! -name 'UpperBound_B.v' | xargs coqwc`)
174+
print_result(`find . ! -path '*demo/*' #{UPPERBOUNDS.inject(""){|sum, i| sum + "! -name \'" + i + ".v\' "}} -name '*.v' | xargs coqwc`)
161175

162-
breakdown.sub! 'FILL_THIS', loc.to_s
163176
puts "----------------------"
164177
print tex1
165178
puts
@@ -169,4 +182,6 @@ def print_result(result)
169182
puts
170183
puts "----------------------"
171184
print breakdown
185+
puts
186+
puts "CHECKING: #{loc} must be 0"
172187

‎scripts/line_count/CompCertM-linking.rb

+35-17
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,10 @@ def print_result(result)
1111
puts
1212

1313
UNREADGLOBPROOFS=["UnreadglobproofC"]
14-
UNREADGLOBPROOFS
14+
15+
MUTRECPROOFS=["MutrecAproof", "MutrecBproof", "MutrecABproof"]
16+
17+
UTODPROOFS=["DemoSpecProof"]
1518

1619
PASS_PROOFS=["cfrontend/Cstrategyproof", "cfrontend/SimplExprproof", "cfrontend/SimplLocalsproof", "cfrontend/Cshmgenproof", "cfrontend/Cminorgenproof",
1720
"backend/Selectionproof", "backend/RTLgenproof", "backend/Tailcallproof", "backend/Inliningproof", "backend/Renumberproof", "backend/Constpropproof",
@@ -20,10 +23,23 @@ def print_result(result)
2023

2124
PASS_PROOFS.map!{|i| i + "C.v"}
2225

26+
UPPERBOUNDS=["UpperBound_AExtra", "UpperBound_A", "UpperBound_B"]
27+
28+
INTERACTIONS=["SemProps", "ModSemProps"]
29+
30+
LANGUAGE=["cfrontend/CsemC", "cfrontend/CstrategyC", "cfrontend/ClightC", "cfrontend/CsharpminorC",
31+
"backend/CminorC", "backend/CminorSelC", "backend/RTLC", "backend/LTLC", "backend/LinearC",
32+
"backend/MachC", "backend/MachExtra", "x86/AsmC", "x86/AsmExtra"]
33+
34+
LOWERBOUNDS=["LinkingC2", "LowerBoundExtra", "LowerBound"]
35+
36+
loc=`find . ! -path '*demo/*' #{UPPERBOUNDS.inject(""){|sum, i| sum + "! -name \'" + i + ".v\' "}} -name '*.v' | xargs coqwc`.split("\n")[-1].split(" ")
37+
loc=loc[0].to_i + loc[1].to_i
38+
2339
puts
2440
puts "<<<PASS_PROOFS>>>"
2541
puts
26-
print_result(`coqwc #{PASS_PROOFS.join(" ")}`)
42+
loc=loc-print_result(`coqwc #{PASS_PROOFS.join(" ")}`)
2743

2844
puts
2945
puts "<<Unreadglob-PASS PROOF>>"
@@ -33,15 +49,13 @@ def print_result(result)
3349
puts
3450
puts "<<Unreadglob-rest>>"
3551
puts
36-
print_result(`find demo/mutrec #{UNREADGLOBPROOFS.inject(""){|sum, i| sum + "! -name \'" + i + ".v\' "}} -name '*.v' | xargs coqwc`)
52+
print_result(`find demo/unreadglob #{UNREADGLOBPROOFS.inject(""){|sum, i| sum + "! -name \'" + i + ".v\' "}} -name '*.v' | xargs coqwc`)
3753

3854
puts
3955
puts "<<Unreadglob-whole>>"
4056
puts
4157
print_result(`coqwc demo/unreadglob/*.v`)
4258

43-
MUTRECPROOFS=["MutrecAproof", "MutrecBproof", "MutrecABproof"]
44-
4559
puts
4660
puts "<<Mutrec-PASS PROOF>>"
4761
puts
@@ -57,8 +71,6 @@ def print_result(result)
5771
puts
5872
print_result(`coqwc demo/mutrec/*.v`)
5973

60-
UTODPROOFS=["DemoSpecProof"]
61-
6274
puts
6375
puts "<<Utod-PASS PROOF>>"
6476
puts
@@ -77,44 +89,50 @@ def print_result(result)
7789
puts
7890
puts "<<Adq. w.r.t. C>>"
7991
puts
80-
print_result(`coqwc bound/UpperBound_AExtra.v bound/UpperBound_A.v bound/UpperBound_B.v`)
92+
print_result(`coqwc #{UPPERBOUNDS.map{|i| "bound/" + i + ".v"}.join(" ")}`)
8193

8294
puts
8395
puts "<<Interation Semantics>>"
8496
puts
85-
print_result(`coqwc compose/*.v`)
97+
loc=loc-print_result(`coqwc compose/*.v #{INTERACTIONS.map{|i| "proof/" + i + ".v"}.join(" ")}`)
8698

8799
puts
88100
puts "<<Language Semantics>>"
89101
puts
90-
print_result(`coqwc cfrontend/CsemC.v cfrontend/CstrategyC.v cfrontend/ClightC.v cfrontend/CsharpminorC.v \
91-
backend/CminorC.v backend/CminorSelC.v backend/RTLC.v backend/LTLC.v backend/LinearC.v backend/MachC.v x86/AsmC.v`)
102+
loc=loc-print_result(`coqwc #{LANGUAGE.map{|i| i + ".v"}.join(" ")}`)
92103

93104
puts
94105
puts "<<Self Simulation>>"
95106
puts
96-
print_result(`coqwc selfsim/*.v`)
107+
loc=loc-print_result(`coqwc selfsim/*.v`)
108+
97109

98110
puts
99-
puts "<<CompCert Meta: the Rest>>"
111+
puts "<<CompCert Meta>>"
100112
puts
113+
loc=loc-print_result(`find . ! -path '*demo/*' ! -path '*compose/*' ! -path '*proof/*' ! -path '*bound/*' ! -path '*selfsim/*' -name '*.v' \
114+
#{PASS_PROOFS.inject(""){|sum, i| sum + "! -wholename \'\*" + i + "\' "}} #{INTERACTIONS.inject(""){|sum, i| sum + "! -name \'" + i + ".v\' "}} \
115+
#{LANGUAGE.inject(""){|sum, i| sum + "! -wholename \'\*" + i + ".v\' "}} #{LOWERBOUNDS.inject(""){|sum, i| sum + "! -name \'" + i + ".v\' "}} | xargs coqwc`)
101116

102117
puts
103118
puts "<<CompCertM meta>>"
104119
puts
105-
print_result(`find proof -name '*.v' ! -name 'Simulation.v' | xargs coqwc`)
120+
loc=loc-print_result(`find proof -name '*.v' ! -name 'Simulation.v' ! -name 'SemProps.v' ! -name 'ModSemProps.v' | xargs coqwc`)
106121

107122
puts
108123
puts "<<Mixed Simulation>>"
109124
puts
110-
print_result(`coqwc proof/Simulation.v`)
125+
loc=loc-print_result(`coqwc proof/Simulation.v`)
111126

112127
puts
113128
puts "<<Adq. w.r.t. Asm>>"
114129
puts
115-
print_result(`coqwc bound/LinkingC2.v bound/LowerBoundExtra.v bound/LowerBound.v`)
130+
loc=loc-print_result(`coqwc #{LOWERBOUNDS.map{|i| "bound/" + i + ".v"}.join(" ")}`)
116131

117132
puts
118133
puts "<<WHOLE>>"
119134
puts
120-
print_result(`find . ! -path '*demo/*' -name '*.v' ! -name 'UpperBound_AExtra.v' ! -name 'UpperBound_A.v' ! -name 'UpperBound_B.v' | xargs coqwc`)
135+
print_result(`find . ! -path '*demo/*' #{UPPERBOUNDS.inject(""){|sum, i| sum + "! -name \'" + i + ".v\' "}} -name '*.v' | xargs coqwc`)
136+
137+
puts
138+
puts "Check #{loc} must be 0"

0 commit comments

Comments
 (0)