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,
hol4.sml
Description: application/smil
------------------------------------------------------------------------------ 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
