überXMHF (pc-intel-x86-32): Convert into a üobject collection with a single üobject task?

Marvelous. Thanks Ethan!

Ok, all the files for the uxmhf uobjcol compile successfully (using gcc v5.4.0)!

Currently running into the following linker error:
uberspark >> [docker] uobj.lscript:113 cannot move location counter backwards (from 000000006508ea88 to 00000000619fffff). Unsure of how to debug this. An initial google search says it has to do with a section running out of space.

I also commented out the slab_main from a couple of the uobjs. Since we’re combining them into a single uobj, the linker didn’t like the fact that it was defined multiple times. How necessary is slab_main with the next-gen toolkit? Is it safe to ignore for now?


Nice work @yeeb!

Can you post the uobj.lscript file? I might need to add a task to add capabilities to the nextgen toolchain to be able to specify section sizes within the configuration space.

It is important, but for now, you might just want to rename it as <uobjname>_slab_main where <uobjname> could be the name of the folder where the uobj resides (e.g., uapi_mempgtbl etc.)


uobj.lscript (4.6 KB)

Sounds good! My work so far is in my fork of the uberxmhf repo (x86-uberobjcol branch) btw.

Ok, I am going to be adding support for specifying section sizes (code, data, stack etc.) within the manifest as part of the following task: überSpark: Add cc-bridge compiler runtime library support, use crt üobjrtl by default in top-level header, and allow binary section specifications within uobj manifest

I will keep you posted…

Hi @yeeb,

Please pull from the PR (feature-ccbridge-cclib) corresponding to the discussion within this thread: überSpark: Add cc-bridge compiler runtime library support, use crt üobjrtl by default in top-level header, and allow binary section specifications within uobj manifest

The aforementioned PR adds a feature that allows you to specify sizes of uobject binary sections within the uobject manifest like below:

