当前位置: 首页 > 工具软件 > seL4 > 使用案例 >

seL4 构建和测试

郭弘方
2023-12-01

转载至:https://source2014.hackpad.com/seL4--IJItb9IDncR

取得核心程式碼

    • mkdir -p seL4-test && cd seL4-test
    • repo sync

KZM-ARM11-01

  • ARM1136 532MHz (Freescale i.MX31) based evaluation board
  • 通过 QEMU 模拟和验证
    • make kzm_simulation_release_xml_defconfig
    • TOOLPREFIX=arm-none-eabi- ARCH=arm make
    • make simulate-kzm
參考執行輸出:
...
    <testcase classname="sel4test" name="TEST_IPC0001">
INFO :sel4utils_elf_load_record_regions:276:  * Loading segment 00008000-->000445e4
INFO :sel4utils_elf_load_record_regions:276:  * Loading segment 0004d000-->00165df8
        <system-out>  TEST_IPC0001
</system-out>
...
    <testcase classname="sel4test" name="TEST_CNODEOP00012">
INFO :sel4utils_elf_load_record_regions:276:  * Loading segment 00008000-->000445e4
INFO :sel4utils_elf_load_record_regions:276:  * Loading segment 0004d000-->00165df8
        <system-out>  TEST_CNODEOP0001
</system-out>
    </testcase>
</testsuite>

126/126 tests passed.
All is well in the universe.

這時候可以準備執行 pkill qemu-system-arm

seL4 Tests

  • BSD License
  • Directory
    • apps/sel4test-driver
    • apps/sel4test-tests

seL4 Verification

  • 取得原始程式碼
    • mkdir -p verification &&cd verification
    • repo sync
  • 準備相關套件
    • sudo apt-get install libwww-perl texlive-bibtex-extra texlive-latex-extra
    • sudo apt-get install python-lxml
    • sudo apt-get install mlton python-tempita
  • 由於 Isabelle 需要額外的套件如 jdk7, jfreechart, scala, xz-java,得自網路抓取
    • cd l4v
    • mkdir -p ~/.isabelle/etc
    • cp -i misc/etc/settings ~/.isabelle/etc/settings
    • ./isabelle/bin/isabelle components -a
  • 遇到以下的小錯誤,可繼續
    • dirname: 缺少運算元
    • Try 'dirname --help' for more information.
  • 這過程相當耗時,解決方式為預先將檔案置放於 ~/.isabelle/contrib/ 目錄
    • cvc3-2.4.1
    • e-1.8
    • exec_process-1.0.3
    • Haskabelle-2013
    • jdk-7u40
    • jedit_build-20131106
    • jfreechart-1.0.14-1
    • kodkodi-1.5.2
    • polyml-5.5.1-1
    • scala-2.10.3
    • spass-3.8ds
    • z3-3.2
    • xz-java-1.2-1
    • ProofGeneral-4.2
  • Automated theorem proving! 確保可用的記憶體 > 2 GB
    • ./isabelle/bin/isabelle jedit -bf
    • ./isabelle/bin/isabelle build -bv HOL-Word
  • 參考輸出
ML_PLATFORM="x86_64-linux"
ML_HOME="/home/jserv/.isabelle/contrib/polyml-5.5.1-1/x86_64-linux"
ML_SYSTEM="polyml-5.5.1"
ML_OPTIONS="-H 2000"

Session Pure/Pure
Session HOL/HOL (main)
Session HOL/HOL-Word (main)
Building Pure ...
Finished Pure (1:36:49 elapsed time, 0:00:51 cpu time, factor 0.00)
Building HOL ...
HOL: theory Code_Generator
HOL: theory HOL
HOL: theory SATz

  • 執行證明 (相當慢)
    • ./run_tests
參考輸出:
Running 31 test(s)...

  running isabelle ...              pass
  running CamkesAdlSpec ...         pass
  running CamkesGlueSpec ...        
  ...
  running CamkesAdlSpec ...          FAILED *
  running CamkesGlueSpec ...        FAILED *
所有的 Test  都是一定會過 ?
要安裝 mlton (已送 pull request)


Issues



 类似资料: