Re: [isabelle] Simpl References Reasoning



Thank you Holger.  I will certainly have look at your extensions.
Cheers,
George

On Mon, Apr 28, 2014, at 02:50 AM, Holger Gast wrote:
> 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)
> 
> 
> On 04/24/2014 05:50 PM, George K. wrote:
> > 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.
> > 
> 




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.