Hi Norrathep,
Indeed, the AutoCorres quick-start tutorial assumes a certain degree of familiarity with Isabelle/HOL. To gain some familiarity, I would recommend working through at least the first few chapters of this book by Tobias Nipkow and Gerwin Klein:
http://www.concrete-semantics.org/
Although Isabelle/HOL can be run in batch mode to check proofs, it is primarily an interactive tool. AutoCorres, and also the C parser on which it builds, have not been designed to write specifications and proofs to files. Rather, specifications and proofs are constructed in the internal state of Isabelle/HOL, and the only realistic way to inspect these is in interactive mode.
For example, the following sequence of commands should give you an interactive session looking at the AutoCorres "plus" example:
# Check out l4v and its companion repositories. # Requires the Google `repo` tool. # See https://github.com/seL4/verification-manifest/blob/master/README.md for more details. $ mkdir verification $ cd verification $ repo init -u ssh://git@github.com/seL4/verification-manifest.git $ repo sync # Build some prerequisites. Requires the "MLton" Standard ML compiler, and possibly some other tools installed. $ cd l4v $ make -C tools/c-parser CParser $ make -C tools/autocorres AutoCorres tests/ROOT # Start an interactive session. # Ignore the warnings in the pop-up dialog. $ ./isabelle/bin/isabelle jedit -d . -l AutoCorres tools/autocorres/tests/examples/Plus.thy &
To see the specifications and definitions produced by the C parser and AutoCorres in the interactive session, make sure you have the "Output" pane open, and type the command "print_theorems" immediately after each of the "install_C_file" and "autocorres" commands, respectively.
Best regards, Matthew Brecknell
________________________________ From: Devel devel-bounces@sel4.systems on behalf of Norrathep Rattanavipanon nrattana@uci.edu Sent: Saturday, 20 July 2019 08:10 To: devel@sel4.systems devel@sel4.systems Subject: [seL4] Autocorres tutorial for Isabelle/HOL beginner
Hello,
I have been trying to study how seL4's C code is formally verified. So I looked into Autocorres tool and had a bit of hard time understanding how to use the tool to generate Isabelle definitions from C code. I tried to follow Autocorres' quickstart but I was confused since I do not know much about Isabelle/HOL.
I simply ran ``make AutoCorresTest" in l4v/tools/autocorres folder and it gave me this output:
``` Session Pure/Pure Session FOL/FOL Session HOL/HOL (main) Session HOL/HOL-Eisbach Session HOL/HOL-Library (main timing) Session HOL/HOL-Computational_Algebra (main timing) Session HOL/HOL-Algebra (main timing) Session HOL/HOL-Number_Theory (main timing) Session HOL/HOL-Statespace Session HOL/HOL-Word (main timing) Session Lib/Word_Lib (lib) Session Lib/Lib (lib) Session C-Parser/Simpl-VCG Session C-Parser/CParser Session Lib/CLib (lib) Session Unsorted/AutoCorres Session Unsorted/AutoCorresTest Building AutoCorresTest ... AutoCorresTest: theory AutoCorresTest.CustomWordAbs AutoCorresTest: theory AutoCorresTest.Test_Spec_Translation ... Finished AutoCorresTest (0:02:33 elapsed time, 0:08:14 cpu time, factor 3.23) ```
But I couldnt find any Isabelle definitions as output except "thy" files that contain:
``` theory somefile imports "AutoCorres.AutoCorres" begin
external_file "somefile.c"
install_C_file "somefile.c"
autocorres "somefile.c"
end ```
I suppose I need to invoke this file somehow using Isabelle in order to generate the definition but I'm not sure how to do that. Any help would be very appreciated.
Best Regards, Norrathep
-- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine