Theory Voblint_Codegen
theory Voblint_Codegen
imports
"Voblint_CLI.Trace_Run"
begin
section "Code export surface"
text ‹
Top-level definitions normally supply their own code equations. Locale definitions
need care: an inline ‹[code]› attribute is applied through interpretation and
does not register the generic constant for direct calls with abstract locale
parameters. Register those equations after the defining locale's ‹end›, in the
theory that owns them, as the grouped ‹declare ... [code]› in
\<^theory>‹Voblint_Result.DG_Analysis› does. Keep this export theory focused on roots.
If a locale theorem still has assumptions, it is not an unconditional code
equation. Discharge them through an interpretation or derive a code equation for
the concrete caller. A successful attribute declaration alone does not establish
executability: check its warnings, export the actual roots, and compile the OCaml.
Use ‹[code]› to retain a named function. ‹[code_unfold]› rewrites its uses during
preprocessing and can duplicate its body in generated callers; it is not a
substitute for a missing code equation.
›
text ‹
This session owns executable exports; the examples session proves and demonstrates the
exported definitions without materializing generated code.
One export block, deliberately. The external OCaml regression driver under
‹codegen/regression/ocaml/› needs a handful of CFG-inspection constants the CLI
never calls; a second, narrower block would not make any surface narrower, because
Isabelle emits the reachable transitive closure of whatever is named. Those constants
are named here instead, so there is one generated artifact for one analysis.
This is still not the project's public API boundary, but it is not nothing either.
Three things are decided separately here:
▪ the roots decide what the emitted OCaml ∗‹signature› exposes, and how much of it
is transparent rather than abstract;
▪ their transitive closure decides what the ∗‹implementation› contains, which no
shortening of the root list reduces;
▪ ‹module_name› decides the ∗‹packaging›.
So trimming a root narrows what a client can name and match on, while leaving the
emitted code the same size. A supported external surface --- one that could rename a
constructor, or hide a representation behind an eliminator --- belongs in the
handwritten OCaml facade ▩‹cli/voblint.ml› rather than in the shape of this
list.
›
text ‹
The roots below are the ∗‹intended callable surface›: what handwritten OCaml under
‹cli/›, ‹codegen/regression/ocaml/› and ‹tests/property/› actually calls. Everything else
in the emitted module is serializer-reachable implementation detail, still present and
still callable --- the signature narrows with the root list, the code does not. So the
intent recorded here is not enforced. Handwritten OCaml names the export through the
facade ▩‹cli/voblint.ml› (module ‹Voblint›), which re-exports this module's
signature unchanged: the root list still decides what the facade can expose, and the
facade is the one place a later, narrower surface would be stated.
Analysis entry goes through \<^const>‹run_voblint›, which checks the
activation list and well-formedness and runs the requested analyses, update rule and
context policy. Every combination is answered, so the CLI never decides legality.
\<^const>‹run_voblint_traced› is the same function in the logic
(@{thm [source] run_voblint_traced_eq}); only its code reports solver steps through the trace
hook, and the CLI calls it only when a trace is requested.
The last group of roots is there for signature visibility rather than for dispatch.
A constant the serializer does not consider public is emitted but left out of the
module signature, and a datatype it does not consider public stays abstract, which
makes it unmatchable. So anything handwritten OCaml names --- even only to take it
apart --- has to be a root: ‹Bot›/‹Lifted›, which the CLI matches to tell a
dead point from a live verdict, and ‹prog_table›/‹prog_main›/‹prog_procs›, which
the OCaml program printer reads on a round trip.
Nothing calls these on the CLI's analysis path, so a reading of the list as "the
callable surface" alone would drop them, and the resulting break shows up not here but
in an OCaml consumer, as an unbound value or a match on an abstract type.
›
text ‹
‹module_name Generated› puts the whole reachable program into one OCaml module rather
than one module per contributing Isabelle theory. The alternative --- letting the
serializer split by theory --- does not survive contact with this program: OCaml's
single-file output emits modules in dependency order and cannot express a cycle, and
the theories here are mutually dependent at code level (the executable state is
instantiated at the solver's own widening/narrowing classes, and the CFG-specific
solver instantiation needs ‹cfg_node› back). Even a split that Isabelle accepts can
fail later in ▩‹ocamlfind ocamlopt›, on a type-class dictionary field that
module-signature inference does not expose across a boundary the unsplit default never
had.
So the generated internals are monolithic, and this says so directly instead of
arriving there by remapping every contributing theory onto one name by hand. Modularity,
if wanted, belongs in the handwritten facade over ‹Generated›,
▩‹cli/voblint.ml›, which today includes it whole.
Two further modules are emitted regardless: ‹Bit_Shifts› and ‹Str_Literal› are HOL's
own runtime support, injected as literal target code rather than generated from
constants here.
›
text ‹
The list below is grouped by what each name is ∗‹for›, because the groups answer
different questions and only one of them is an operation.
▪ ❙‹Run.› \<^const>‹run_voblint›, and its traced twin
\<^const>‹run_voblint_traced›. Everything a caller can ask the analyser to do goes
through one of them; the untraced one reaches no hand-written target code.
▪ ❙‹Result.› \<^type>‹analysis_answer›'s cases, which a caller must tell apart, the
projection \<^const>‹render_report› that turns an analysed report into displayable
data, and the readers of that data: contexts, states, routes, checks, globals and
diagnostics. The records reach OCaml abstract, readable only through their
selectors, so a field added later cannot break a consumer that matched on field
order. A caller maps \<^const>‹render_report› over the answer with
\<^const>‹map_analysis_answer›, passing the value printer it wants: the CLI composes
\<^const>‹string_of_abstract_value› with its decoding of ASCII symbol tokens.
▪ ❙‹Ask.› The values naming a request: which domain, which rule merges
side-effected globals, which context policy. A caller constructs these, so their
constructors are public.
▪ ❙‹Program.› What the frontend builds an \<^type>‹imp_prog› out of: the command
and expression constructors, the program builder, and the numeral and character
conversions that bridge OCaml's integers to HOL's.
▪ ❙‹Inspect.› Structural readers with no consumer on the CLI's analysis path.
They exist for the OCaml program printer and the CFG regressions, and are listed
apart so that reading the surface as ``what the CLI calls'' does not quietly drop
them.
▪ ❙‹Trace.› The solver's events and the readers a run hands the tracer
(\<^theory>‹Voblint_CLI.Trace_Run›). The CLI's trace renderer matches on them, so
they must be public.
›
export_code
run_voblint run_voblint_traced
Invalid_Activation Malformed_Program No_Answer Analysed map_analysis_answer
render_report
res_cfg res_contexts res_states res_joined res_routes res_checks res_globals res_diagnostics
res_graph graph_nodes graph_edges Local_Node Global_Node
Intra_Dep Enter_Dep Combine_Dep Continue_Dep Global_Read Global_Write
Context_Unit Context_Entry Context_Call_String
state_point state_context state_value state_checks state_diagnostics state_steps
Field_Store Field_Whole
route_point route_context route_callee route_targets
check_point check_label check_exp check_verdict
global_unknown global_state Global_Named Global_Seed
diagnostic_point diagnostic_occurrence diagnostic_obligation diagnostic_verdict
arithmetic_operation arithmetic_divisor
Check_Proved Check_Refuted Check_Unknown
Bot Lifted
cfg_entry cfg_node_list
Analysis_Config
Program_Globals_Flow_Sensitive Program_Globals_Flow_Insensitive
Sign_Analysis Interval_Analysis Int_Analysis Refine_Fixpoint Refine_Once Refine_Never
Parity_Analysis Congruence_Analysis Order_Analysis
Globals_Join Globals_Per_Origin Globals_Warrow Globals_Warrow_Per_Origin Globals_Bounded_Narrowing
Ctx_None Ctx_EntryState Ctx_CallString
mk_program gproc_decl_ext
SKIP Assign Seq gcom.If While Return Check gcom.Call
N V Plus Minus Times Div Mod
exp.Not And Or Less exp.Eq
Statement FunctionEntry FunctionResult
int_of_integer nat_of_integer integer_of_int integer_of_nat
declared_global_vars
prog_table prog_main prog_procs
prog_cfg cfg_intra_list cfg_calls_list prog_stmt_post_order
EA_Nop EA_Assign EA_Special EA_Assume EA_AssumeNot EA_Body EA_Ret EA_Check
CallEdge Nondet_Int
Ev_Start Ev_Stop Ev_Query Ev_Query_Wpoint Ev_Iterate_From_Query Ev_Add_Infl Ev_Answer
Ev_Query_Global Ev_Answer_Global Ev_Iterate Ev_Eq Ev_Rhs Ev_Still_Unstable Ev_Widen Ev_Sol
Ev_Wpoint_Remove Ev_Wpoint_Clear Ev_Update Ev_Iterate_Changed Ev_Side Ev_Update_Global
Ev_Destabilize
Ev_Stable_Remove
Ev_Route Trace_Printers Trace_Buffer Trace_Global Trace_Seed string_of_abstract_value Inl Inr
in OCaml module_name Generated file_prefix "Voblint_Generated"
end