überSpark: add CASM bridge plugin support for C/HWM and Assembly output

This task will add the following capabilities to the existing CASM bridge plugin

  • Generate C code of th input .cS file with the CASM HWM implementation embedded.
  • Generate output Assembly code of the input .cS file with the output assembly instructions corresponding to the function(s) within the .cS input source file.

The following are the proposed sub-tasks:

  1. Add logic within Casmbridge_gensrc.casm_extract within tools/bridge-plugins/as-bridge/casmbridge_gensrc.ml to: parse the input AST, locate the CASM function definitions, and replace the corresponding CASM instructions within the CASM function definitions with their corresponding CASM/HWM implementation.

  2. The bridge plugin support function Uberspark.Context.get_hwm_manifest_var_cpu provides the CPU HWM manifest var which contains the field hwm.cpu.casm_instructions that is an association list of casm_mnemonic to the record of type json_node_uberspark_hwm_cpu_casm_instruction_t that is defined within tools/libs/uberspark__manifest.mli

  3. Once the AST is modified with the CASM/HWM implementation then write out the corresponding CASM functions into the output .c file that is specified by the output_file parameter to Casmbridge_gensrc.casm_extract.

  4. Add logic within Casmbridge_gensrc.casm_genc within tools/bridge-plugins/as-bridge/casmbridge_gensrc.ml to: parse the input AST, locate the CASM function definitions, and write the corresponding output assembly language instruction into the output .s file that is specified by the output_file parameter to Casmbridge_gensrc.casm_genc.

  5. For the step above, you will need to add a assembler function definition prologue for every CASM function defined. The prologue is as below:

     .section #casm_fn_section_name
     .balign #casm_fn_alignment
     .global #casm_fn_name
     #casm_fn_name:
    

    Where #casm_fn_name is the name of the CASM function. The output assembly instructions will follow this prologue for the corresponding CASM function. #casm_fn_section_name is obtained by parsing any __attribute__(section()) directive for the function definition. If that is absent the default value of .text is used for #casm_fn_section_name. Similarly, #casm_fn_alignment is obtained by parsing any __attribute__(aligned()) directive for the function definition. If that is absent the default value of 4 is used for #casm_fn_alignment. The attribute directives are part of the Cil function node.

Working branches:
TBD

PR(s):
TBD

Merge(s):
TBD

Below is a quick reference on function attributes:
https://gcc.gnu.org/onlinedocs/gcc/x86-Function-Attributes.html#x86-Function-Attributes

Hi @amitvasudevan ,
Is this line https://github.com/uberspark/uberspark/blob/d7ac95c7037e5bf235456315e94f2b74e8d174b1/src-nextgen/tools/bridge-plugins/as-bridge/casmbridge_gensrc.ml#L86 currently just copy *.cS to *.c? However, when I run

uberspark verify -v

within src-nextgen/coss-examples/hello_mul/ucoss_src/uobjcoll, I don’t see nullfunc.cS generated. Thanks!

Yes the current implementation of generating .c from .cS just copies the file contents and lets the pre-processor handle the CASM instruction macro expansions. Our aim is to revise this function per the OP task description so we can do those expansions within our plugin instead of relying on the pre-processor.

I am not sure what you mean, but nullfunc.cS is not generated; it is the source CASM file that is written. What is generated is nullfunc.c within the _staging folder. Can you post the output log from the uberspark verify -v command?

Thanks!

Thanks for the replay. Sorry I meant nullfunc.c not nullfunc.cS. Found it in /uberspark/src-nextgen/cossexamples/hello_mul/ucoss_src/uobjcoll/_staging/uberspark/uobjcoll/generic/hello_mul/uobjs/main. Thanks!

1 Like

Hi @amitvasudevan , I am wondering if it is necessary to modify the ast of .cS file and write the modified ast to the .c file? Would it be possible to just directly write to a .c file when going thru the ast of .cS file. And the verification bridge will utilize the functionalities of frama-c to parse the generated .c file.

Good point! Yes you can directly write to the .c file. Thanks @zhang-zichao !

1 Like

Hi @amitvasudevan ! Sorry for the delay. I just created a PR. It still have a minor problem. Please have a look and let me know what you think! Thanks!

  • If I don’t include the header files in the original .cS file in the generated .c file, frama-c will complaint. For example, if you comment out/delete line 73 to 82 in src-nextgen/tools/bridge-plugins/as-bridge/casmbridge_gensrc.ml, those header files will not be included and uberspark verify -v on the hello_mull example will show the following error:
...
uberspark >> [docker] [kernel] Parsing nullfunc.c (with preprocessing)
uberspark >> [docker] [kernel] nullfunc.c:7: 
uberspark >> [docker]   syntax error:
uberspark >> [docker]   Location: line 7, between columns 21 and 31, before or at token: )
uberspark >> [docker]   5     _impl__casm__popl_ebx();
uberspark >> [docker]   6     _impl__casm__popl_esi();
uberspark >> [docker]   7     hwm_cpu_gprs_eip = *(uint32_t *)hwm_cpu_gprs_esp;
uberspark >> [docker]         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
uberspark >> [docker]   8     hwm_cpu_gprs_esp += sizeof(uint32_t);
uberspark >> [docker]   9     return;
uberspark >> [docker] [kernel] Frama-C aborted: invalid user input.
uberspark >> > invoke_bridge: end(l_retval=false)...
uberspark >> ERROR: error in invoking action bridge!
uberspark >> ERROR: Could not process action!
uberspark: could not create and initialize operation context!

Currently those header files is hard coded into the output file (line 73 to 82). One potential solution is to pass the architecture information to the casm_genc function and to insert the appropriate header files. What do you think?

Can we just copy the #include lines from the source .cS file into the generated .c files verbatim? A simple function outline like the one below could achieve it:

fd = open input file
while (end of lines in fd){
  line = readline
  trim_leading_whitespace(line)
  if line starts with "#include" copy to output file
}

Thoughts?