Re: [Why3-club] Low level constructs

[Claude Marché]

Le 15/08/2016 à 21:01, Jean-Christophe Filliatre a écrit :
> The ARM paper mentioned by Per builds upon an older paper of mine where
> the verification of assembly programs is considered. You can find it
> here: http://www.lri.fr/~filliatr/publis/verifmix.pdf
> This handles arbitrary control flows, provided any loop in the CFG
> contains at least an invariant.

Just to add my 2 cents: the same idea for handling arbitrary control
flow is reused in the following thesis (Section 9.5 in particular)

https://tel.archives-ouvertes.fr/tel-00710193

to deal with x86 assembly code.

- Claude

-- 
Claude Marché  | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France   |
Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex|
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/mailman/listinfo/why3-club

Re: [Why3-club] Low level constructs

[Jean-Christophe Filliatre]

Hi Neil,

There are no gotos in WhyML, as already mentioned by Per.

But WhyML supports exceptions and some gotos (typically forward gotos)
can be translated to exceptions (with a "raise" at the goto place and a
suitable "try with" to handle it at the goto label place).

Of course, if you are interested in the full power of gotos, this is a
different matter.

The ARM paper mentioned by Per builds upon an older paper of mine where
the verification of assembly programs is considered. You can find it
here: http://www.lri.fr/~filliatr/publis/verifmix.pdf
This handles arbitrary control flows, provided any loop in the CFG
contains at least an invariant.

Best regards,
--
Jean-Christophe


On 15/08/2016 17:07, Neil Evans wrote:
> Hello,
> 
> I'm trying to do a comparison between Why3 and MALPAS, specifically
> WhyML and the MALPAS Intermediate Language (MALPAS IL). (Knowledge of
> MALPAS is not important for answering my query but I thought I'd mention
> it just in case.)
> 
> I would like to know to what extent WhyML can represent low-level
> language constructs such as GOTOs (unconditional jumps to labels) and
> updates to non-local variables (to model side effects). I've looked at
> the manual/tutorial but it's not immediately apparent if these sorts of
> thing are possible or not. These features are available in MALPAS IL but
> it is now old technology and I'm seeking alternative tools to model
> instruction sets and assembly code for formal analysis.
> 
> Thanks,
> 
> Neil.
> 
> 
> ___
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/why3-club
> 
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/mailman/listinfo/why3-club

Re: [Why3-club] Low level constructs

[Per Lindgren]

Hi Neil

On 15 Aug 2016, at 17:07, Neil Evans 
mailto:n.ev...@zepler.net>> wrote:

Hello,

I'm trying to do a comparison between Why3 and MALPAS, specifically WhyML and 
the MALPAS Intermediate Language (MALPAS IL). (Knowledge of MALPAS is not 
important for answering my query but I thought I'd mention it just in case.)

I would like to know to what extent WhyML can represent low-level language 
constructs such as GOTOs (unconditional jumps to labels) and updates to 
non-local variables (to model side effects). I've looked at the manual/tutorial 
but it's not immediately apparent if these sorts of thing are possible or not. 
These features are available in MALPAS IL but it is now old technology and I'm 
seeking alternative tools to model instruction sets and assembly code for 
formal analysis.

To my knowledge you cannot model GOTO in the native WhyML language.

Global variables (per module) can be modelled and used by functions with side 
effects (“writes” and “reads”).

You may have a look at toccata (http://toccata.lri.fr) there you find a large 
number of verification examples.

When it comes to modelling other languages/instruction sets in why3, you can 
have a look at “wp_revisited” 
(http://toccata.lri.fr/gallery/WP_revisited.en.html) and “double_wp” 
(http://toccata.lri.fr/gallery/double_wp.en.html), both encode operational 
semantics and Hoare logic. While wp_revisted has a focus on generating VCs from 
assertions in the input language, double_wp encodes wps to verify the 
correctness of a “toy” compiler. Both models a “classic” imp language with 
assignments conditionals and (while) loops.

An encoding of the ARM instruction set can be found at. 
http://inforum.org.pt/INForum2012/docs/20120013.pdf. However, quote  "As it can 
be noticed, branching instructions are not included in the grammar rules. This 
happens due to the fact that sequentialization mechanism removes those 
instructions from the code of sequential programs.” (I.e, the input program is 
unrolled (by an external tool) before put to analysis.)

If this is not what you are looking for, you may have a look at Bedrock 
(http://plv.csail.mit.edu/bedrock/) which is a more extensive “low level 
programming” framework in Coq. Another encoding of (simple) imperative language 
(and Hoare logic) in Coq is found in SF 
(https://www.cis.upenn.edu/~bcpierce/sf/current/index.html), a very good 
introduction to both Coq and program verification. Also 
(http://research.microsoft.com/en-us/um/people/nick/coqasm.pdf) shows an 
encoding of low level instruction (X86) set in Coq. There are probably loads 
more.

Best,
  Per



Thanks,

Neil.
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/mailman/listinfo/why3-club

___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/mailman/listinfo/why3-club