Email Gateway (Jan 15 2024 at 22:32): Email Gateway (Jan 15 2024 at 22:32):From: "Daniel v. Kirschten" <daniel.kirschten@tum.de>
Hi all,
I found a situation where Isabelle reports a segmentation fault, and I was
told that this mailing list is the correct place to report this.
I'm using Isabelle 2023 on a x64 Windows 11 machine, and the segmentation
fault occurs in an instance of veriT spawned by the "try" command. Below is a
MWE demonstrating this - it already contains the offending "try" (line 43).
(There doesn't seem to be a way to attach files on this mailing list, that's
why I inlcuded it in this message's body - sorry.)
The concrete error message appears in the output windows, and on my machine,
it is as follows (note that I replaced my username with "xyz"):
/cygdrive/c/Users/xyz/AppData/Local/Temp/isabelle/
bash_script15875907052655868959: Zeile 4: 675 Segmentation fault /cygdrive/
e/Programme/Programmierung/Isabelle/Isabelle2023/contrib/verit-2021.06.2-rmx/
x86_64-windows/veriT --proof-with-sharing --proof-define-skolems --proof-prune
--proof-merge --disable-print-success --disable-banner --index-sorts --index-
fresh-sorts --triggers-new --triggers-sel-rm-specific --max-time\=7500 C:\
\Users\\xyz\\AppData\\Local\\Temp\\isabelle\\process3811362632330976021\
\cache-io-5406120 > /cygdrive/c/Users/xyz/AppData/Local/Temp/isabelle/
process3811362632330976021/cache-io-5406122 2>&1
Steps to reproduce:
Move the cursor to the "try" in line 43 and wait for all background
theories to finish.
Wait for the "try" to finish. Observe the the segmentation fault message in
the Output view (note that cvc4 even finds some proof).
Is there any additional info you need? Is this a known problem? If this
mailing list isn't the correct place to report this, where else should I
report this, if at all?
Kind regards,
Daniel v. Kirschten
PS: At least for me, this doesn't have any priority. I stumbled upon this
while doing some homework which I have solved by now regardless. Also, I
actually found several instances of such a segfault during this homework, but
I only extracted a MWE for the first of them.
theory Segfault
imports "HOL-IMP.Big_Step" "HOL-Library.Extended_Nat"
begin
inductive
big_step_t :: "com \<times> state \<Rightarrow> nat \<Rightarrow> state
\<Rightarrow> bool" ("_ \<Rightarrow>^/_ _" 55)
where
Skip: "(SKIP, s) \<Rightarrow>^1 s" |
Assign: "(x ::= a,s) \<Rightarrow>^1 s(x := aval a s)" |
Seq: "\<lbrakk> (c\<^sub>1,s\<^sub>1) \<Rightarrow>^n\<^sub>1 s\<^sub>2; (c
\<^sub>2,s\<^sub>2) \<Rightarrow>^n\<^sub>2 s\<^sub>3; n\<^sub>1+n\<^sub>2 = n
\<^sub>3 \<rbrakk> \<Longrightarrow> (c\<^sub>1;;c\<^sub>2, s\<^sub>1)
\<Rightarrow>^n\<^sub>3 s\<^sub>3" |
IfTrue: "\<lbrakk> bval b s; (c\<^sub>1,s) \<Rightarrow>^n\<^sub>1 t; n
\<^sub>3 = Suc n\<^sub>1 \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE
c\<^sub>2, s) \<Rightarrow>^n\<^sub>3 t" |
IfFalse: "\<lbrakk> \<not>bval b s; (c\<^sub>2,s) \<Rightarrow>^n\<^sub>2 t;
n\<^sub>3 = Suc n\<^sub>2 \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1
ELSE c\<^sub>2, s) \<Rightarrow>^n\<^sub>3 t" |
WhileFalse: "\<lbrakk> \<not>bval b s \<rbrakk> \<Longrightarrow> (WHILE b DO
c, s) \<Rightarrow>^1 s" |
WhileTrue:
"\<lbrakk> bval b s\<^sub>1; (c,s\<^sub>1) \<Rightarrow>^n\<^sub>1 s\<^sub>2;
(WHILE b DO c, s\<^sub>2) \<Rightarrow>^n\<^sub>2 s\<^sub>3; n\<^sub>1+n
\<^sub>2+1 = n\<^sub>3 \<rbrakk>
\<Longrightarrow> (WHILE b DO c, s\<^sub>1) \<Rightarrow>^n\<^sub>3 s
\<^sub>3"
inductive_cases If_tE[elim!]: "(IF b THEN c\<^sub>1 ELSE c\<^sub>2,s)
\<Rightarrow>^x t"
type_synonym qassn = "state \<Rightarrow> enat"
fun emb :: "bool \<Rightarrow> enat" ("\<down>") where
"emb False = \<infinity>"
| "emb True = 0"
definition hoare_Qvalid :: "qassn \<Rightarrow> com \<Rightarrow> qassn
\<Rightarrow> bool"
("\<Turnstile>\<^sub>Q {(1_)}/ (_)/ {(1_)}" 50) where
"\<Turnstile>\<^sub>Q {P} c {Q} \<longleftrightarrow> (\<forall>s. P s <
\<infinity> \<longrightarrow> (\<exists>t p. ((c,s) \<Rightarrow>^p t) \<and>
P s \<ge> p + Q t))"
theorem If_sound:
assumes "\<Turnstile>\<^sub>Q {\<lambda>a. P a + \<down> (bval b a)} c
\<^sub>1 {Q}"
and " \<Turnstile>\<^sub>Q {\<lambda>a. P a + \<down> (\<not> bval b a)}
c\<^sub>2 {Q}"
shows "\<Turnstile>\<^sub>Q {\<lambda>a. eSuc (P a)} IF b THEN c\<^sub>1
ELSE c\<^sub>2 {Q}"
unfolding hoare_Qvalid_def proof(safe)
fix s
assume "eSuc (P s) < \<infinity>"
then have Ps_fin: "P s < \<infinity>" by (metis eSuc_infinity eSuc_mono)
show "\<exists>t p. ((IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow>^p
t) \<and> enat p + Q t \<le> eSuc (P s)"
proof(cases "bval b s")
case True
have "P s + \<down>(bval b s) < \<infinity> \<longrightarrow> (\<exists>t
p. ((c\<^sub>1, s) \<Rightarrow>^p t) \<and> enat p + Q t \<le> P s +
\<down>(bval b s))"
using assms(1) unfolding hoare_Qvalid_def by simp
then obtain t p where "(c\<^sub>1, s) \<Rightarrow>^p t" and "enat p + Q t
\<le> eSuc (P s)" using True Ps_fin try sorry
then show ?thesis sorry
next
case False
then show ?thesis sorry
qed
qed
end
Email Gateway (Jan 15 2024 at 22:32):From: Daniel von Kirschten <daniel.kirschten@tum.de>
Hi all,
I found a situation where Isabelle reports a segmentation fault, and I
was told that this mailing list is the correct place to report this.
I'm using Isabelle 2023 on a x64 Windows 11 machine, and the
segmentation fault occurs in an instance of veriT spawned by the "try"
command. Please find attached a MWE demonstrating this - it already
contains the offending "try" (line 43).
The concrete error message appears in the output windows, and on my
machine, it is as follows (note that I replaced my username with "xyz"):
/cygdrive/c/Users/xyz/AppData/Local/Temp/isabelle/bash_script15875907052655868959:
Zeile 4: 675 Segmentation fault
/cygdrive/e/Programme/Programmierung/Isabelle/Isabelle2023/contrib/verit-2021.06.2-rmx/x86_64-windows/veriT
--proof-with-sharing --proof-define-skolems --proof-prune --proof-merge
--disable-print-success --disable-banner --index-sorts
--index-fresh-sorts --triggers-new --triggers-sel-rm-specific
--max-time\=7500
C:\\Users\\xyz\\AppData\\Local\\Temp\\isabelle\\process3811362632330976021\\cache-io-5406120/cygdrive/c/Users/xyz/AppData/Local/Temp/isabelle/process3811362632330976021/cache-io-5406122
2>&1
Steps to reproduce:
- Open Isabelle 2023.
- Open Segfault.thy in Isabelle.
- Move the cursor to the "try" in line 43 and wait for all background
theories to finish.
- Wait for the "try" to finish. Observe the the segmentation fault
message in the Output view (note that cvc4 even finds some proof).
Is there any additional info you need? Is this a known problem? If this
mailing list isn't the correct place to report this, where else should I
report this, if at all?
Kind regards,
Daniel v. Kirschten
PC: At least for me, this doesn't have any priority. I stumbled upon
this while doing some homework which I have solved by now regardless.
Also, I actually found several instances of such a segfault during this
homework, but I only extracted a MWE for the first of them.
Email Gateway (Jan 16 2024 at 08:37):From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
Dear Daniel,
Thanks for your report. I will send it to veriT's main developer, Pascal Fontaine, but since veriT is no longer the focus of his research (he's working on a new SMT solver), I suspect he might decide not to prioritize this.
Best,
Jasmin
Last updated: Apr 29 2024 at 01:08 UTC