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

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.


I believe you meant libxmhfdebug? I was able to add it as a uobj and build the image with gcc. One caveat though is that some functions from libgcc aren’t getting linked for some reason (even though I see libgcc.a in the bridge manifest). This led to an error in the debug library since there is a modulo and division operation on unsigned long long and int, leading to undefined reference to '__umoddi3' and '__udivdi3' (https://stackoverflow.com/questions/34532528/undefined-reference-to-divdi3).

I was able to work around it by using the do_div macro from the linux kernel (https://elixir.bootlin.com/linux/latest/source/arch/x86/include/asm/div64.h#L9) but it’s probably better to figure out why the functions aren’t getting linked or maybe just cast the types?

Fixing that might be unnecessary since I’m trying to switch to compcert now, but I’m running into a couple of errors.
First, compcert doesn’t seem to like blank initializers for structs (i.e. struct = {}), so it would throw an error when compiling the uobj_intrauobjcoll_callees_info.c and related files since I’m not defining any intrauobjcoll-callees in the manifest. I managed to work around this by commenting out the parts of the uberspark frontend lib that generated that info but maybe there is a better way around this?

After this workaround, everything proceeds normally to the linking step, where I encounter this error:
uberspark >> [docker] (.text+0xa7e): undefined reference to '__compcert_va_int32'. I couldn’t find any information on what this means. Any advice? I’ve attached the build log below:
build.log (312.1 KB)


Fantastic! Yes, I meant libxmhfdebug :slight_smile:

I isolated this to an issue within the current gcc cc-bridge manifest. We need to specify libgcc.a from the 32-bit folder.

Isolated this to current compcert cc-bridge not including libcompcert.a

Will need to revise frontend lib to generate this file with initializers so its compatible across compilers.

Ok this is what I recommend:

  1. I am going to merge this PR: überSpark: Add x86_32 CASM bridge and support for compiling CASM source files since it seems like the CASM extractor is working fine now

  2. I will create a new task to fix the aforementioned issues and report back here when I have something ready for you to test…

Thanks @yeeb!