`call` causes state splitting
Nadie ha tomado este issue todavía.
Evaluación
- Dificultad
- 4/5
- Tiempo estimado
- 3-5 días
- Aptitud para principiantes
- 25/100
Línea de trabajo
Comienza reproduciendo el grafo de ejecución de la llamada a la función "main" de wrc20 después de que el módulo se haya cargado en el backend de Haskell. Inspecciona el axioma 112 y los nodos 94 y 111, comparando la reducción de la llamada con el estado de invocación resultante. Se considera terminado cuando se haya explicado la división de estado no intencionada y la ejecución de la llamada se comporte como se espera.
Escrito por el modelo de indexación a partir del texto del issue.
Descripción
The below screenshot of the execution graph in the Haskell backend shows the splitting at axiom 112, which is call. The splitting occurs in node 94 and 111.
This is when calling the "main" function of wrc20 after the module has been loaded.
Axiom 112
Kore (95)> axiom 112
\rewrites{SortGeneratedTopCell{}}(
\and{SortGeneratedTopCell{}}(
\top{SortGeneratedTopCell{}}(),
Lbl'-LT-'generatedTop'-GT-'{}(
Lbl'-LT-'ewasm'-GT-'{}(
Var'Unds'23:SortEeiCell{},
Lbl'-LT-'wasm'-GT-'{}(
Lbl'-LT-'k'-GT-'{}(
kseq{}(
/* Inj: */ inj{SortPlainInstr{}, SortKItem{}}(
Lblcall'UndsUnds'WASM'Unds'PlainInstr'Unds'Index{}(
VarTFIDX:SortIndex{}
)
),
VarDotVar3:SortK{}
)
),
Var'Unds'16:SortValstackCell{},
Lbl'-LT-'curFrame'-GT-'{}(
Var'Unds'0:SortLocalsCell{},
Var'Unds'1:SortLocalIdsCell{},
Lbl'-LT-'curModIdx'-GT-'{}(
/* Inj: */ inj{SortInt{}, SortOptionalInt{}}(
VarCUR:SortInt{}
)
),
Var'Unds'2:SortLabelDepthCell{},
Var'Unds'3:SortLabelIdsCell{}
),
Var'Unds'17:SortModuleRegistryCell{},
Var'Unds'18:SortModuleIdsCell{},
Lbl'-LT-'moduleInstances'-GT-'{}(
/* builtin: */
Lbl'Unds'ModuleInstCellMap'Unds'{}(
/* element: */ LblModuleInstCellMapItem{}(
Lbl'-LT-'modIdx'-GT-'{}(VarCUR:SortInt{}),
Lbl'-LT-'moduleInst'-GT-'{}(
Lbl'-LT-'modIdx'-GT-'{}(VarCUR:SortInt{}),
Var'Unds'4:SortExportsCell{},
Var'Unds'5:SortTypeIdsCell{},
Var'Unds'6:SortTypesCell{},
Var'Unds'7:SortNextTypeIdxCell{},
Lbl'-LT-'funcIds'-GT-'{}(VarIDS:SortMap{}),
Lbl'-LT-'funcAddrs'-GT-'{}(
/* builtin: */
Lbl'Unds'Map'Unds'{}(
/* element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
/* Inj: */ inj{SortInt{}, SortKItem{}}(
Lbl'Hash'ContextLookup'LParUndsCommUndsRParUnds'WASM-DATA'Unds'Int'Unds'Map'Unds'Index{}(
VarIDS:SortMap{},
VarTFIDX:SortIndex{}
)
),
/* Inj: */ inj{SortInt{}, SortKItem{}}(
VarFADDR:SortInt{}
)
),
/* opaque child: */ VarDotVar7:SortMap{}
)
),
Var'Unds'8:SortNextFuncIdxCell{},
Var'Unds'9:SortTabIdsCell{},
Var'Unds'10:SortTabAddrsCell{},
Var'Unds'11:SortMemIdsCell{},
Var'Unds'12:SortMemAddrsCell{},
Var'Unds'13:SortGlobIdsCell{},
Var'Unds'14:SortGlobalAddrsCell{},
Var'Unds'15:SortNextGlobIdxCell{}
)
),
/* opaque child: */ VarDotVar5:SortModuleInstCellMap{}
)
),
Var'Unds'19:SortNextModuleIdxCell{},
Var'Unds'20:SortMainStoreCell{},
Var'Unds'21:SortDeterministicMemoryGrowthCell{},
Var'Unds'22:SortNextFreshIdCell{}
),
Var'Unds'24:SortParamstackCell{}
),
VarDotVar0:SortGeneratedCounterCell{}
)
),
\and{SortGeneratedTopCell{}}(
\top{SortGeneratedTopCell{}}(),
Lbl'-LT-'generatedTop'-GT-'{}(
Lbl'-LT-'ewasm'-GT-'{}(
Var'Unds'23:SortEeiCell{},
Lbl'-LT-'wasm'-GT-'{}(
Lbl'-LT-'k'-GT-'{}(
kseq{}(
/* Inj: */ inj{SortInstr{}, SortKItem{}}(
Lbl'LPar'invoke'UndsRParUnds'WASM'Unds'Instr'Unds'Int{}(
VarFADDR:SortInt{}
)
),
VarDotVar3:SortK{}
)
),
Var'Unds'16:SortValstackCell{},
Lbl'-LT-'curFrame'-GT-'{}(
Var'Unds'0:SortLocalsCell{},
Var'Unds'1:SortLocalIdsCell{},
Lbl'-LT-'curModIdx'-GT-'{}(
/* Inj: */ inj{SortInt{}, SortOptionalInt{}}(
VarCUR:SortInt{}
)
),
Var'Unds'2:SortLabelDepthCell{},
Var'Unds'3:SortLabelIdsCell{}
),
Var'Unds'17:SortModuleRegistryCell{},
Var'Unds'18:SortModuleIdsCell{},
Lbl'-LT-'moduleInstances'-GT-'{}(
/* builtin: */
Lbl'Unds'ModuleInstCellMap'Unds'{}(
/* element: */ LblModuleInstCellMapItem{}(
Lbl'-LT-'modIdx'-GT-'{}(VarCUR:SortInt{}),
Lbl'-LT-'moduleInst'-GT-'{}(
Lbl'-LT-'modIdx'-GT-'{}(VarCUR:SortInt{}),
Var'Unds'4:SortExportsCell{},
Var'Unds'5:SortTypeIdsCell{},
Var'Unds'6:SortTypesCell{},
Var'Unds'7:SortNextTypeIdxCell{},
Lbl'-LT-'funcIds'-GT-'{}(VarIDS:SortMap{}),
Lbl'-LT-'funcAddrs'-GT-'{}(
/* builtin: */
Lbl'Unds'Map'Unds'{}(
/* element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
/* Inj: */ inj{SortInt{}, SortKItem{}}(
Lbl'Hash'ContextLookup'LParUndsCommUndsRParUnds'WASM-DATA'Unds'Int'Unds'Map'Unds'Index{}(
VarIDS:SortMap{},
VarTFIDX:SortIndex{}
)
),
/* Inj: */ inj{SortInt{}, SortKItem{}}(
VarFADDR:SortInt{}
)
),
/* opaque child: */ VarDotVar7:SortMap{}
)
),
Var'Unds'8:SortNextFuncIdxCell{},
Var'Unds'9:SortTabIdsCell{},
Var'Unds'10:SortTabAddrsCell{},
Var'Unds'11:SortMemIdsCell{},
Var'Unds'12:SortMemAddrsCell{},
Var'Unds'13:SortGlobIdsCell{},
Var'Unds'14:SortGlobalAddrsCell{},
Var'Unds'15:SortNextGlobIdxCell{}
)
),
/* opaque child: */ VarDotVar5:SortModuleInstCellMap{}
)
),
Var'Unds'19:SortNextModuleIdxCell{},
Var'Unds'20:SortMainStoreCell{},
Var'Unds'21:SortDeterministicMemoryGrowthCell{},
Var'Unds'22:SortNextFreshIdCell{}
),
Var'Unds'24:SortParamstackCell{}
),
VarDotVar0:SortGeneratedCounterCell{}
)
)
)
- Lenguaje dominante
- WebAssembly
- Estrellas
- 106
- Forks
- 24
- Métricas de merge de PR
- Sin PR fusionados en 30 d
Preparar el entorno
Primeros pasos
- Lee el issue completo y luego la guía de contribución del proyecto.
- Comenta en el issue que vas a ocuparte — evita que dos personas hagan lo mismo.
- Haz un fork del repositorio y trabaja en una rama.
- Abre un pull request que haga referencia al número del issue.
Más de runtimeverification/wasm-semantics
-
enhancement
Dificultad 2/5 1-3 horas Aptitud para principiantes 55/100
-
bug
Dificultad 4/5 3-5 días Aptitud para principiantes 35/100
-
Dificultad 3/5 1-2 días Aptitud para principiantes 48/100
-
Dificultad 3/5 1-2 días Aptitud para principiantes 55/100
-
Improve tokenisation supportAbierto
Dificultad 4/5 3-5 días Aptitud para principiantes 35/100
Todos los issues de runtimeverification/wasm-semantics
Issues similares
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 84/100
objectionary/jeo-maven-plugin#1827 ·
Los mantenedores suelen responder en 4 días
-
backend:DirectX
Dificultad 2/5 1-3 horas Aptitud para principiantes 84/100
llvm/llvm-project#227530 ·
Los mantenedores suelen responder en 1 día
-
`enzymexla.linalg.lu` lowering fails for a tall matrix: the permutation is built with the pivot typeAbierto
Dificultad 2/5 1-3 horas Aptitud para principiantes 78/100
EnzymeAD/Enzyme-JAX#3286 ·
Los mantenedores suelen responder en 1 día
-
bot-triaged oncall: cpu inductor
Dificultad 2/5 1-3 horas Aptitud para principiantes 78/100
pytorch/pytorch#199058 · 1 comentario ·
Los mantenedores suelen responder en 1 día
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 82/100
WebAssembly/component-model#733 · 1 comentario ·
Los mantenedores suelen responder en 2 días