search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
621 stars 140 forks source link

ex/mc/graph: RISC-V graph decompiler sfence.vma pseudo-function naming #840

Open mbrcknl opened 4 years ago

mbrcknl commented 4 years ago

This issue concerns the RISC-V version of the binary-to-graph decompiler in examples/machine-code/graph.

When decompiling the sfence.vma instruction, the decompiler generates a graph pseudo-function with a name similar to instruction'sfence_vma_8401157C. The underscore in sfence_vma confuses the graph-refine component of the seL4 binary correctness toolchain, since graph-refine parses the names of these pseudo-functions, treating underscore as a separator. Since the C graph uses names like asm_instruction'sfence.vma for its pseudo-functions, i.e. retaining the "." in sfence.vma, graph-refine fails to match the pseudo-function calls.

Would it be possible to retain the original name of the sfence.vma instruction (with period rather than an underscore) in the name of the pseudo-function generated by the decompiler?

mn200 commented 2 years ago

Does anyone involved here want to claim that this has been fixed, or not?