diff --git a/README.md b/README.md index e1c95cf1..fb569767 100644 --- a/README.md +++ b/README.md @@ -7,7 +7,7 @@ prevent entire categories of bugs. The language's goal is ... [![CI](https://github.com/berkeleynerd/safe/actions/workflows/ci.yml/badge.svg)](https://github.com/berkeleynerd/safe/actions/workflows/ci.yml) ![Spec version](https://img.shields.io/badge/spec-v0.1_working_draft-blue) -![Proved fixtures](https://img.shields.io/badge/proved_fixtures-262-brightgreen) +![Proved fixtures](https://img.shields.io/badge/proved_fixtures-263-brightgreen) The current toolchain compiles it through Ada/SPARK-oriented artifacts. The user-facing goal is not to preserve Ada @@ -150,7 +150,7 @@ itself. Two independent evidence channels back the safety claims: **Emitted proof corpus.** The blocking emitted-proof inventory currently covers -262 fixtures with 4 explicit exclusions and 0 uncovered fixtures: 3 frontend +263 fixtures with 4 explicit exclusions and 0 uncovered fixtures: 3 frontend spec exclusions and 1 intentional tooling-reject fixture. No compiling runtime-regression fixture remains outside the emitted proof lane. These fixtures are emitted as Ada/SPARK and verified by GNATprove through the @@ -163,11 +163,11 @@ proved, 1 Silver VC justified, and 0 unproved. Its 16 templates account for | Metric | Value | |--------|-------| -| Proved emitted fixtures | 262 (4 exclusions: 3 spec, 1 tooling, 0 runtime proof gaps; 0 uncovered) | +| Proved emitted fixtures | 263 (4 exclusions: 3 spec, 1 tooling, 0 runtime proof gaps; 0 uncovered) | | Companion template VCs | 553 total (414 proved, 1 justified, 0 unproved, 138 flow passed) | | Companion templates | 16 templates, 315 template checks | | Tracked proof assumptions | [13](companion/assumptions.yaml) (12 open, 1 resolved) | -| Test corpus | 650 `.safe` files (positive, negative, build, concurrency, interfaces, embedded, emitted-shape) | +| Test corpus | 651 `.safe` files (positive, negative, build, concurrency, interfaces, embedded, emitted-shape) | | Embedded evidence lane | STM32F4 / Jorvik / Renode (blocking in CI) | | Compiler size | ~73K LOC Ada across 75 source files | | Emitter size | ~26K LOC Ada across 14 emitter source files | diff --git a/compiler_impl/src/safe_frontend-ada_emit-statements.adb b/compiler_impl/src/safe_frontend-ada_emit-statements.adb index 02122524..db64d5b2 100644 --- a/compiler_impl/src/safe_frontend-ada_emit-statements.adb +++ b/compiler_impl/src/safe_frontend-ada_emit-statements.adb @@ -46,6 +46,7 @@ package body Safe_Frontend.Ada_Emit.Statements is type Shared_Condition_Replacement is record Call_Image : FT.UString := FT.To_UString (""); + Snapshot_Name : FT.UString := FT.To_UString (""); Replacement_Image : FT.UString := FT.To_UString (""); end record; @@ -230,13 +231,14 @@ package body Safe_Frontend.Ada_Emit.Statements is Item_Range : CM.Discrete_Range; State : in out Emit_State) return String; procedure Append_Assignment - (Buffer : in out SU.Unbounded_String; - Unit : CM.Resolved_Unit; - Document : GM.Mir_Document; - State : in out Emit_State; - Stmt : CM.Statement; - Depth : Natural; - In_Loop : Boolean := False); + (Buffer : in out SU.Unbounded_String; + Unit : CM.Resolved_Unit; + Document : GM.Mir_Document; + State : in out Emit_State; + Stmt : CM.Statement; + Statement_Index : Positive; + Depth : Natural; + In_Loop : Boolean := False); procedure Append_Float_Loop_Invariant (Buffer : in out SU.Unbounded_String; Unit : CM.Resolved_Unit; @@ -330,7 +332,8 @@ package body Safe_Frontend.Ada_Emit.Statements is State : in out Emit_State; Target : CM.Expr_Access; Value : CM.Expr_Access; - Depth : Natural) + Depth : Natural; + Rendered_Value_Image : String := "") ; procedure Append_Float_Narrowing_Checks (Buffer : in out SU.Unbounded_String; @@ -2531,6 +2534,7 @@ package body Safe_Frontend.Ada_Emit.Statements is begin Rendered.Replacements.Append ((Call_Image => Info.Call_Image, + Snapshot_Name => FT.To_UString (Snapshot_Name), Replacement_Image => FT.To_UString (Snapshot_Name & "." & FT.To_String (Info.Field_Ada_Name)))); @@ -2644,31 +2648,180 @@ package body Safe_Frontend.Ada_Emit.Statements is return SU.To_String (Result); end Replace_All; - function Render_Shared_Condition - (Unit : CM.Resolved_Unit; - Document : GM.Mir_Document; - Expr : CM.Expr_Access; - State : in out Emit_State; - Statement_Index : Positive) return Shared_Condition_Render + procedure Apply_Shared_Condition_Replacements + (Rendered : in out Shared_Condition_Render; + Base_Image : String) is - Result : Shared_Condition_Render; - Image : SU.Unbounded_String; + Image : SU.Unbounded_String := SU.To_Unbounded_String (Base_Image); + Used_Snapshots : Shared_Condition_Snapshot_Vectors.Vector; + Used_Replacements : Shared_Condition_Replacement_Vectors.Vector; + + function Uses_Snapshot + (Replacement : Shared_Condition_Replacement; + Snapshot : Shared_Condition_Snapshot) return Boolean + is + Prefix : constant String := FT.To_String (Replacement.Snapshot_Name) & "."; + Replacement_Text : constant String := FT.To_String (Replacement.Replacement_Image); + begin + -- Snapshot-name equality identifies the paired declaration. Keep + -- the prefix check as a fail-fast construction guard: a future + -- malformed replacement image must still name the retained snapshot + -- local it depends on. + return + Snapshot.Snapshot_Name = Replacement.Snapshot_Name + and then Replacement_Text'Length >= Prefix'Length + and then Replacement_Text + (Replacement_Text'First .. Replacement_Text'First + Prefix'Length - 1) = Prefix; + end Uses_Snapshot; + + function Collect_Replacement_Snapshot + (Replacement : Shared_Condition_Replacement) + return Boolean + is + begin + for Snapshot of Rendered.Snapshots loop + if Uses_Snapshot (Replacement, Snapshot) then + for Existing of Used_Snapshots loop + if FT.To_String (Existing.Snapshot_Name) + = FT.To_String (Snapshot.Snapshot_Name) + then + -- Snapshot already retained; the caller records this + -- additional field replacement against the shared + -- declaration. + return True; + end if; + end loop; + + Used_Snapshots.Append (Snapshot); + return True; + end if; + end loop; + return False; + end Collect_Replacement_Snapshot; begin - Collect_Shared_Condition_Snapshots - (Unit, Document, Expr, Statement_Index, Result); - Image := SU.To_Unbounded_String (Render_Expr (Unit, Document, Expr, State)); + for Replacement of Rendered.Replacements loop + declare + Before : constant String := SU.To_String (Image); + -- Replacement images are snapshot-selected components. They must + -- not contain another getter call image, or sequential replacement + -- could double-substitute already rewritten Ada text. + After : constant String := + Replace_All + (Before, + FT.To_String (Replacement.Call_Image), + FT.To_String (Replacement.Replacement_Image)); + begin + if After /= Before then + if Collect_Replacement_Snapshot (Replacement) then + Image := SU.To_Unbounded_String (After); + Used_Replacements.Append (Replacement); + else + -- If future replacement construction breaks the paired + -- snapshot invariant, fail here instead of emitting a + -- reference to an undeclared snapshot local. + Raise_Internal + ("shared snapshot replacement missing snapshot declaration during Ada emission"); + end if; + end if; + end; + end loop; - for Replacement of Result.Replacements loop - Image := + -- A renderer may fold or rewrite an expression before replacement. Keep + -- only snapshots whose getter text was actually replaced in Base_Image. + Rendered.Snapshots := Used_Snapshots; + -- Variant while guards reuse the replacement vector after condition + -- rendering, so keep it in sync with the pruned snapshot set. + Rendered.Replacements := Used_Replacements; + Rendered.Image := FT.To_UString (SU.To_String (Image)); + end Apply_Shared_Condition_Replacements; + + procedure Prune_Shared_Snapshots + (Rendered : in out Shared_Condition_Render; + Base_Image : String) + is + Probe : Shared_Condition_Render := Rendered; + begin + Apply_Shared_Condition_Replacements (Probe, Base_Image); + Rendered.Snapshots := Probe.Snapshots; + Rendered.Replacements := Probe.Replacements; + end Prune_Shared_Snapshots; + + function Apply_Shared_Replacements_To_Image + (Image : String; + Replacements : Shared_Condition_Replacement_Vectors.Vector) return String + is + Result : SU.Unbounded_String := SU.To_Unbounded_String (Image); + begin + for Replacement of Replacements loop + Result := SU.To_Unbounded_String (Replace_All - (SU.To_String (Image), + (SU.To_String (Result), FT.To_String (Replacement.Call_Image), FT.To_String (Replacement.Replacement_Image))); end loop; - Result.Image := FT.To_UString (SU.To_String (Image)); + return SU.To_String (Result); + end Apply_Shared_Replacements_To_Image; + + procedure Require_Shared_Replacements + (Unit : CM.Resolved_Unit; + Document : GM.Mir_Document; + Expr : CM.Expr_Access; + Statement_Index : Positive; + Base_Image : String; + Context : String) + is + Probe : Shared_Condition_Render; + begin + Collect_Shared_Condition_Snapshots + (Unit, Document, Expr, Statement_Index, Probe); + + for Replacement of Probe.Replacements loop + if Replace_All + (Base_Image, + FT.To_String (Replacement.Call_Image), + FT.To_String (Replacement.Replacement_Image)) + = Base_Image + then + Raise_Internal + ("shared snapshot replacement missing from rendered " + & Context + & " during Ada emission"); + end if; + end loop; + end Require_Shared_Replacements; + + function Render_Shared_Condition_From_Image + (Unit : CM.Resolved_Unit; + Document : GM.Mir_Document; + Expr : CM.Expr_Access; + Statement_Index : Positive; + Base_Image : String) return Shared_Condition_Render + is + Result : Shared_Condition_Render; + begin + Collect_Shared_Condition_Snapshots + (Unit, Document, Expr, Statement_Index, Result); + Apply_Shared_Condition_Replacements (Result, Base_Image); return Result; + end Render_Shared_Condition_From_Image; + + function Render_Shared_Condition + (Unit : CM.Resolved_Unit; + Document : GM.Mir_Document; + Expr : CM.Expr_Access; + State : in out Emit_State; + Statement_Index : Positive) return Shared_Condition_Render + is + begin + return + Render_Shared_Condition_From_Image + (Unit, + Document, + Expr, + Statement_Index, + Render_Expr (Unit, Document, Expr, State)); end Render_Shared_Condition; procedure Append_Shared_Condition_Declarations @@ -2690,6 +2843,23 @@ package body Safe_Frontend.Ada_Emit.Statements is end loop; end Append_Shared_Condition_Declarations; + procedure Append_Shared_Rendered_Statement + (Buffer : in out SU.Unbounded_String; + Rendered : Shared_Condition_Render; + Depth : Natural) + is + begin + if Rendered.Snapshots.Is_Empty then + Append_Line (Buffer, FT.To_String (Rendered.Image) & ";", Depth); + else + Append_Line (Buffer, "declare", Depth); + Append_Shared_Condition_Declarations (Buffer, Rendered, Depth + 1); + Append_Line (Buffer, "begin", Depth); + Append_Line (Buffer, FT.To_String (Rendered.Image) & ";", Depth + 1); + Append_Line (Buffer, "end;", Depth); + end if; + end Append_Shared_Rendered_Statement; + function Tail_Statements (Statements : CM.Statement_Access_Vectors.Vector; First : Positive) return CM.Statement_Access_Vectors.Vector @@ -3000,6 +3170,48 @@ package body Safe_Frontend.Ada_Emit.Statements is Expr_Type_Info (Unit, Document, Actual.Prefix))); end Needs_Growable_Indexed_Copy_Back; + Target_Subprogram : CM.Resolved_Subprogram; + Target_Subprogram_Resolved : Boolean := False; + Needs_Copy_Back : Boolean := False; + + function Has_Formal_For_Arg (Arg_Index : Positive) return Boolean is + begin + return + not Target_Subprogram.Params.Is_Empty + and then Arg_Index >= Target_Subprogram.Params.First_Index + and then Arg_Index <= Target_Subprogram.Params.Last_Index; + end Has_Formal_For_Arg; + + function Render_Call_From_Image + (Base_Image : String) return Shared_Condition_Render + is + Result : Shared_Condition_Render; + begin + -- The outer call-statement gate resolves the target before this + -- renderer is reachable. + -- The early fallback path renders without using this copy-back-aware pass. + -- Callees are subprogram references, so iterate only arguments here; + -- arguments with no shared getter call contribute no snapshots. + + for Arg_Index in Call_Expr.Args.First_Index .. Call_Expr.Args.Last_Index loop + Collect_Shared_Condition_Snapshots + (Unit, Document, Call_Expr.Args (Arg_Index), Statement_Index, Result); + end loop; + + for Arg_Index in Call_Expr.Args.First_Index .. Call_Expr.Args.Last_Index loop + Require_Shared_Replacements + (Unit, + Document, + Call_Expr.Args (Arg_Index), + Statement_Index, + Base_Image, + "call argument"); + end loop; + + Apply_Shared_Condition_Replacements (Result, Base_Image); + return Result; + end Render_Call_From_Image; + function Mutable_Actual_Temp_Name (Statement_Index : Positive; Arg_Index : Positive) return String is @@ -3015,10 +3227,17 @@ package body Safe_Frontend.Ada_Emit.Statements is Ada.Strings.Both); end Mutable_Actual_Temp_Name; - procedure Append_Growable_Indexed_Writeback - (Actual : CM.Expr_Access; - Temp_Name : String; - Depth : Natural) + function Mutable_Actual_Index_Temp_Name + (Statement_Index : Positive; + Arg_Index : Positive) return String is + begin + return Mutable_Actual_Temp_Name (Statement_Index, Arg_Index) & "_Index"; + end Mutable_Actual_Index_Temp_Name; + + function Growable_Indexed_Element_Image + (Actual : CM.Expr_Access; + Prefix_Image : String; + Index_Image : String) return String is Prefix_Info : constant GM.Type_Descriptor := Base_Type @@ -3026,49 +3245,106 @@ package body Safe_Frontend.Ada_Emit.Statements is Document, Expr_Type_Info (Unit, Document, Actual.Prefix)); begin - State.Needs_Safe_Array_RT := True; - Append_Line - (Buffer, - Array_Runtime_Instance_Name (Prefix_Info) - & ".Replace_Element (" - & Render_Expr (Unit, Document, Actual.Prefix, State) - & ", Integer (" - & Render_Expr - (Unit, - Document, - Actual.Args (Actual.Args.First_Index), - State) - & "), " - & Temp_Name - & ");", - Depth); - end Append_Growable_Indexed_Writeback; + return + Array_Runtime_Instance_Name (Prefix_Info) + & ".Element (" + & Prefix_Image + & ", " + & Index_Image + & ")"; + end Growable_Indexed_Element_Image; + + function Copy_Back_Init_Image + (Formal : CM.Symbol; + Element_Image : String) return String + is + begin + if Is_Plain_String_Type (Unit, Document, Formal.Type_Info) then + State.Needs_Safe_String_RT := True; + return Element_Image; + elsif Is_Bounded_String_Type (Formal.Type_Info) then + Register_Bounded_String_Type (State, Formal.Type_Info); + return Element_Image; + elsif Is_Integer_Type (Unit, Document, Formal.Type_Info) + or else Is_Float_Type (Unit, Document, Formal.Type_Info) + or else Is_Binary_Type (Unit, Document, Formal.Type_Info) + then + return + Render_Subtype_Indication (Unit, Document, Formal.Type_Info) + & " (" + & Element_Image + & ")"; + end if; + + return Element_Image; + end Copy_Back_Init_Image; + + function Growable_Indexed_Writeback_Image + (Actual : CM.Expr_Access; + Prefix_Image : String; + Index_Image : String; + Temp_Name : String) return String + is + Prefix_Info : constant GM.Type_Descriptor := + Base_Type + (Unit, + Document, + Expr_Type_Info (Unit, Document, Actual.Prefix)); + begin + -- Keep Index_Image embedded literally: copy-back snapshot coverage + -- checks validate that any shared getter calls in the isolated index + -- render also appear in this enclosing writeback image. + return + Array_Runtime_Instance_Name (Prefix_Info) + & ".Replace_Element (" + & Prefix_Image + & ", Integer (" + & Index_Image + & "), " + & Temp_Name + & ")"; + end Growable_Indexed_Writeback_Image; - Target_Subprogram : CM.Resolved_Subprogram; - Needs_Copy_Back : Boolean := False; begin - if not Find_Called_Subprogram (Call_Expr, Target_Subprogram) - or else Call_Expr = null + if Call_Expr = null then + Raise_Internal + ("call statement missing call expression during Ada emission"); + end if; + + Target_Subprogram_Resolved := Find_Called_Subprogram (Call_Expr, Target_Subprogram); + + if not Target_Subprogram_Resolved or else Call_Expr.Kind /= CM.Expr_Call or else Call_Expr.Args.Is_Empty then - Append_Line - (Buffer, - Render_Expr (Unit, Document, Call_Expr, State) & ";", - Depth); + declare + Rendered : constant Shared_Condition_Render := + Render_Shared_Condition_From_Image + (Unit, + Document, + Call_Expr, + Statement_Index, + Render_Expr (Unit, Document, Call_Expr, State)); + begin + Append_Shared_Rendered_Statement (Buffer, Rendered, Depth); + end; return; end if; - for Formal_Index in Target_Subprogram.Params.First_Index .. Target_Subprogram.Params.Last_Index loop - exit when Formal_Index > Call_Expr.Args.Last_Index; - if Needs_Growable_Indexed_Copy_Back - (Target_Subprogram.Params (Formal_Index), - Call_Expr.Args (Formal_Index)) - then - Needs_Copy_Back := True; - exit; - end if; - end loop; + if not Target_Subprogram.Params.Is_Empty then + for Formal_Index in + Target_Subprogram.Params.First_Index .. Target_Subprogram.Params.Last_Index + loop + exit when Formal_Index > Call_Expr.Args.Last_Index; + if Needs_Growable_Indexed_Copy_Back + (Target_Subprogram.Params (Formal_Index), + Call_Expr.Args (Formal_Index)) + then + Needs_Copy_Back := True; + exit; + end if; + end loop; + end if; if not Needs_Copy_Back then declare @@ -3085,7 +3361,7 @@ package body Safe_Frontend.Ada_Emit.Statements is Call_Image := Call_Image & SU.To_Unbounded_String (", "); end if; - if Arg_Index <= Target_Subprogram.Params.Last_Index then + if Has_Formal_For_Arg (Arg_Index) then declare Formal : constant CM.Symbol := Target_Subprogram.Params (Arg_Index); begin @@ -3117,56 +3393,138 @@ package body Safe_Frontend.Ada_Emit.Statements is end; end loop; Call_Image := Call_Image & SU.To_Unbounded_String (")"); - Append_Line (Buffer, SU.To_String (Call_Image) & ";", Depth); + declare + Rendered : constant Shared_Condition_Render := + Render_Call_From_Image (SU.To_String (Call_Image)); + begin + Append_Shared_Rendered_Statement (Buffer, Rendered, Depth); + end; end; return; end if; - Append_Line (Buffer, "declare", Depth); - for Formal_Index in Target_Subprogram.Params.First_Index .. Target_Subprogram.Params.Last_Index loop - exit when Formal_Index > Call_Expr.Args.Last_Index; - if Needs_Growable_Indexed_Copy_Back - (Target_Subprogram.Params (Formal_Index), - Call_Expr.Args (Formal_Index)) - then - declare - Formal : constant CM.Symbol := - Target_Subprogram.Params (Formal_Index); - Temp_Name : constant String := - Mutable_Actual_Temp_Name (Statement_Index, Formal_Index); - Init_Image : constant String := - (if FT.To_String (Formal.Mode) = "out" - then - Default_Value_Expr - (Unit, - Document, - Formal.Type_Info) - else - Render_Expr_For_Target_Type - (Unit, - Document, - Call_Expr.Args (Formal_Index), - Formal.Type_Info, - State)); - begin - Append_Line - (Buffer, - Temp_Name - & " : " - & Render_Type_Name (Formal.Type_Info) - & " := " - & Init_Image - & ";", - Depth + 1); - end; - end if; - end loop; - Append_Line (Buffer, "begin", Depth); declare + package Text_Vectors is new Ada.Containers.Vectors + (Index_Type => Positive, + Element_Type => FT.UString); + + Statement_Rendered : Shared_Condition_Render; + Temp_Declarations : Text_Vectors.Vector; + Writebacks : Text_Vectors.Vector; Call_Image : SU.Unbounded_String := SU.To_Unbounded_String (Render_Expr (Unit, Document, Call_Expr.Callee, State) & " ("); + Combined_Image : SU.Unbounded_String; + + procedure Include_Image (Image : String) is + begin + if SU.Length (Combined_Image) > 0 then + Combined_Image := Combined_Image & SU.To_Unbounded_String (" "); + end if; + Combined_Image := Combined_Image & SU.To_Unbounded_String (Image); + end Include_Image; begin + -- Copy-back calls need one statement-level shared snapshot set: + -- index temp initialization, non-copy-back call arguments, and + -- post-call writeback must all see the same shared-root snapshot. + for Formal_Index in + Target_Subprogram.Params.First_Index .. Target_Subprogram.Params.Last_Index + loop + exit when Formal_Index > Call_Expr.Args.Last_Index; + if Needs_Growable_Indexed_Copy_Back + (Target_Subprogram.Params (Formal_Index), + Call_Expr.Args (Formal_Index)) + then + declare + Actual : constant CM.Expr_Access := + Call_Expr.Args (Formal_Index); + Formal : constant CM.Symbol := + Target_Subprogram.Params (Formal_Index); + Temp_Name : constant String := + Mutable_Actual_Temp_Name (Statement_Index, Formal_Index); + Index_Temp_Name : constant String := + Mutable_Actual_Index_Temp_Name (Statement_Index, Formal_Index); + Index_Expr : constant CM.Expr_Access := + Actual.Args (Actual.Args.First_Index); + begin + if Expr_Needs_Shared_Condition_Snapshot + (Unit, Document, Actual.Prefix) + then + Raise_Unsupported + (State, + Actual.Prefix.Span, + "growable copy-back targets cannot be rooted in shared reads"); + end if; + + declare + Prefix_Image : constant String := + Render_Expr (Unit, Document, Actual.Prefix, State); + Index_Image : constant String := + Render_Expr (Unit, Document, Index_Expr, State); + Index_Declaration_Image : constant String := + Index_Temp_Name + & " : constant Integer := Integer (" + & Index_Image + & ");"; + Actual_Value_Image : constant String := + Growable_Indexed_Element_Image + (Actual, Prefix_Image, Index_Temp_Name); + Init_Image : constant String := + (if FT.To_String (Formal.Mode) = "out" + then + Default_Value_Expr + (Unit, + Document, + Formal.Type_Info) + else + Copy_Back_Init_Image (Formal, Actual_Value_Image)); + Declaration_Image : constant String := + Temp_Name + & " : " + & Render_Type_Name (Formal.Type_Info) + & " := " + & Init_Image + & ";"; + Writeback_Image : constant String := + Growable_Indexed_Writeback_Image + (Actual, Prefix_Image, Index_Temp_Name, Temp_Name); + begin + State.Needs_Safe_Array_RT := True; + -- Snapshot only the index expression. The prefix is the + -- mutable Replace_Element target; rewriting it to a + -- snapshot copy would discard the writeback. + Collect_Shared_Condition_Snapshots + (Unit, + Document, + Index_Expr, + Statement_Index, + Statement_Rendered); + + -- Evaluate the index once before the call. The temp + -- initializer and writeback both use this value, so + -- copy-back cannot retarget if the call mutates data + -- used by the original index expression. + Require_Shared_Replacements + (Unit, + Document, + Index_Expr, + Statement_Index, + Index_Declaration_Image, + "copy-back index temp"); + + Temp_Declarations.Append + (FT.To_UString (Index_Declaration_Image)); + Temp_Declarations.Append + (FT.To_UString (Declaration_Image)); + Writebacks.Append (FT.To_UString (Writeback_Image)); + Include_Image (Index_Declaration_Image); + Include_Image (Declaration_Image); + Include_Image (Writeback_Image); + end; + end; + end if; + end loop; + for Arg_Index in Call_Expr.Args.First_Index .. Call_Expr.Args.Last_Index loop declare Arg_Image : SU.Unbounded_String; @@ -3176,7 +3534,7 @@ package body Safe_Frontend.Ada_Emit.Statements is Call_Image := Call_Image & SU.To_Unbounded_String (", "); end if; - if Arg_Index <= Target_Subprogram.Params.Last_Index + if Has_Formal_For_Arg (Arg_Index) and then Needs_Growable_Indexed_Copy_Back (Target_Subprogram.Params (Arg_Index), Call_Expr.Args (Arg_Index)) @@ -3185,7 +3543,7 @@ package body Safe_Frontend.Ada_Emit.Statements is SU.To_Unbounded_String (Mutable_Actual_Temp_Name (Statement_Index, Arg_Index)); Used_Formal := True; - elsif Arg_Index <= Target_Subprogram.Params.Last_Index then + elsif Has_Formal_For_Arg (Arg_Index) then declare Formal : constant CM.Symbol := Target_Subprogram.Params (Arg_Index); begin @@ -3213,26 +3571,79 @@ package body Safe_Frontend.Ada_Emit.Statements is State)); end if; + if not + (Has_Formal_For_Arg (Arg_Index) + and then Needs_Growable_Indexed_Copy_Back + (Target_Subprogram.Params (Arg_Index), + Call_Expr.Args (Arg_Index))) + then + Collect_Shared_Condition_Snapshots + (Unit, + Document, + Call_Expr.Args (Arg_Index), + Statement_Index, + Statement_Rendered); + end if; + Call_Image := Call_Image & Arg_Image; end; end loop; Call_Image := Call_Image & SU.To_Unbounded_String (")"); - Append_Line (Buffer, SU.To_String (Call_Image) & ";", Depth + 1); - end; + Include_Image (SU.To_String (Call_Image)); - for Formal_Index in Target_Subprogram.Params.First_Index .. Target_Subprogram.Params.Last_Index loop - exit when Formal_Index > Call_Expr.Args.Last_Index; - if Needs_Growable_Indexed_Copy_Back - (Target_Subprogram.Params (Formal_Index), - Call_Expr.Args (Formal_Index)) - then - Append_Growable_Indexed_Writeback - (Call_Expr.Args (Formal_Index), - Mutable_Actual_Temp_Name (Statement_Index, Formal_Index), + for Arg_Index in Call_Expr.Args.First_Index .. Call_Expr.Args.Last_Index loop + if not + (Has_Formal_For_Arg (Arg_Index) + and then Needs_Growable_Indexed_Copy_Back + (Target_Subprogram.Params (Arg_Index), + Call_Expr.Args (Arg_Index))) + then + Require_Shared_Replacements + (Unit, + Document, + Call_Expr.Args (Arg_Index), + Statement_Index, + SU.To_String (Combined_Image), + "copy-back call argument"); + end if; + end loop; + + -- Combined_Image is not emitted. Use the final rendered + -- declaration/writeback/call text only to prune snapshots and + -- replacements that did not actually match those images. + Prune_Shared_Snapshots + (Statement_Rendered, SU.To_String (Combined_Image)); + + Append_Line (Buffer, "declare", Depth); + Append_Shared_Condition_Declarations + (Buffer, Statement_Rendered, Depth + 1); + for Declaration_Image of Temp_Declarations loop + Append_Line + (Buffer, + Apply_Shared_Replacements_To_Image + (FT.To_String (Declaration_Image), + Statement_Rendered.Replacements), Depth + 1); - end if; - end loop; - Append_Line (Buffer, "end;", Depth); + end loop; + Append_Line (Buffer, "begin", Depth); + Append_Line + (Buffer, + Apply_Shared_Replacements_To_Image + (SU.To_String (Call_Image), + Statement_Rendered.Replacements) + & ";", + Depth + 1); + for Writeback_Image of Writebacks loop + Append_Line + (Buffer, + Apply_Shared_Replacements_To_Image + (FT.To_String (Writeback_Image), + Statement_Rendered.Replacements) + & ";", + Depth + 1); + end loop; + Append_Line (Buffer, "end;", Depth); + end; end Emit_Call_Statement; procedure Render_Statements @@ -3455,7 +3866,8 @@ package body Safe_Frontend.Ada_Emit.Statements is if State.Task_Body_Depth > 0 then Append_Task_Assignment_Warning_Suppression (Buffer, Depth); end if; - Append_Assignment (Buffer, Unit, Document, State, Item.all, Depth, In_Loop); + Append_Assignment + (Buffer, Unit, Document, State, Item.all, Index, Depth, In_Loop); if In_Loop then Append_Integer_Loop_Invariant (Buffer, Unit, Document, State, Item.Target, Depth); @@ -3467,17 +3879,37 @@ package body Safe_Frontend.Ada_Emit.Statements is end if; when CM.Stmt_Call => if Is_Print_Call (Item.Call) then - State.Needs_Safe_IO := True; - Append_Line - (Buffer, - "IO.Put_Line (" - & Render_Print_Argument - (Unit, - Document, - Item.Call.Args (Item.Call.Args.First_Index), - State) - & ");", - Depth); + declare + Print_Image : constant String := + "IO.Put_Line (" + & Render_Print_Argument + (Unit, + Document, + Item.Call.Args (Item.Call.Args.First_Index), + State) + & ")"; + begin + State.Needs_Safe_IO := True; + -- Validate before rendering the shared statement. The + -- render helper intentionally recollects snapshots so + -- all callers share the same pruning path. + Require_Shared_Replacements + (Unit, + Document, + Item.Call.Args (Item.Call.Args.First_Index), + Index, + Print_Image, + "print argument"); + Append_Shared_Rendered_Statement + (Buffer, + Render_Shared_Condition_From_Image + (Unit, + Document, + Item.Call.Args (Item.Call.Args.First_Index), + Index, + Print_Image), + Depth); + end; else Emit_Call_Statement (Buffer, Unit, Document, Item.Call, Index, State, Depth); @@ -8220,13 +8652,14 @@ package body Safe_Frontend.Ada_Emit.Statements is end Render_Discrete_Range; procedure Append_Assignment - (Buffer : in out SU.Unbounded_String; - Unit : CM.Resolved_Unit; - Document : GM.Mir_Document; - State : in out Emit_State; - Stmt : CM.Statement; - Depth : Natural; - In_Loop : Boolean := False) + (Buffer : in out SU.Unbounded_String; + Unit : CM.Resolved_Unit; + Document : GM.Mir_Document; + State : in out Emit_State; + Stmt : CM.Statement; + Statement_Index : Positive; + Depth : Natural; + In_Loop : Boolean := False) is Target_Type : constant String := FT.To_String (Stmt.Target.Type_Name); Target_Info : constant GM.Type_Descriptor := @@ -8282,6 +8715,35 @@ package body Safe_Frontend.Ada_Emit.Statements is return ""; end Static_Integer_Assignment_Image; + + function Render_Shared_Value_From_Image + (Base_Image : String; + Source_Expr : CM.Expr_Access := Stmt.Value) return Shared_Condition_Render + is + begin + return + Render_Shared_Condition_From_Image + (Unit, + Document, + Source_Expr, + Statement_Index, + Base_Image); + end Render_Shared_Value_From_Image; + + procedure Require_Shared_Value_Replacements + (Base_Image : String; + Context : String; + Source_Expr : CM.Expr_Access := Stmt.Value) + is + begin + Require_Shared_Replacements + (Unit, + Document, + Source_Expr, + Statement_Index, + Base_Image, + Context); + end Require_Shared_Value_Replacements; begin if Suppress_Target_Static_Binding then -- Loop bodies are emitted once and reused at runtime, so do not @@ -8423,43 +8885,98 @@ package body Safe_Frontend.Ada_Emit.Statements is elsif Stmt.Target.Kind = CM.Expr_Ident and then Is_Wide_Name (State, FT.To_String (Stmt.Target.Name)) then - if FT.Lowercase (Target_Type) /= "integer" then - Append_Line - (Buffer, - "pragma Assert (" - & Render_Wide_Expr (Unit, Document, Stmt.Value, State) - & " >= Safe_Runtime.Wide_Integer (" - & Target_Type - & "'First) and then " - & Render_Wide_Expr (Unit, Document, Stmt.Value, State) - & " <= Safe_Runtime.Wide_Integer (" - & Target_Type - & "'Last));", - Depth); - end if; - Append_Line - (Buffer, - Target_Image & " := " & Render_Wide_Expr (Unit, Document, Stmt.Value, State) & ";", - Depth); - if FT.Lowercase (Target_Type) /= "integer" then - Append_Line - (Buffer, - "pragma Assert (" - & Target_Image - & " >= Safe_Runtime.Wide_Integer (" - & Target_Type - & "'First) and then " - & Target_Image - & " <= Safe_Runtime.Wide_Integer (" - & Target_Type - & "'Last));", - Depth); - end if; + declare + Base_Image : constant String := + Render_Wide_Expr (Unit, Document, Stmt.Value, State); + begin + Require_Shared_Value_Replacements (Base_Image, "wide assignment"); + declare + Rendered : constant Shared_Condition_Render := + Render_Shared_Value_From_Image (Base_Image); + Line_Depth : constant Natural := + (if Rendered.Snapshots.Is_Empty then Depth else Depth + 1); + begin + if not Rendered.Snapshots.Is_Empty then + Append_Line (Buffer, "declare", Depth); + Append_Shared_Condition_Declarations + (Buffer, Rendered, Depth + 1); + Append_Line (Buffer, "begin", Depth); + end if; + + if FT.Lowercase (Target_Type) /= "integer" then + Append_Line + (Buffer, + "pragma Assert (" + & FT.To_String (Rendered.Image) + & " >= Safe_Runtime.Wide_Integer (" + & Target_Type + & "'First) and then " + & FT.To_String (Rendered.Image) + & " <= Safe_Runtime.Wide_Integer (" + & Target_Type + & "'Last));", + Line_Depth); + end if; + Append_Line + (Buffer, + Target_Image & " := " & FT.To_String (Rendered.Image) & ";", + Line_Depth); + if FT.Lowercase (Target_Type) /= "integer" then + Append_Line + (Buffer, + "pragma Assert (" + & Target_Image + & " >= Safe_Runtime.Wide_Integer (" + & Target_Type + & "'First) and then " + & Target_Image + & " <= Safe_Runtime.Wide_Integer (" + & Target_Type + & "'Last));", + Line_Depth); + end if; + + if not Rendered.Snapshots.Is_Empty then + Append_Line (Buffer, "end;", Depth); + end if; + end; + end; elsif Is_Wide_Integer_Type (Unit, Document, Target_Type) and then Uses_Wide_Value (Unit, Document, State, Stmt.Value) then - Append_Narrowing_Assignment - (Buffer, Unit, Document, State, Stmt.Target, Stmt.Value, Depth); + declare + Base_Image : constant String := + Render_Wide_Expr (Unit, Document, Stmt.Value, State); + begin + Require_Shared_Value_Replacements (Base_Image, "wide narrowing assignment"); + declare + Rendered : constant Shared_Condition_Render := + Render_Shared_Value_From_Image (Base_Image); + Line_Depth : constant Natural := + (if Rendered.Snapshots.Is_Empty then Depth else Depth + 1); + begin + if not Rendered.Snapshots.Is_Empty then + Append_Line (Buffer, "declare", Depth); + Append_Shared_Condition_Declarations + (Buffer, Rendered, Depth + 1); + Append_Line (Buffer, "begin", Depth); + end if; + + Append_Narrowing_Assignment + (Buffer, + Unit, + Document, + State, + Stmt.Target, + Stmt.Value, + Line_Depth, + Rendered_Value_Image => FT.To_String (Rendered.Image)); + + if not Rendered.Snapshots.Is_Empty then + Append_Line (Buffer, "end;", Depth); + end if; + end; + end; else declare Condition_Image : FT.UString; @@ -8476,39 +8993,160 @@ package body Safe_Frontend.Ada_Emit.Statements is Lower_Image, Upper_Image) then - Append_Line - (Buffer, - "if " & FT.To_String (Condition_Image) & " then", - Depth); - Append_Line - (Buffer, - Target_Image & " := " & FT.To_String (Lower_Image) & ";", - Depth + 1); - Append_Line (Buffer, "else", Depth); - Append_Line - (Buffer, - Target_Image & " := " & FT.To_String (Upper_Image) & ";", - Depth + 1); - Append_Line (Buffer, "end if;", Depth); + declare + Combined_Image : constant String := + -- This concatenation is only a membership test for + -- complete shared getter call substrings. Getter call + -- images are generated Ada call/selected-name fragments, + -- so the separator spaces cannot create a cross-image + -- replacement match. + FT.To_String (Condition_Image) + & " " + & FT.To_String (Lower_Image) + & " " + & FT.To_String (Upper_Image); + Rendered : constant Shared_Condition_Render := + -- The stable interpolation images are rendered only from + -- subexpressions reachable through Stmt.Value, so walking + -- the whole RHS captures every shared getter eligible for + -- replacement in the generated condition/lower/upper text. + Render_Shared_Value_From_Image (Combined_Image); + Rewritten_Condition : SU.Unbounded_String := + SU.To_Unbounded_String (FT.To_String (Condition_Image)); + Rewritten_Lower : SU.Unbounded_String := + SU.To_Unbounded_String (FT.To_String (Lower_Image)); + Rewritten_Upper : SU.Unbounded_String := + SU.To_Unbounded_String (FT.To_String (Upper_Image)); + Line_Depth : constant Natural := + (if Rendered.Snapshots.Is_Empty then Depth else Depth + 1); + begin + Require_Shared_Value_Replacements + (Combined_Image, "stable float interpolation"); + + Rewritten_Condition := + SU.To_Unbounded_String + (Apply_Shared_Replacements_To_Image + (SU.To_String (Rewritten_Condition), + Rendered.Replacements)); + Rewritten_Lower := + SU.To_Unbounded_String + (Apply_Shared_Replacements_To_Image + (SU.To_String (Rewritten_Lower), + Rendered.Replacements)); + Rewritten_Upper := + SU.To_Unbounded_String + (Apply_Shared_Replacements_To_Image + (SU.To_String (Rewritten_Upper), + Rendered.Replacements)); + + if not Rendered.Snapshots.Is_Empty then + Append_Line (Buffer, "declare", Depth); + Append_Shared_Condition_Declarations + (Buffer, Rendered, Depth + 1); + Append_Line (Buffer, "begin", Depth); + end if; + + Append_Line + (Buffer, + "if " & SU.To_String (Rewritten_Condition) & " then", + Line_Depth); + Append_Line + (Buffer, + Target_Image + & " := " + & SU.To_String (Rewritten_Lower) + & ";", + Line_Depth + 1); + Append_Line (Buffer, "else", Line_Depth); + Append_Line + (Buffer, + Target_Image + & " := " + & SU.To_String (Rewritten_Upper) + & ";", + Line_Depth + 1); + Append_Line (Buffer, "end if;", Line_Depth); + + if not Rendered.Snapshots.Is_Empty then + Append_Line (Buffer, "end;", Depth); + end if; + end; elsif Is_Explicit_Float_Narrowing (Unit, Document, Target_Type, Stmt.Value) then - Append_Float_Narrowing_Assignment - (Buffer, - Unit => Unit, - Document => Document, - Target_Type => Target_Type, - Target_Image => Target_Image, - Inner_Image => Render_Expr (Unit, Document, Stmt.Value.Inner, State), - Depth => Depth); + declare + Base_Image : constant String := + Render_Expr (Unit, Document, Stmt.Value.Inner, State); + begin + Require_Shared_Value_Replacements + (Base_Image, + "float narrowing assignment", + Source_Expr => Stmt.Value.Inner); + declare + Rendered : constant Shared_Condition_Render := + Render_Shared_Value_From_Image + (Base_Image, + Source_Expr => Stmt.Value.Inner); + Line_Depth : constant Natural := + (if Rendered.Snapshots.Is_Empty then Depth else Depth + 1); + begin + if not Rendered.Snapshots.Is_Empty then + Append_Line (Buffer, "declare", Depth); + Append_Shared_Condition_Declarations + (Buffer, Rendered, Depth + 1); + Append_Line (Buffer, "begin", Depth); + end if; + + Append_Float_Narrowing_Assignment + (Buffer, + Unit => Unit, + Document => Document, + Target_Type => Target_Type, + Target_Image => Target_Image, + Inner_Image => FT.To_String (Rendered.Image), + Depth => Line_Depth); + + if not Rendered.Snapshots.Is_Empty then + Append_Line (Buffer, "end;", Depth); + end if; + end; + end; else - Append_Line - (Buffer, - Target_Image - & " := " - & (if Static_Integer_Assignment_Image'Length > 0 - then Static_Integer_Assignment_Image - else Value_Image) - & ";", - Depth); + declare + Static_Image : constant String := + Static_Integer_Assignment_Image; + Base_Image : constant String := + (if Static_Image'Length > 0 + then Static_Image + else Value_Image); + begin + Require_Shared_Value_Replacements (Base_Image, "assignment value"); + declare + Rendered : constant Shared_Condition_Render := + Render_Shared_Value_From_Image (Base_Image); + begin + if Rendered.Snapshots.Is_Empty then + Append_Line + (Buffer, + Target_Image + & " := " + & FT.To_String (Rendered.Image) + & ";", + Depth); + else + Append_Line (Buffer, "declare", Depth); + Append_Shared_Condition_Declarations + (Buffer, Rendered, Depth + 1); + Append_Line (Buffer, "begin", Depth); + Append_Line + (Buffer, + Target_Image + & " := " + & FT.To_String (Rendered.Image) + & ";", + Depth + 1); + Append_Line (Buffer, "end;", Depth); + end if; + end; + end; end if; end; end if; @@ -9444,7 +10082,8 @@ package body Safe_Frontend.Ada_Emit.Statements is State : in out Emit_State; Target : CM.Expr_Access; Value : CM.Expr_Access; - Depth : Natural) + Depth : Natural; + Rendered_Value_Image : String := "") is Target_Name : constant String := FT.To_String (Target.Type_Name); Target_Info : constant GM.Type_Descriptor := @@ -9452,7 +10091,10 @@ package body Safe_Frontend.Ada_Emit.Statements is Target_Subtype : constant String := Render_Subtype_Indication (Unit, Document, Target_Info); Target_Image : constant String := Render_Expr (Unit, Document, Target, State); - Wide_Image : constant String := Render_Wide_Expr (Unit, Document, Value, State); + Wide_Image : constant String := + (if Rendered_Value_Image'Length > 0 + then Rendered_Value_Image + else Render_Wide_Expr (Unit, Document, Value, State)); begin Append_Line (Buffer, diff --git a/compiler_impl/stdlib/ada/safe_array_identity_rt.ads b/compiler_impl/stdlib/ada/safe_array_identity_rt.ads index 7e406b45..7d9aeb9a 100644 --- a/compiler_impl/stdlib/ada/safe_array_identity_rt.ads +++ b/compiler_impl/stdlib/ada/safe_array_identity_rt.ads @@ -60,6 +60,7 @@ is Item : Element_Type) with Global => null, Pre => Index <= Length (Value), + Always_Terminates, Post => Length (Value) = Length (Value'Old) and then Element (Value, Index) = Item diff --git a/compiler_impl/stdlib/ada/safe_array_rt.ads b/compiler_impl/stdlib/ada/safe_array_rt.ads index 0934007b..6bb7d9e3 100644 --- a/compiler_impl/stdlib/ada/safe_array_rt.ads +++ b/compiler_impl/stdlib/ada/safe_array_rt.ads @@ -44,6 +44,7 @@ package Safe_Array_RT is Item : Element_Type) with Global => null, Pre => Index <= Length (Value), + Always_Terminates, Post => Length (Value) = Length (Value'Old) and then Element (Value, Index) = Item diff --git a/docs/emitted_output_verification_matrix.md b/docs/emitted_output_verification_matrix.md index dcd42e9a..3f27bc2f 100644 --- a/docs/emitted_output_verification_matrix.md +++ b/docs/emitted_output_verification_matrix.md @@ -109,6 +109,7 @@ subset remain outside the current surface; see | Multiple independent accumulator proof-expansion surface | `tests/build/pr1123e_multi_accumulator_build.safe` | PR11.23e emits independent fail-closed loop invariants for multiple integer accumulators in a growable `for of` body. PR11.23f intentionally extends this fixture with the sum/count relational invariant because it contains both `count = count + 1` and `sum = sum + item`. The fixture also covers an intentionally skipped non-additive `max_seen = item` update. | yes | yes | yes | yes | yes | none | no | | Scoped sum/count relational proof-expansion surface | `tests/build/pr1123f_sum_count_relational_build.safe`, `tests/negative/neg_pr1123f_unguarded_sum_count.safe` | PR11.23f emits fail-closed relational invariants for the guarded average pattern: one exact top-level `count = count + 1` counter, no recursive writes or shadowing, and one distinct bounded nonnegative sum accumulator. The positive fixture proves a bounded `sum / count` conversion under an explicit `count > 0` guard; the negative fixture pins unguarded post-loop `sum / count` as a clean frontend rejection pending #321. | yes | yes | yes | yes | yes | Unguarded post-loop nonzero inference remains tracked as #321. | no | | Fixed-depth nested iteration proof-expansion surface | `tests/build/pr1123g_nested_iteration_build.safe` | PR11.23g emits fail-closed composed accumulator invariants for the fixed two-level nested `for of` shape where the inner iterable is a literal-backed local growable collection with a known static length and the inner update has a bounded nonnegative product delta. The fixture proves `total = total + x * y` across local literal-backed `xs` and `ys` lists at level 2, and pins that an unrelated inner loop does not suppress an outer accumulator invariant. The supporting progress conjunct is intentionally shared by all growable accumulator invariants, so adjacent proof-expansion fixtures such as `pr213_map_entry_build.safe`, `pr1123e_multi_accumulator_build.safe`, and `pr1123f_sum_count_relational_build.safe` also receive emitted-Ada snapshot churn. Dynamic inner lengths, arbitrary-depth nesting, and type-capacity inference remain out of scope. | yes | yes | yes | yes | yes | none | no | +| Shared call-argument snapshot proof-expansion surface | `tests/build/pr1123h_shared_call_argument_snapshot_build.safe` | PR11.23h generalizes the existing shared-condition snapshot replacement pass into assignment RHS and standalone call-argument contexts. The fixture pins the original compound-condition #287 shape, then proves flat and nested shared getter reads passed through function call arguments and `print` without exposing volatile getter calls to GNATprove's interfering-context checks. The existing one-snapshot-per-shared-root discipline is preserved, so multiple field reads from the same shared object use one whole-root snapshot local per statement. | yes | yes | yes | yes | yes | none | no | | Built-in container checkpoint surface | `tests/positive/pr1110a_optional_guarded.safe`, `tests/positive/pr1110b_list_basics.safe`, `tests/positive/pr1110c_map_basics.safe`, plus the build-backed `pr1110a*`, `pr1110b*`, and `pr1110c*` fixtures in `scripts/_lib/proof_inventory.py` | PR11.10a/PR11.10b/PR11.10c close the shipped optional/list/map surface under blocking emitted proof manifests, and PR11.10d ratifies that union as the parent container checkpoint. `tests/build/pr1110b_list_empty_build.safe` and `tests/build/pr213_map_entry_build.safe` now both prove through the emitted lane; PR11.22h.1 closes the former runtime-only container proof gaps, and PR11.23c reclassifies `pr213_map_entry_build.safe` as the conditional static-delta accumulator proof-expansion checkpoint for #279. | yes | yes | yes | yes | yes | none | no | | Shared-wrapper checkpoint surface | `tests/positive/pr1112a_shared_field_access.safe`, `tests/positive/pr1112b_shared_snapshot.safe`, plus the build-backed `pr1112c*`, `pr1112d*`, `pr1112e*`, and `pr1112f*` fixtures in `scripts/_lib/proof_inventory.py` and `tests/interfaces/provider_shared_ceiling.safe` | PR11.12a through PR11.12f close the shipped shared-wrapper surface under blocking emitted proof manifests, and PR11.12g ratifies that union as the parent shared checkpoint. The current shared family carries no named proof exclusions, so the parent checkpoint closes with zero unnamed coverage holes and zero shared-specific exclusion debt. | yes | yes | yes | yes | yes | none | no | | Sum-type checkpoint surface | `tests/positive/pr1113a_sum_construction.safe`, `tests/positive/pr1113b_sum_match.safe`, plus the build-backed `pr1113c*` fixtures in `scripts/_lib/proof_inventory.py` | PR11.13a, PR11.13b, and PR11.13c close the shipped sum-type surface under blocking emitted proof manifests. The parent `PR11.13 checkpoint` ratifies same-unit and imported constructor/match behavior, including heap-backed imported payloads and overlapping imported variant names resolved by scrutinee type. | yes | yes | yes | yes | yes | none | no | diff --git a/docs/roadmap.md b/docs/roadmap.md index bc1e15da..0250dca9 100644 --- a/docs/roadmap.md +++ b/docs/roadmap.md @@ -3474,6 +3474,21 @@ accumulator invariants. Snapshot churn in adjacent fixtures such as `pr1123f_sum_count_relational_build.safe` is therefore expected and should be checked when refactoring this helper. +### PR11.23h Note + +PR11.23h implements #287 by reusing the shared-condition snapshot collector for +assignment RHS and standalone call-argument contexts. The condition path was +already covered by the PR11.22h.1 shared-condition fixtures; this slice pins the +original compound-condition shape and adds flat plus nested call-argument +coverage in `tests/build/pr1123h_shared_call_argument_snapshot_build.safe`. +Snapshotting remains scoped to statement contexts with a clear declaration +insertion point and preserves one whole-root snapshot per shared object per +statement. The generalized assignment/call pass intentionally refreshes emitted +hashes for adjacent shared-wrapper fixtures that contain shared reads in +assignments or `print` calls, including `pr1112a_shared_task_build.safe`, +`pr1112e_imported_shared_record_build.safe`, `pr1112a_shared_field_access.safe`, +and `pr1112b_shared_snapshot.safe`. + --- ## PR11.23j: Post-Sprint Emitter Analysis Hardening diff --git a/scripts/_lib/proof_inventory.py b/scripts/_lib/proof_inventory.py index 5cdc7948..62432142 100644 --- a/scripts/_lib/proof_inventory.py +++ b/scripts/_lib/proof_inventory.py @@ -376,6 +376,7 @@ class EmittedProofExclusion: "tests/build/pr1123e_multi_accumulator_build.safe", "tests/build/pr1123f_sum_count_relational_build.safe", "tests/build/pr1123g_nested_iteration_build.safe", + "tests/build/pr1123h_shared_call_argument_snapshot_build.safe", ] diff --git a/tests/build/pr1123h_shared_call_argument_snapshot_build.safe b/tests/build/pr1123h_shared_call_argument_snapshot_build.safe new file mode 100644 index 00000000..103374d1 --- /dev/null +++ b/tests/build/pr1123h_shared_call_argument_snapshot_build.safe @@ -0,0 +1,69 @@ +package pr1123h_shared_call_argument_snapshot_build + + subtype slot_index is integer (1 to 3); + subtype small_value is integer (0 to 40); + type int_list is array of small_value; + + type sensor is record + temperature : integer; + active : boolean; + label : string (5); + slot : slot_index; + + shared probe : sensor = (temperature = 0, active = false, label = "idle-", slot = 1); + + condition_result : integer = 0; + flat_result : integer = 0; + nested_result : integer = 0; + blended : long_float = 0.0; + values : int_list = [10, 20, 30]; + + function is_hot (temperature : integer) returns boolean + return temperature > 0 + + function choose (hot : boolean; on : boolean) returns integer + if hot and then on + return 1 + return 0 + + function echo_label (value : string (5)) returns string (5) + return value + + function bump (item : mut small_value) + if item < 40 + item = item + 1; + + function touch_if_hot (item : mut small_value; temperature : integer) + if temperature > 0 + item = item; + + probe.temperature = 72; + probe.active = true; + probe.label = "ready"; + probe.slot = 2; + + -- Original #287 condition shape: already supported, pinned here. + if probe.temperature > 0 and then probe.active + condition_result = 1; + if blended == 0.0 + condition_result = condition_result + 1; + + -- PR11.23h extends snapshots into call arguments and nested calls. + flat_result = choose (probe.temperature > 0, probe.active); + nested_result = choose (is_hot (probe.temperature), probe.active); + -- Stable float interpolation emits an if block from rendered subimages; + -- shared reads in those subimages must be snapshot-localized too. + blended = long_float (probe.temperature) + long_float (probe.slot) * (long_float (probe.slot) - long_float (probe.temperature)); + if blended > 0.0 + condition_result = condition_result + 1; + + print (choose (is_hot (probe.temperature), probe.active)); + print (echo_label (probe.label)); + print (condition_result); + print (flat_result); + print (nested_result); + + -- Copy-back temp initialization/writeback also need snapshots. + bump (values (probe.slot)); + touch_if_hot (values (probe.slot), probe.temperature); + print (values (2)) diff --git a/tests/emitted_ada_snapshot.json b/tests/emitted_ada_snapshot.json index 0957746d..ef435693 100644 --- a/tests/emitted_ada_snapshot.json +++ b/tests/emitted_ada_snapshot.json @@ -1,5 +1,5 @@ { - "compiler_hash": "026cda1ff9e8b4fc30561b0dc55254341fb8e2b1cf9c75475f5f99be05f84c48", + "compiler_hash": "8062614695eac2186805b6fe320fb0341b0e373d07c375c5843b08ac6d4332c3", "fixtures": { "tests/build/pr1110a_optional_growable_build.safe": { "pr1110a_optional_growable_build.adb": "edea57f7f04c1890732b861d79740c6b86dbea49247d4148e722aaf4c447f102", @@ -104,9 +104,9 @@ "pr1111c_provider_collision_right_line_map.json": "49180721ecd03bc59d854871e47838e9e276329ad607280dd02e5100262583a9" }, "tests/build/pr1112a_shared_task_build.safe": { - "pr1112a_shared_task_build.adb": "3cff2b435cf28d9e5cf116932624c11275fa5118cd98637735d6cf5712a75395", + "pr1112a_shared_task_build.adb": "15c2bbf3bae591a52bec31e64cadd8e92d0ae0b53fcc336ff11c3f76def1b1b1", "pr1112a_shared_task_build.ads": "ed4c327d0d3fc83a99a46bcf89bde0b066cf4df398d8795709cd7d8049d72cb7", - "pr1112a_shared_task_build_line_map.json": "e88692a6785298d53b744c7dbb8284e0f326efe5fdbfd2fcd99f79de2fb26eaf" + "pr1112a_shared_task_build_line_map.json": "6681d4411c7ce3ae1774bfe0b82965b65f3dd38b531396f59ab64a5784fd035c" }, "tests/build/pr1112b_shared_update_build.safe": { "pr1112b_shared_update_build.adb": "f82a5fceb2dbf1c02ce22501ff2c61c2721ae9fa530b1d48c115c77783e44fb7", @@ -139,9 +139,9 @@ "pr1112d_shared_list_root_build_line_map.json": "a271d6e11ad6e13b21cc59137d26aa4ef1f5247f81d3e7986646648c7f4f42ae" }, "tests/build/pr1112d_shared_map_indexed_remove_build.safe": { - "pr1112d_shared_map_indexed_remove_build.adb": "05b8d84da29dad7e507b93a31395f631bdafe4c9b2cada1abae43596117567de", + "pr1112d_shared_map_indexed_remove_build.adb": "e8b55d2129fd53b46a51e80e8e260262ea7759a2abf6df38390a143d9576536a", "pr1112d_shared_map_indexed_remove_build.ads": "3c8ca345ddc7b4609adf7f1eae567b1ab1e8b2a4e633a2736754a2fda2e26b9b", - "pr1112d_shared_map_indexed_remove_build_line_map.json": "1286922ec6c05ae1f5a5055916d6a0e8f81743ef1a62c2a76155b4e286103b80" + "pr1112d_shared_map_indexed_remove_build_line_map.json": "37f5c8ab726ff316a19657b38e79f2cacae69a572763693d0dc1f7d8d55efced" }, "tests/build/pr1112d_shared_map_root_build.safe": { "pr1112d_shared_map_root_build.adb": "0bcee77d0b7d79d25aa19dac1a259d329847fbcf64cc3911a7123d3c2ae66d57", @@ -165,9 +165,9 @@ "pr1112e_provider_shared_map_line_map.json": "b65f10e43e0989576e2fabd0b127888cf381dca248fe5bc3e09fb296cfdc6864" }, "tests/build/pr1112e_imported_shared_record_build.safe": { - "pr1112e_imported_shared_record_build.adb": "937a2324ad1ebfaae0f15dc36691490668ae91b8e67b8554c76efbcb8af6978f", + "pr1112e_imported_shared_record_build.adb": "1e8ad26eb5981c1a5ba8f5c79daed1b0fa80329d8c1510b780f45ff451d8b61a", "pr1112e_imported_shared_record_build.ads": "8b184d315efb51a593eca3f5248cd311f75eb1808ce0b78adfa1d181070bfa39", - "pr1112e_imported_shared_record_build_line_map.json": "6fdaa51ea22a828882df3176eab0242ac0b73d7120e6982b0ad8de8ecea2d2be", + "pr1112e_imported_shared_record_build_line_map.json": "93895ca150b9a0674114d3fffbd39c00468c0fdbb65859aac480a8bc9800b836", "pr1112e_provider_shared_record.adb": "6bc78c1eaf43077609ce21ee920b179ccc99bc45deb837accfc97a666659a427", "pr1112e_provider_shared_record.ads": "59603312f15ded5e528134f3db75e9af0c2f863d02e8e836ab636a09bccd529d", "pr1112e_provider_shared_record_line_map.json": "603577aa15364a2c4fc4fac600e81e49cc16e3e4319f7636149abf4b86dd64e2" @@ -317,6 +317,11 @@ "pr1123g_nested_iteration_build.ads": "e03683786f0da559f74ce959736ca31144365595633029aad1fc17c5a9e3deaa", "pr1123g_nested_iteration_build_line_map.json": "3ba5542d365c9758d308267a724c3eb549286d6485bf79812b236e26700ac0a5" }, + "tests/build/pr1123h_shared_call_argument_snapshot_build.safe": { + "pr1123h_shared_call_argument_snapshot_build.adb": "f9df08dc8f36470e79ffd6d442bac8a62ed89f34bbf1f1a380ec2bd71a7cb848", + "pr1123h_shared_call_argument_snapshot_build.ads": "eca3b48efb0b4c6d9c679fc6e928f855327143234337fdc21ddf62a589af6d04", + "pr1123h_shared_call_argument_snapshot_build_line_map.json": "8bb91b900e0fe7a1ecb2eb1f76dcd46611898002b7ce3f93463d9d5d8c2e50c9" + }, "tests/build/pr118c2_entry_build.safe": { "main.adb": "50641acff6114f530b052e2addbe1a8ad1b3ec3e57b8ba07ff78c9fa27e40289", "pr118c2_entry_build.adb": "4d5a032db25ec5d26466735b493402f5a182a8b3a5bd9cf6d26aefbbbb3437f8", @@ -847,7 +852,7 @@ "pr1110a_optional_guarded_line_map.json": "de1466e405855907774342eae9fd706cd2bafa875f2088b51dd6a495241a801d" }, "tests/positive/pr1110b_disjoint_mut_indices.safe": { - "pr1110b_disjoint_mut_indices.adb": "41672370ba5256994c01630a0563602473fc317d6a42016a883b393802156076", + "pr1110b_disjoint_mut_indices.adb": "a80eada7bdac9cbb61742cc9ea6d60c4fed0a56a1e8e31543ebcce7bd7b8cbdb", "pr1110b_disjoint_mut_indices.ads": "a8338289473eea15e57428808f495483fb83f320012bea41d135d0bc7e59c8e0", "pr1110b_disjoint_mut_indices_line_map.json": "2f7ccf72165ddc55654ea592d0bbf63a7de999d6f514e4d3bad836748efc3423" }, @@ -887,14 +892,14 @@ "pr1111c_generic_constraint_line_map.json": "cddb4f8bb9467048bff595807b0a505030f928cef3748189e422298edc3a5336" }, "tests/positive/pr1112a_shared_field_access.safe": { - "pr1112a_shared_field_access.adb": "f1ba1bd19584c3e8828054a0a1a6df671842ff526d5fb6c41509faed42d2bfcb", + "pr1112a_shared_field_access.adb": "7ea2cc62a669e21a3d3128d79d6e8a819628f709afe7ed2d4e02b7560716e954", "pr1112a_shared_field_access.ads": "e3bb9ecc0617a890ba43664e4e7d9b1508a6c58419c9f3d62b5d535143a81851", - "pr1112a_shared_field_access_line_map.json": "1815dd67948babd6656aaec3c49a2639d4d3aeee861513d7a51081db4cdb88c3" + "pr1112a_shared_field_access_line_map.json": "6417f967e2a5c0b1479f656c399d7cfefdc140d1928d6dbbfd22546c1f3b2f26" }, "tests/positive/pr1112b_shared_snapshot.safe": { - "pr1112b_shared_snapshot.adb": "b0065b53e0b0f615959115ae6962c58ef7e84c3d5d9c449930d2b8356b4d4ce1", + "pr1112b_shared_snapshot.adb": "e9d992c38933cc86e5ad044d46c0dc71052c9b7db405b3323ac346e90bb5b5ba", "pr1112b_shared_snapshot.ads": "62e27e30b914b93ce95827369ef22fd57e7953ed0961a7da12a8ea81bed88500", - "pr1112b_shared_snapshot_line_map.json": "4374186c00395e5321a043988a64f1a5639017ccc98f72c9384f3213645f62fa" + "pr1112b_shared_snapshot_line_map.json": "42f3c71717c73cba3802fb4b4b39468397e67f6fa0d1f7c64ac6f25a4754fa06" }, "tests/positive/pr1113a_sum_construction.safe": { "pr1113a_sum_construction.adb": "06ef559f7e17551d9eefb6d9b52814e8dbdbdf3ec04a51215b65a98de195428a",