"uberspark-uobj" : {
  "sections": [
      "name" : "uobj_rwdata",
      "size" : "0x400000"

See docs/nextgen-toolkit/cossdev-guide/create-uobjs.rst for more information on how to specify sections and the uobject standard section names for code, data, stack etc.

Also note that the default section alignment is set to 0x200000 (2MB pages) and the specified sizes are rounded up to the section alignment.

You may also need to change the max. size of the uobj binary image to accommodate the new section sizes. This can be done via the following command:

uberspark staging config-set --setting-name=uobj_binary_image_size --setting-value=0x02C00000

The example above sets the max. binary image size to 0x02C00000 bytes (the default value is 0x02400000 bytes). The max. binary image size should be equal to or greater than all the LENGTH fields combined in the MEMORY section of uobj.lscript

Let me know if this helps.


Great, works well! I’m thinking that we should add some documentation about overriding the sizes for the default sections (i.e. uobj_code, uobj_tstack, etc.) since I spent some time trying to add new sections instead of specifying the sizes for those.

Currently encountering some undefined reference errors, I’ll try to debug and notify you of the progress.

Great! Please feel free to go ahead and add this documentation and commit to PR ( feature-ccbridge-cclib ) corresponding to the discussion within this thread: überSpark: Add cc-bridge compiler runtime library support, use crt üobjrtl by default in top-level header, and allow binary section specifications within uobj manifest

Hey @amitvasudevan, I think we’re ready to start integrating the CASM bridge.

Currently only running into linker “undefined reference” errors for the CASM functions. I am getting a fair amount of warnings from gcc but I think dealing with them is low priority for now (only these three types: Wint-conversion, Wincompatible-pointer-types, and Wpointer-to-int-cast).

Also, it looks like the CASM files in the hw uobjrtl get treated as normal .c files (i.e. added to the compile and linking commands). I’ve commented them out for now, how do you want to handle them?

I’ve attached the build log, let me know what you think the next steps are.
build.log (223.7 KB)

Great stuff @yeeb!

Agreed, lets put this on the back-burner for now

Hmm, I guess you can comment them out for the time-being, until the CASM bridge is in place…

We first need to merge the following two outstanding tooling related tasks:

  1. überSpark: Add cc-bridge compiler runtime library support, use crt üobjrtl by default in top-level header, and allow binary section specifications within uobj manifest
  2. überSpark: Add frama-c and uberspark verification bridge with uberspark verification bridge plugin infrastructure

I will ping back here once I have wrapped them up…


Hey @yeeb,

This is done and merged into develop

We now have support for building CASM source files! Please see the following task: überSpark: Add x86_32 CASM bridge and support for compiling CASM source files

Can you use the PR linked in the aforementioned task to see if you can make further progress for the uobjcoll build?


Awesome stuff!
I’ll resume work on the task and reply back when I’ve made some more progress.

Hey @amitvasudevan,
CASM extractor works well, except I’m running into an issue where CASM files that rely on #defined macros result in an undefined reference error during the linking step. I think having the C preprocessor run on the casm files will solve the issue (gcc -E) but I’m not sure where to add this.

I’ve attached the build log below:
build.log (804.5 KB)

I also ran into another undefined reference error with the xmhfgeec_slab_info_table. I believe it used to be defined through the old toolchain. I’ve commented out the files that use it for now, how should we proceed?


See src-nextgen/bridges/as-bridge/container/amd64/x86_32/generic/casm/vlatest/uberspark.json. You will need to modify the last line in the bridge_cmd JSON node to add this before running ccomp. However, I thought ccomp (compcert compiler) runs the pre-processor for us, so take a look and see…

We will need to add capabilities to the existing tool-chain to generate this table.

For now, look into target _uobjs_configureandgenerateuobjinfo within src/Makefile.in in the uberspark git repo. This is where we generate uobjinfotable.c which contains the xmhfgeec_slab_info_table variable definition. You can build regular uxmhf with the old tool-chain to generate this file and then copy it over to the uobjcoll folder and include it within the uobj manifest for the new tool-chain. Hope this makes sense.

Thanks @yeeb!

You might also want to check src-nextgen/hwm/include/arch/x86/generic/cpu.h to see which of those builtin_annots are responsible for not expanding the definitions. For example, within xcexhub_excpstub.cS there is a call to xmhfhwm_cpu_insn_movw_imm_ax(__DS_CPL0). However, I am not sure if _DS_CPL0 is getting expanded. The following might also be worth reading up on: https://gcc.gnu.org/onlinedocs/cpp/Argument-Prescan.html

Thanks for the link, apparently the errors were due to the fact that the builtin_annots stringized their arguments so the macro was never expanded. I managed to work around this by defining another macro #define MACRO_EXPANSION_WORKAROUND(func, ...) func(__VA_ARGS__) as recommended in the link above.

Currently working on the xmhfgeec_slab_info_table definition, but without those files everything finished building and I get a binary! I’ll update the thread once I work out the xmhfgeec_slab_info_table.

Ok, added a uobjinfotable.c that defines xmhfgeec_slab_info_table and everything builds to a binary image!

There’s still a few things that need fixing:

  • I missed renaming some function calls in hwm/include/device/net/ethernet/intel/e1000/e1000.h. I can submit a quick PR to update them.
  • I’m only using the geec_slabstubs_vft.cS file from the ported over xmhfgeec library to avoid multiple definition errors. Is this correct or is there a better way to do this?
  • How should we handle all the warnings (build.log (876.5 KB))? Mainly Wint-conversion, Wincompatible-pointer-types, and Wpointer-to-int-cast. I can explicitly cast them, though I’m not sure why these warnings don’t appear when building the old uberxmhf, I only renamed them.

I am still defining compile-time macros in xmhf-config.h, but that should be an easy fix once the following task completes and I don’t think it’s a priority at the moment.

Let me know what you think the next steps are. I can also work on migrating the debug library.


Fantastic news! Great job @yeeb!

Yeah, just go ahead and submit a PR.

Yes, this is good for the time being since all we are going to have for now is verified uobjs

Which version of the compcert bridge are you using? The easy way to do this is to perhaps ignore warning, but the right thing to do would be to cast them within the code. However, this can be something we can punt to a later stage.

Agreed. We can revisit this once the linked task is completed.

That will be very useful. I think we should introduce it as a uobjrtl (e.g., debug) which every uobj links to. Thoughts?

Thanks @amitvasudevan!

Will do.

Hmm I’ve actually been using the gcc 5.5.0 bridge. I’ll try to rebuild with compcert now and let you know how it goes.

I was thinking the same thing. I’ll get started on it this week. Should we move discussion to another task thread?

Ok. I just created the new task here: https://forums.uberspark.org/t/uberspark-add-debug-uobject-runtime-library/212

On further thought, for the time-being, I think we should bring libxmhfgeec from uberspark.git as a folder within the main uobj at uberxmhf.git/uxmhf/uobjcoll/.

Eventually, we should probably pare it away as a separate debug uobj that can be housed within src-nextgen/uobjs/debug namespace within uberspark.git.