Starting with S2E-ARM

[Thuan Pham]

I have been working with S2E on x86. Now, I want to work on ARM to target embedded systems.

I think someone in this group is working with ARM so I would like to get help from you. Could you share with me some tutorials/steps/information to start working with ARM like 1)Which Android version is used, 2)Which ARM core is used, 3)Running instructions that are ARM-specific...

Thanks a lot.

Thuan.

[Thuan Pham]

I have followed this link (https://github.com/surajx/qemu-arm-linux/wiki/Compile-Linux,-BusyBox-for-ARM-and-load-it-using-QEMU) to install successfully an embedded Linux for testing. I can boot up the system using the following command:
<path to arm-softmmu>/qemu-system-arm -M vexpress-a9 -m 256M -kernel linux-3.10/arch/arm/boot/zImage -initrd busybox-1.21.1/rootfs.img -append "root=/dev/ram rdinit=/sbin/init"
Now, I have some other questions
1. While testing Windows guest image, I can easily create a snapshot for the raw.s2e image. Could you let me know how to create a similar snapshot for an embedded linux image? In my case, the rootfs is just a compiled busybox in .img format.
2. I am trying to cross-compile a simple C program for testing. To do so, I include the s2e-arm.h to call s2e_make_concolic custom instruction but I face errors due to missing uint64_t data type definition
s2e-arm.h:316:43: error: unknown type name ‘uint64_t’
s2e-arm.h:317:43: error: unknown type name ‘uint64_t’
s2e-arm.h:318:43: error: unknown type name ‘uint64_t’
s2e-arm.h:319:43: error: unknown type name ‘uint64_t’
s2e-arm.h:450:59: error: unknown type name ‘uint64_t’
Could you give me some suggestion to fix the issue.

Thanks a lot.
Thuan.

[Thuan Pham]

For my first question, I think I cannot create the snapshot for the .img rootfs because it is loaded as an intial Ramdisk => not a block device. So, I may need to create a NAND flash to store my rootfs in order to create snapshot. Am I right?

For my second question, I have removed some functions that use uint64_t from s2e-arm.h. In addition, I have to copy two functions (__s2e_touch_string and __s2e_touch_buffer) from s2e.h to s2e-arm.h. Now, I can compile my test program successfully.

Now, I want to run s2e-arm in symbolic mode but I don't know how to write the LUA configuration file in this case. Could someone kindly share with me a very simple LUA file that you have used for ARM.

I have tried to create a very simple LUA file (as attached) and run with the following command but I cannot boot up the system properly.
/home/konst/Revgen/build/qemu-release/arm-s2e-softmmu/qemu-system-arm -M vexpress-a9 -m 256M -kernel zImage -initrd rootfs.img -append "root=/dev/ram rdinit=/sbin/init" -net none -s2e-config-file s2e.config.lua -s2e-verbose

Please find attached the s2e-last folder.
Thanks a lot.
Thuan.

[Thuan Pham]

FYI, I cannot run with the minimal LUA file

-- File: config.lua
s2e = {
  kleeArgs = {}
}

plugins = {
  -- Enable a plugin that handles S2E custom opcode
  "BaseInstructions"
}

The output messages is:

WARNING: Linking two modules of different data layouts!
Creating plugin CorePlugin
Creating plugin BaseInstructions
0 [State 0] Created initial state
oss: Could not initialize DAC
oss: Failed to open `/dev/dsp'
oss: Reason: No such file or directory
oss: Could not initialize DAC
oss: Failed to open `/dev/dsp'
oss: Reason: No such file or directory
audio: Failed to create voice `lm4549.out'
Initing initial device state.
WARNING!!! All writes to disk will be lost after shutdown.
qemu-system-arm: /home/konst/Revgen/s2e/qemu/s2e/S2EExecutionState.cpp:1349: void s2e::S2EExecutionState::writeRamConcrete(uint64_t, const uint8_t *, uint64_t): Assertion `op.first && op.first->isUserSpecified && op.first->address == page_addr && op.first->size == (1 << 7)' failed.
Aborted (core dumped)

[Vitaly Chipounov]

Hi,

You may want to follow the instructions on http://s3.eurecom.fr/tools/avatar/

Vitaly

--
--
You received this message because you are a member of the S2E Developer Forum.
To post to this group, send email to s2e...@googlegroups.com
To unsubscribe from this group, send email to s2e-dev+u...@googlegroups.com
For more options, visit this group at http://groups.google.com/group/s2e-dev

---
You received this message because you are subscribed to the Google Groups "S2E Developer Forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to s2e-dev+u...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[microp...@gmail.com]

Several years later, but I am hitting the same assertion error. Did you ever figure this out?

[microp...@gmail.com]

For anyone else who is curious, the vexpress -a9 armhf image doesn't work under S2E for some reason, failing on the assert in Thaun's message.

What you want are the ARMEL images here:
https://people.debian.org/~aurel32/qemu/armel/