Hacktoberfest 2026: los issues que los mantenedores marcaron para octubre, abiertos y aptos para principiantes. Explorar issues de Hacktoberfest

Concolic Explorer

Abierto
  • ¿Algo no está bien?
#4,937 0 comentarios 0 reacciones 0 asignados Ver en GitHub

Nadie ha tomado este issue todavía.

Evaluación

Dificultad
5/5
Tiempo estimado
Más de una semana
Aptitud para principiantes
32/100
Tipo de issue
Nueva funcionalidad
Claridad
Bastante claro
Estado de actividad
Tranquilo
Stack tecnológico
python
Área
compilers, testing-qa

Línea de trabajo

The issue names ConcolicExplorer, Checker, generate_proof_trace, and guided_execute, but no files or tests. Start by locating those entry points and tracing the existing LLVM-backed execution flow. Done means the worklist explores satisfiable remainders to completion, reports UNKNOWN as UndecidedObligation, and respects the stated deterministic-semantics and missing-rule limitations.

Escrito por el modelo de indexación a partir del texto del issue.

Descripción

ConcolicExplorer builds the proof the Checker validates: a concrete seed names one path, the Checker folds it into edges plus a remainder, and that remainder's model is the next seed — repeated until no satisfiable remainder is left.

worklist ← [ (root, get_model(φ)) ]            # an open node + a concrete seed for it
while worklist:
    (node, seed) ← worklist.pop()
    τ ← generate_proof_trace(seed)              # run the seed on the LLVM backend → rule sequence
    S ← node
    loop:
        r ← guided_execute(S, τ)                # fold edges; stop at first SAT remainder or trace end
        record r.edge
        case r:
          SAT remainder (guard g):              # taken rule covers only part of S
            record branch g (→ r.S')
            worklist.push( (node ∧ ¬g, r.model) )   # still-uncovered region: more guards to find
            S, τ ← r.S', τ[r.consumed:]             # continue along the taken branch
          UNKNOWN:
            emit UndecidedObligation; break
          TRACE END:
            close S' (cover to target / loop, terminal, or Failed counterexample); break
# worklist empty ⇒ every remainder unsatisfiable or covered ⇒ all paths covered
Limitations
  • Non-deterministic semantics. Concrete execution takes one rule per state (by priority), so it can never witness several rules applying to the same concrete state — hence the deterministic-semantics scope.
  • Rules missing from the concrete trace. Some rules never fire in concrete execution (e.g. symbolic-only [symbolic] rules and lemmas), so the LLVM trace cannot name them; the symbolic side must supply them itself. This may need composable symbolic execution to ensure the concolic execution only works for the src without the assume instructions in the test.
Lenguaje dominante
Python
Estrellas
591
Forks
163
Sin PR fusionados en 30 d

Preparar el entorno

Primeros pasos

  1. Lee el issue completo y luego la guía de contribución del proyecto.
  2. Comenta en el issue que vas a ocuparte — evita que dos personas hagan lo mismo.
  3. Haz un fork del repositorio y trabaja en una rama.
  4. Abre un pull request que haga referencia al número del issue.

Más de runtimeverification/k

Todos los issues de runtimeverification/k

Issues similares

Más issues de Python

Recibe los nuevos issues en tu correo

Un resumen breve de issues de GitHub para principiantes.