Dear Antony,
Thank you very much for this wonderful explanation! Is there any example of
such simplification inside the HOL4's ARM model?
Regards,Hamed
--- On Mon, 1/28/13, Anthony Fox <[email protected]> wrote:
From: Anthony Fox <[email protected]>
Subject: Re: [Hol-info] HOL4's ARM
model- Output Simplification.
To: "hamed nemati" <[email protected]>
Cc: "hol-info" <[email protected]>
Date: Monday, January 28, 2013, 2:15 PM
Hi Hamed,
I’m assuming that your example comes from using the tool
arm_random_testingLib.arm_step_updates.
If you wish to manipulate these terms then you can do so using HOL4’s
collection of syntax functions (e.g. see Term, boolSyntax and wordsSyntax).
These libraries can be used to destruct terms and to build new ones. For
example, you can get a list of bytes as follows:
> val l = HolKernel.strip_binop (Lib.total wordsSyntax.dest_word_concat) tm;
val l =
[``mem (r2 + 7w)``,
``mem (r2 + 6w)``,
``mem (r2 + 5w)``,
``mem (r2 + 4w)``]: term list
where tm is your original term. You can then build a term that is close to what
you’re after
as follows:
Term.mk_comb
(Term.mk_var ("mem", ``:word32 # 'a -> word32``),
pairSyntax.mk_pair
(boolSyntax.rand (List.last l),
Term.mk_var ("e_little", Type.alpha)));
val it = ``mem (r2 + 4w,e_little)``:
However, note that this is definitely not "proper simplification” because the
manipulations are not constrained by HOL’s logic. The manipulations are purely
syntactic and there is no proof going on at all.
If you wish to do simplifications (proofs) then
arm_random_testingLib.arm_step_updates is not the way to go; you should instead:
1. Use armLib.arm_step to give you a theorem.
2. Make definitions that correspond with BAP’s model, e.g. define a memory
operation with the right semantics.
3. Use forward proof (e.g. REWRITE_RULE and SIMP_RULE) to translate the
step-theorem into the required
form.
Regards,
Anthony
On 28 Jan 2013, at 12:40, hamed nemati <[email protected]> wrote:
>
> Dear developers,
>
> I am a student working on formal verification of a middle-ware. In this
> project as a part of this verification task, I have to convert the HOL4 step
> theorem's output to a simplified intermediate language which can be processed
> by another tool called BAP(http://bap.ece.cmu.edu/).
>
> I already implemented a prototype version of such a converter module, which
> is completely based on syntax analysis of the HOL4's output. Now, I am trying
> to adopt a new approach to introduce this converter into the HOL4 structure,
> but I do not know what is the best way to do this. I would appreciate if you
> could help me with this by providing a
guideline. As an example for instructions which deal with memory like (ldr
r1,[r2,#4]) , what the HOL4 model for ARM produces is as follows: (I attached
the code snippet producing the following output)
>
> ((mem :u32 -> u8) ((r2 :u32) + (7w :u32)) @@
> ((mem (r2 + (6w :u32)) @@
> ((mem (r2 + (5w :u32)) @@ mem (r2 + (4w :u32))) :word16))
> :word24))
>
> However the BAP's intermediate language syntax for this instruction is
>
> mem:?u32[(R2:u32 + 0x4:u32),e_little]:u32
>
> I was wondering if there is way to do this kind of simplification inside the
> HOL4. Many thanks in advance.
>
> Regards,
>
> ------------------------------------------------------------------------------
> Master Visual Studio, SharePoint, SQL, ASP.NET,
C# 2012, HTML5, CSS,
> MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current
> with LearnDevNow - 3,200 step-by-step video tutorials by Microsoft
> MVPs and experts. ON SALE this month only -- learn more at:
> http://p.sf.net/sfu/learnnow-d2d_______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Master Visual Studio, SharePoint, SQL, ASP.NET, C# 2012, HTML5, CSS,
MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current
with LearnDevNow - 3,200 step-by-step video tutorials by Microsoft
MVPs and experts. ON SALE this month only -- learn more at:
http://p.sf.net/sfu/learnnow-d2d
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
