Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

sv-benchmarks intel-tdx-module parsing errors #176

Open
sim642 opened this issue Nov 8, 2024 · 1 comment
Open

sv-benchmarks intel-tdx-module parsing errors #176

sim642 opened this issue Nov 8, 2024 · 1 comment
Labels

Comments

@sim642
Copy link
Member

sim642 commented Nov 8, 2024

SV-COMP has a new SoftwareSystems subcategory where we cannot parse any of the programs. For example:

$ ./goblint --conf conf/svcomp25.json --sets ana.specification ../sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 64bit ../sv-benchmarks/c
/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i
[Warning] --sets is deprecated, use --set instead.
[Warning] --sets is deprecated, use --set instead.
REDOREDOREDOREDO../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:6002: Error: Cannot find designated field leaf
error in createGlobal(cpuid_lookup: ../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:6002): GoblintCil__Errormsg.Error../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:6450: Error: Cannot find designated field leaf
error in createGlobal(cpuid_configurable: ../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:6450): GoblintCil__Errormsg.Error../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:6542: Error: Cannot find designated field vmm_rd_mask
error in createGlobal(global_sys_lookup: ../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:6542): GoblintCil__Errormsg.Error../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:7139: Error: Cannot find designated field prod_rd_mask
error in createGlobal(td_l2_vmcs_lookup: ../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:7139): GoblintCil__Errormsg.Error../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:8725: Error: Cannot find designated field prod_rd_mask
error in createGlobal(td_vmcs_lookup: ../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:8725): GoblintCil__Errormsg.Error../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:10167: Error: Cannot find designated field prod_rd_mask
error in createGlobal(tdr_tdcs_lookup: ../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:10167): GoblintCil__Errormsg.Error../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:11104: Error: Cannot find designated field prod_rd_mask
error in createGlobal(tdvps_lookup: ../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:11104): GoblintCil__Errormsg.ErrorREDOREDOREDOREDOError: There were parsing errors in ../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i
Fatal error: exception Goblint_lib__Maingoblint.FrontendError("Errormsg.Error")
@sim642 sim642 added the bug label Nov 8, 2024
@sim642
Copy link
Member Author

sim642 commented Nov 8, 2024

The first error also happens on this minimized program:

typedef unsigned int uint32_t;
typedef unsigned long long int uint64_t;
typedef union
{
    struct
    {
        uint32_t leaf;
        uint32_t subleaf;
    };
    uint64_t raw;
} cpuid_config_leaf_subleaf_t;
typedef struct
{
    cpuid_config_leaf_subleaf_t leaf_subleaf;
} cpuid_lookup_t;
extern const cpuid_lookup_t cpuid_lookup[68];
const cpuid_lookup_t cpuid_lookup[68] = {
 [10] = { .leaf_subleaf = {.leaf = 0x0, .subleaf = 0xffffffff}}
};

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant