Email Gateway (Aug 19 2022 at 14:11): Email Gateway (Aug 19 2022 at 14:11):From: "George K." <g_karab@encs.concordia.ca>
Hello all,
I have been using Schirmer's Simpl for the past couple of months now.
I am stuck when trying to reason with a procedure that deals with
references. In particular, I cannot discharge the procedure's
specification when the procedure calls other procedures that allocate
memory and set field values.
I am attaching a theory that illustrates the issues I have. This theory
contains:
1) A globals_memory hoarestate, containing a list of allocated
references and a free counter of available memory. Taken straight out
of the examples of the AFP SIMPL distro.
2) A globals_First hoarestate that declares a data structure that just
holds a single field of int type
3) A procedure First() that is, in essence, a constructor.
4) A globals_Second hoarestate which contain two fields each one being a
"ref => ref". The intent is to model a data structure that contains
references to other structures.
5) A Second_1 procedure that is a constructor accepting a two
references.
6) A Second_2 procedure that is also a constructor--however, we pass
integer values and invoke the First() procedure twice. It is this
procedure I cannot prove the functional specification.
The functional spec looks as follows:
lemma (in Second_2_impl) Second_2_spec:
"
∀σ x1 x2. Γ,Θ ⊢⇩t
⦃σ. ´x1 = x1 ∧ ´x2 = x2 ∧ (sz_Second + sz_First + sz_First) ≤
´free ⦄
´result' :== PROC Second_2(´x1,´x2)
⦃
´result' ≠ Null ∧ ´result'→´Y ≠ Null ∧ ´result'→´Z ≠ Null ∧
´free = ⇗σ⇖free - sz_Second - sz_First - sz_First ∧
´result'→´Z→´X = x2 ∧
´result'→´Y→´X = x1 ∧
´result' ∈ set ´alloc
⦄
"
The last two conjucts (i.e. ´result'→´Y→´X = x1 ∧ ´result' ∈ set ´alloc)
are giving me hard time. I believe the issues I have are related to
letting Isabelle know that the references allocated within the Second_2
procedure are distinct (at least this is what I understand when reading
on the split heap model used in Simpl). Unfortunately, I am not sure
how I can express this kind of distinctness in Isabelle.
Furthermore, I am unsure on whether I need to abstract simple data
structures (such as the one in the attached theory) in HOL, similarly to
the manner linked lists in the heap are abstracted to HOL lists using
the List predicate.
Any help is appreciated.
George.
SimplMemTester.thy
Email Gateway (Aug 19 2022 at 14:12):From: Thomas Sewell <thomas.sewell@nicta.com.au>
Hello George.
Indeed you need a lot of distinctness. The problem with this kind of
hoare level reasoning about heaps is that you need to establish not only
that the modified values are modified as expected, but that everything
else is unchanged.
I can fix your proof by extending First_spec as follows:
lemma (in First_impl) First_spec:
"
\<forall>\<sigma> x. \<Gamma>,\<Theta> \<turnstile>\<^sub>t
\<lbrace>\<sigma>. \<acute>x = x \<and> sz_First \<le>
\<acute>free \<rbrace>
\<acute>result' :== PROC First(\<acute>x)
\<lbrace> \<acute>result' \<noteq> Null \<and>
\<acute>result'\<rightarrow>\<acute>X = x \<and>
\<acute>result' \<in> set \<acute>alloc \<and>
\<acute>result' \<notin> set (\<^bsup>\<sigma>\<^esup>alloc)
\<and> set \<acute>alloc = insert \<acute>result' (set
(\<^bsup>\<sigma>\<^esup>alloc))
\<and> \<acute>free = \<^bsup>\<sigma>\<^esup>free - sz_First
\<and> (\<forall>x \<in> set
(\<^bsup>\<sigma>\<^esup>alloc). x\<rightarrow>\<acute>X =
x\<rightarrow>\<^bsup>\<sigma>\<^esup>X )\<rbrace>
"
(you might have to save that and load it in jEdit to read it).
I've additionally asserted that the allocated address was not previously
allocated, that the set of allocated addresses has grown by the one
allocated address, and that all values previously allocated are unchanged.
The current fashion is to avoid this tedious enumeration of everything
that stays the same by using some kind of separation logic. Perhaps you
should investigate whether Simpl provides something like that, or some
standard idiom for expressing what hasn't changed.
Good luck,
Thomas.
Email Gateway (Aug 19 2022 at 14:12):From: Holger Gast <gast@informatik.uni-tuebingen.de>
Hello George,
Thomas mentions using separation logic in his reply.
As it happens, I have build the usual symbolic
execution approach on top of Simpl for a project [1].
The basic idea is to reconstruct the original execution
sequence of heap operations as much as necessary in the form
of nested let expressions, by considering the nesting
of the heap access expressions and various side-conditions.
The latest version of the implementation is available from
the homepage of last year's lecture on software verification:
https://www21.in.tum.de/teaching/isv/SS13
The file SimplC.zip also contains a (rudimentary)
C parser, translator to Simpl, the reconstruction
mentioned above, and symbolic execution/heap matching.
Hope this helps,
Holger
[1] Gast, H. "Semi-automatic proofs about object graphs in separation logic",
in: Merz, S. and Lüttgen, G.: Automated Verification of Critical Systems
(AVoCS '12)
Email Gateway (Aug 19 2022 at 14:13):From: "George K." <g_karab@encs.concordia.ca>
Thank you Thomas! Indeed this is tedious, but it does make sense. My
initial understanding was that specifying the frame condition would
suffice but I was wrong.
I will start tackling Separation Logic as soon as I can.
Cheers,
George
Email Gateway (Aug 19 2022 at 14:13):From: "George K." <g_karab@encs.concordia.ca>
Thank you Holger. I will certainly have look at your extensions.
Cheers,
George
Last updated: Nov 21 2024 at 12:39 UTC