diff --git a/Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean b/Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean index 6c1189a73..796b5d737 100644 --- a/Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean +++ b/Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean @@ -455,9 +455,10 @@ public def inlineCoreFixpoint (program : Core.Program) /-- Type-check a Core program using the standard context and factory. Returns the type-checked program and the resulting type environment. -/ public def typeCheckCore (program : Core.Program) + (factory : @Lambda.Factory Core.CoreLParams := Core.Factory) : Except String (Core.Program × Core.Expression.TyEnv) := do let Ctx := { Lambda.LContext.default with - functions := Core.Factory, knownTypes := Core.KnownTypes } + functions := factory, knownTypes := Core.KnownTypes } let Env := Lambda.TEnv.default match Core.Program.typeCheck Ctx Env program with | .ok (tcPgm, Env') => return (tcPgm, Env') @@ -514,11 +515,12 @@ public def inlineCoreToGotoFiles (program : Core.Program) (baseName : String) (sourceText : Option String := none) (entryPoints : List String := ["main", "__main__"]) + (factory : @Lambda.Factory Core.CoreLParams := Core.Factory) : EIO String Unit := do let inlined ← match inlineCoreFixpoint program with | .ok r => pure r | .error msg => throw msg - let (tcPgm, Env) ← match typeCheckCore inlined with + let (tcPgm, Env) ← match typeCheckCore inlined factory with | .ok r => pure r | .error msg => throw msg coreToGotoFiles tcPgm Env baseName sourceText entryPoints diff --git a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean index 3b138729c..d5ff33200 100644 --- a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean +++ b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean @@ -93,6 +93,7 @@ partial def translateHighType (arg : Arg) : TransM HighTypeMd := do | q`Laurel.float64Type, _ => return mkHighTypeMd .TFloat64 md | q`Laurel.realType, _ => return mkHighTypeMd .TReal md | q`Laurel.stringType, _ => return mkHighTypeMd .TString md + | q`Laurel.regexType, _ => return mkHighTypeMd (.TCore "regex") md | q`Laurel.mapType, #[keyArg, valArg] => let keyType ← translateHighType keyArg let valType ← translateHighType valArg diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean index 5bb1669a1..1ed8e7a0c 100644 --- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean +++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean @@ -8,7 +8,7 @@ module -- Laurel dialect definition, loaded from LaurelGrammar.st -- NOTE: Changes to LaurelGrammar.st are not automatically tracked by the build system. -- Update this file (e.g. this comment) to trigger a recompile after modifying LaurelGrammar.st. --- Last grammar change: added exit and labelledBlock ops for break/continue support. +-- Last grammar change: added regexType op public import Strata.DDM.Integration.Lean public meta import Strata.DDM.Integration.Lean diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st index 0e1b7ccf4..8f944e4af 100644 --- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st +++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st @@ -9,6 +9,7 @@ op boolType : LaurelType => "bool"; op realType : LaurelType => "real"; op float64Type : LaurelType => "float64"; op stringType : LaurelType => "string"; +op regexType : LaurelType => "regex"; op mapType (keyType: LaurelType, valueType: LaurelType): LaurelType => "Map " keyType " " valueType; op compositeType (name: Ident): LaurelType => name; diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index 125fac35f..bcd2aab48 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -56,7 +56,6 @@ def translateType (model : SemanticModel) (ty : HighTypeMd) : LMonoTy := | .TSet elementType => Core.mapTy (translateType model elementType) LMonoTy.bool | .TMap keyType valueType => Core.mapTy (translateType model keyType) (translateType model valueType) | .UserDefined name => - -- Composite types map to "Composite"; datatypes map to their own name match name.uniqueId.bind model.refToDef.get? with | some (.compositeType _) => .tcons "Composite" [] | some (.datatypeDefinition dt) => .tcons dt.name.text [] diff --git a/Strata/Languages/Python/PyFactory.lean b/Strata/Languages/Python/PyFactory.lean index 814b779ba..0c83beb4e 100644 --- a/Strata/Languages/Python/PyFactory.lean +++ b/Strata/Languages/Python/PyFactory.lean @@ -16,92 +16,111 @@ public section ------------------------------------------------------------------------------- /- -Candidate translation pass for Python `re` code: - -## Python Code: - -``` -... -PATTERN = r"^[a-z0-9][a-z0-9.-]{1,3}[a-z0-9]$" -REGEX = re.compile(PATTERN) # default flags == 0 -... -if not re.match(REGEX, name) then # default flags == 0 - return False -... -``` - -## Corresponding Strata.Core: - -``` -procedure _main () { - -var PATTERN : string = "^[a-z0-9][a-z0-9.-]{1,3}[a-z0-9]$"; - -var REGEX : regex; -var $__REGEX : Except Error regex := PyReCompile(PATTERN, 0) - -if ExceptErrorRegex_isOK($__REGEX) then { - REGEX := ExceptErrorRegex_getOK($__REGEX); -} else if (Error_isUnimplemented(ExceptErrorRegex_getError($__REGEX)) then { - // Unsupported by Strata. - havoc REGEX; -} else { - // - // TODO: Implement a version of `assert` that takes an expression to be - // evaluated when the assertion fails. In this case, we'd display the - // (computed) error message in `ExceptErrorRegex_getError($__REGEX)`. - // - // E.g., `assert false (printOnFailure := ExceptErrorRegex_getError($__REGEX));` - // - assert false; -} -... - -if not PyReMatch(REGEX, name, 0) then - return false -} -``` - +## Python regex verification — factory functions + +These factory functions provide `concreteEval` implementations that call +`pythonRegexToCore` to translate Python regex pattern strings into SMT-LIB +regex expressions at verification time. + +### Architecture + +Python's `re.compile` is a semantic no-op in the Laurel pipeline — it returns +the pattern string unchanged. The actual compilation to SMT-LIB regex happens +at the point of matching (`re.fullmatch`, `re.match`, `re.search`), where the +match mode is known. + +This is important because `pythonRegexToCore` produces *different* regex +expressions depending on the mode -- in particular, it handles anchors (`^`/`$`) +by generating a union of anchor-activation variants with appropriate `.*` +wrapping (see `ReToCore.lean`). Compiling once at `re.compile` time would +require knowing the eventual match mode, which is not available. + +### Factory functions + +Each call to `re.fullmatch(pattern, s)` (and similarly `re.match`/`re.search`) +causes `pythonRegexToCore` to be called twice via `concreteEval`: + +1. **`re_pattern_error(pattern)`** — Parses the pattern and returns + `NoError()` on success or `RePatternError(msg)` for a genuinely malformed + pattern. Unimplemented features return `NoError()` because Python would + succeed at runtime; the mode-specific factory staying uninterpreted provides + a sound over-approximation for those cases. The prelude checks this first + and returns `exception(err)` for pattern errors, modeling Python's + `re.error`. + +2. **`re_fullmatch_str(pattern)`** (or `re_match_str`/`re_search_str`) — + Compiles the pattern with the correct `MatchMode`. Returns the compiled + regex on success, or `.none` on error (leaving the function uninterpreted). + Since pattern errors are already caught by `re_pattern_error`, the `.none` + case here only fires for unimplemented features, producing `unknown` VCs — + a sound over-approximation. + +The double parse is defensible because `pythonRegexToCore` is fast enough -- it +runs at translation time, not solver time, and keeps the factory functions +orthogonal. -/ open Core open Lambda LTy.Syntax LExpr.SyntaxMono -def reCompileFunc : LFunc Core.CoreLParams := - { name := "PyReCompile", +-- Mode-specific regex compilation. Each function compiles a Python regex +-- string with the correct MatchMode so that anchors (^/$) are handled +-- properly. +private def mkModeCompileFunc (name : String) (mode : MatchMode) : + LFunc Core.CoreLParams := + { name := name, + typeArgs := [], + inputs := [("pattern", mty[string])], + output := mty[regex], + concreteEval := some + (fun _ args => match args with + | [LExpr.strConst () s] => + let (expr, maybe_err) := pythonRegexToCore s mode + match maybe_err with + | none => .some expr + | some _ => .none + | _ => .none) + } + +def reFullmatchStrFunc : LFunc Core.CoreLParams := + mkModeCompileFunc "re_fullmatch_str" .fullmatch +def reMatchStrFunc : LFunc Core.CoreLParams := + mkModeCompileFunc "re_match_str" .match +def reSearchStrFunc : LFunc Core.CoreLParams := + mkModeCompileFunc "re_search_str" .search + +def rePatternErrorFunc : LFunc Core.CoreLParams := + { name := "re_pattern_error", typeArgs := [], - inputs := [("string", mty[string]), - ("flags", mty[int])] - output := mty[ExceptErrorRegex], + inputs := [("pattern", mty[string])], + output := mty[Error], concreteEval := some (fun _ args => match args with - | [LExpr.strConst () s, LExpr.intConst () 0] => - -- This function has a concrete evaluation implementation only when - -- flags == 0. - -- (FIXME): We use `.match` mode below because we support only - -- `re.match` for now. However, `re.compile` isn't mode-specific in - -- general. - let (expr, maybe_err) := pythonRegexToCore s .match + | [LExpr.strConst () s] => + let (_, maybe_err) := pythonRegexToCore s .fullmatch -- mode irrelevant: errors come from parseTop before mode-specific compilation match maybe_err with | none => - -- Note: Do not use `eb` (in Strata Core Syntax) here (e.g., see below) - -- eb[(~ExceptErrorRegex_mkOK expr)] - -- that captures `expr` as an `.fvar`. - .some (LExpr.mkApp () (.op () "ExceptErrorRegex_mkOK" none) [expr]) - | some (ParseError.unimplemented msg _pattern _pos) => - .some (LExpr.mkApp () (.op () "ExceptErrorRegex_mkErr" none) - [LExpr.mkApp () (.op () "Error_Unimplemented" none) [.strConst () (toString msg)]]) - | some (ParseError.patternError msg _pattern _pos) => - .some (LExpr.mkApp () (.op () "ExceptErrorRegex_mkErr" none) - [LExpr.mkApp () (.op () "Error_RePatternErr" none) [.strConst () (toString msg)]]) + .some (LExpr.mkApp () (.op () "NoError" (some mty[Error])) []) + | some (ParseError.unimplemented ..) => + .some (LExpr.mkApp () (.op () "NoError" (some mty[Error])) []) + | some (ParseError.patternError msg ..) => + .some (LExpr.mkApp () (.op () "RePatternError" (some mty[string → Error])) + [.strConst () (toString msg)]) | _ => .none) } def ReFactory : @Factory Core.CoreLParams := #[ - reCompileFunc + reFullmatchStrFunc, + reMatchStrFunc, + reSearchStrFunc, + rePatternErrorFunc ] +/-- Core.Factory extended with regex factory functions. -/ +def PythonFactory : @Lambda.Factory Core.CoreLParams := + Core.Factory.append ReFactory + end -- public section ------------------------------------------------------------------------------- diff --git a/Strata/Languages/Python/PythonLaurelCorePrelude.lean b/Strata/Languages/Python/PythonLaurelCorePrelude.lean index 9cff544a3..4ebabce4c 100644 --- a/Strata/Languages/Python/PythonLaurelCorePrelude.lean +++ b/Strata/Languages/Python/PythonLaurelCorePrelude.lean @@ -49,7 +49,8 @@ datatype Error () { AssertionError (Assertion_msg : string), UnimplementedError (Unimplement_msg : string), UndefinedError (Undefined_msg : string), - IndexError (IndexError_msg : string) + IndexError (IndexError_msg : string), + RePatternError (Re_msg : string) }; // ///////////////////////////////////////////////////////////////////////////////////// @@ -100,12 +101,103 @@ datatype DictStrAny () { DictStrAny_cons (key: string, val: Any, tail: DictStrAny) }; +// Forward declarations: needed so the inline functions after CoreOnlyDelimiter +// can reference these during DDM parsing. Filtered out at merge (precede the +// sentinel). The real definitions with concreteEval are supplied by ReFactory +// at verification time. +function re_fullmatch_str(pattern : string) : regex; +function re_match_str(pattern : string) : regex; +function re_search_str(pattern : string) : regex; +function re_pattern_error(pattern : string) : Error; + type CoreOnlyDelimiter; // ===================================================================== // Core-only declarations (not expressed in Laurel) // ===================================================================== +// ///////////////////////////////////////////////////////////////////////////////////// +// Regex support +// +// Python signatures: +// re.compile(pattern: str) -> re.Pattern +// re.match(pattern: str | re.Pattern, string: str) -> re.Match | None +// re.search(pattern: str | re.Pattern, string: str) -> re.Match | None +// re.fullmatch(pattern: str | re.Pattern, string: str) -> re.Match | None +// +// Architecture: +// +// re.compile is a semantic no-op — it returns the pattern string unchanged. +// The mode-specific factory functions re_fullmatch_str, re_match_str, +// re_search_str each compile a pattern string to a regex with the correct +// MatchMode (via pythonRegexToCore), so anchors (^/$) are handled properly. +// Their concreteEval fires when the pattern is a string literal. +// +// The _bool helpers call the mode-specific factories, so there is a single +// source of truth for mode-specific compilation. +// +// On match, we return a from_ClassInstance wrapping a concrete re_Match +// with pos=0 and endpos=str.len(s), which is sound for the module-level +// API (no pos/endpos parameters). +// ///////////////////////////////////////////////////////////////////////////////////// + +// Mode-specific factory functions are declared via ReFactory (with concreteEval +// for literal pattern expansion), not in this prelude, to avoid duplicate +// definitions. + +inline function re_fullmatch_bool(pattern : string, s : string) : bool { + str.in.re(s, re_fullmatch_str(pattern)) +} +inline function re_match_bool(pattern : string, s : string) : bool { + str.in.re(s, re_match_str(pattern)) +} +inline function re_search_bool(pattern : string, s : string) : bool { + str.in.re(s, re_search_str(pattern)) +} + +inline function mk_re_Match(s : string) : Any { + from_ClassInstance("re_Match", + DictStrAny_cons("re_match_string", from_string(s), + DictStrAny_cons("re_match_pos", from_int(0), + DictStrAny_cons("re_match_endpos", from_int(str.len(s)), + DictStrAny_empty())))) +} + +// re.compile is a no-op: returns the pattern string unchanged. +inline function re_compile(pattern : Any) : Any + requires Any..isfrom_string(pattern); +{ + pattern +} + +inline function re_fullmatch(pattern : Any, s : Any) : Any + requires Any..isfrom_string(pattern) && Any..isfrom_string(s); +{ + if Error..isRePatternError(re_pattern_error(Any..as_string!(pattern))) + then exception(re_pattern_error(Any..as_string!(pattern))) + else if re_fullmatch_bool(Any..as_string!(pattern), Any..as_string!(s)) + then mk_re_Match(Any..as_string!(s)) + else from_none() +} +inline function re_match(pattern : Any, s : Any) : Any + requires Any..isfrom_string(pattern) && Any..isfrom_string(s); +{ + if Error..isRePatternError(re_pattern_error(Any..as_string!(pattern))) + then exception(re_pattern_error(Any..as_string!(pattern))) + else if re_match_bool(Any..as_string!(pattern), Any..as_string!(s)) + then mk_re_Match(Any..as_string!(s)) + else from_none() +} +inline function re_search(pattern : Any, s : Any) : Any + requires Any..isfrom_string(pattern) && Any..isfrom_string(s); +{ + if Error..isRePatternError(re_pattern_error(Any..as_string!(pattern))) + then exception(re_pattern_error(Any..as_string!(pattern))) + else if re_search_bool(Any..as_string!(pattern), Any..as_string!(s)) + then mk_re_Match(Any..as_string!(s)) + else from_none() +} + // ///////////////////////////////////////////////////////////////////////////////////// //Functions that we provide to Python user //to write assertions/contracts about about types of variables diff --git a/Strata/Languages/Python/PythonRuntimeLaurelPart.lean b/Strata/Languages/Python/PythonRuntimeLaurelPart.lean index 47d0298da..9de71728c 100644 --- a/Strata/Languages/Python/PythonRuntimeLaurelPart.lean +++ b/Strata/Languages/Python/PythonRuntimeLaurelPart.lean @@ -42,7 +42,8 @@ datatype Error { AssertionError (Assertion_msg : string), UnimplementedError (Unimplement_msg : string), UndefinedError (Undefined_msg : string), - IndexError (IndexError_msg : string) + IndexError (IndexError_msg : string), + RePatternError (Re_msg : string) } // ///////////////////////////////////////////////////////////////////////////////////// @@ -96,6 +97,48 @@ datatype DictStrAny { DictStrAny_cons (key: string, val: Any, tail: DictStrAny) } +// ///////////////////////////////////////////////////////////////////////////////////// +// Regex support — re.Match +// +// Models Python's re.Match as a composite (reference) type following the +// module_Class naming convention (re_Match). +// +// The Python-through-Laurel pipeline is entirely Any-typed: all user +// variables and function inputs/outputs are wrapped in the Any datatype. +// Consequently, re_match/re_search/re_fullmatch return Any (from_none +// or from_ClassInstance wrapping a re_Match). If the pipeline ever +// moves to concrete types, these should return re_Match | None directly. +// +// Fields that can be determined from the call site are set concretely +// in the Core-only prelude. pos and endpos are sound as 0 / str.len +// for the module-level re.match/re.search/re.fullmatch API which does +// not accept pos/endpos arguments. If compiled-pattern method calls +// with explicit pos/endpos are supported later, those values must be +// threaded through. +// +// Methods that depend on capture groups (group, start, end, span, +// groups, lastindex, lastgroup) are uninterpreted because SMT-LIB's +// string theory has no capture group support. This is a sound +// over-approximation: the solver treats them as abstract, so +// verification results involving these will be inconclusive rather +// than unsound. + +composite re_Match { + var re_match_string : string + var re_match_pos : int + var re_match_endpos : int +} + +// re.Match methods — uninterpreted (capture groups are beyond SMT-LIB) +function re_Match_group (self : re_Match, n : int) : string; +function re_Match_start (self : re_Match, n : int) : int; +function re_Match_end (self : re_Match, n : int) : int; +function re_Match_span_start (self : re_Match, n : int) : int; +function re_Match_span_end (self : re_Match, n : int) : int; +function re_Match_lastindex (self : re_Match) : int; +function re_Match_lastgroup (self : re_Match) : string; +function re_Match_groups (self : re_Match) : ListStr; + datatype FIRST_END_MARKER { } #end diff --git a/Strata/Languages/Python/Regex/ReToCore.lean b/Strata/Languages/Python/Regex/ReToCore.lean index c56f107f8..c889b3f09 100644 --- a/Strata/Languages/Python/Regex/ReToCore.lean +++ b/Strata/Languages/Python/Regex/ReToCore.lean @@ -16,6 +16,7 @@ public section ------------------------------------------------------------------------------- open Lambda.LExpr +open Lambda.LTy.Syntax open Core /-- @@ -105,39 +106,48 @@ private def RegexAST.hasNonAnchorContent (r : RegexAST) : Bool := | .complement _ => true | _ => false) +-- Type annotations for regex ops. concreteEval runs after the type-checker, +-- so expressions it produces must already carry annotations for the SMT encoder. +private def reTy := mty[regex] +private def s2r := mty[string → regex] +private def r2r := mty[regex → regex] +private def rr2r := mty[regex → (regex → regex)] +private def ss2r := mty[string → (string → regex)] +private def rii2r := mty[regex → (int → (int → regex))] + /-- Empty regex pattern; matches an empty string. -/ -private def Core.emptyRegex : Core.Expression.Expr := - mkApp () (.op () strToRegexFunc.name none) [strConst () ""] +private def Core.emptyRegex : Expression.Expr := + mkApp () (.op () strToRegexFunc.name (some s2r)) [strConst () ""] /-- Unmatchable regex pattern. -/ -private def Core.unmatchableRegex : Core.Expression.Expr := - mkApp () (.op () reNoneFunc.name none) [] +private def Core.unmatchableRegex : Expression.Expr := + mkApp () (.op () reNoneFunc.name (some reTy)) [] -- Core regex expression builders. -private abbrev mkReFromStr (s : String) : Core.Expression.Expr := - mkApp () (.op () strToRegexFunc.name none) [strConst () s] -private abbrev mkReRange (c1 c2 : Char) : Core.Expression.Expr := - mkApp () (.op () reRangeFunc.name none) [strConst () (toString c1), strConst () (toString c2)] -private abbrev mkReAllChar : Core.Expression.Expr := - .op () reAllCharFunc.name none -private abbrev mkReComp (r : Core.Expression.Expr) : Core.Expression.Expr := - mkApp () (.op () reCompFunc.name none) [r] -private abbrev mkReUnion (a b : Core.Expression.Expr) : Core.Expression.Expr := - mkApp () (.op () reUnionFunc.name none) [a, b] -private abbrev mkReConcat (a b : Core.Expression.Expr) : Core.Expression.Expr := - mkApp () (.op () reConcatFunc.name none) [a, b] -private abbrev mkReInter (a b : Core.Expression.Expr) : Core.Expression.Expr := - mkApp () (.op () reInterFunc.name none) [a, b] -private abbrev mkReStar (r : Core.Expression.Expr) : Core.Expression.Expr := - mkApp () (.op () reStarFunc.name none) [r] -private abbrev mkRePlus (r : Core.Expression.Expr) : Core.Expression.Expr := - mkApp () (.op () rePlusFunc.name none) [r] -private abbrev mkReLoop (r : Core.Expression.Expr) (lo hi : Nat) : Core.Expression.Expr := - mkApp () (.op () reLoopFunc.name none) [r, intConst () lo, intConst () hi] +private abbrev mkReFromStr (s : String) : Expression.Expr := + mkApp () (.op () strToRegexFunc.name (some s2r)) [strConst () s] +private abbrev mkReRange (c1 c2 : Char) : Expression.Expr := + mkApp () (.op () reRangeFunc.name (some ss2r)) [strConst () (toString c1), strConst () (toString c2)] +private abbrev mkReAllChar : Expression.Expr := + .op () reAllCharFunc.name (some reTy) +private abbrev mkReComp (r : Expression.Expr) : Expression.Expr := + mkApp () (.op () reCompFunc.name (some r2r)) [r] +private abbrev mkReUnion (a b : Expression.Expr) : Expression.Expr := + mkApp () (.op () reUnionFunc.name (some rr2r)) [a, b] +private abbrev mkReConcat (a b : Expression.Expr) : Expression.Expr := + mkApp () (.op () reConcatFunc.name (some rr2r)) [a, b] +private abbrev mkReInter (a b : Expression.Expr) : Expression.Expr := + mkApp () (.op () reInterFunc.name (some rr2r)) [a, b] +private abbrev mkReStar (r : Expression.Expr) : Expression.Expr := + mkApp () (.op () reStarFunc.name (some r2r)) [r] +private abbrev mkRePlus (r : Expression.Expr) : Expression.Expr := + mkApp () (.op () rePlusFunc.name (some r2r)) [r] +private abbrev mkReLoop (r : Expression.Expr) (lo hi : Nat) : Expression.Expr := + mkApp () (.op () reLoopFunc.name (some rii2r)) [r, intConst () lo, intConst () hi] /-- Shared body for `star` and `loop {0, m}` (m ≥ 2): @@ -303,7 +313,7 @@ private def RegexAST.toCore (r : RegexAST) (atStart atEnd : Bool) : def pythonRegexToCore (pyRegex : String) (mode : MatchMode := .fullmatch) : Core.Expression.Expr × Option ParseError := match parseTop pyRegex with - | .error err => (mkApp () (.op () reAllFunc.name none) [], some err) + | .error err => (mkApp () (.op () reAllFunc.name (some reTy)) [], some err) | .ok ast => -- `dotStar`: passed with `atStart=false`, `atEnd=false` since `anychar` -- ignores both. diff --git a/StrataMain.lean b/StrataMain.lean index 977d9d5c8..eb8e0ac66 100644 --- a/StrataMain.lean +++ b/StrataMain.lean @@ -446,7 +446,8 @@ def pyAnalyzeLaurelCommand : Command where | .some dir => { baseOptions with vcDirectory := some (dir : System.FilePath) } | .none => baseOptions let vcResults ← - match ← Strata.verifyCore coreProgram options |>.toBaseIO with + match ← Strata.verifyCore coreProgram options + (moreFns := Strata.Python.ReFactory) |>.toBaseIO with | .ok r => pure r | .error msg => exitInternalError msg @@ -525,7 +526,7 @@ def pyAnalyzeToGotoCommand : Command where | ⟨.error e, _⟩ => panic! e | ⟨.ok (_changed, newPgm), _⟩ => -- Type-check the full program (registers Python types like ExceptOrNone) - let Ctx := { Lambda.LContext.default with functions := Core.Factory, knownTypes := Core.KnownTypes } + let Ctx := { Lambda.LContext.default with functions := Strata.Python.PythonFactory, knownTypes := Core.KnownTypes } let Env := Lambda.TEnv.default let (tcPgm, _) ← match Core.Program.typeCheck Ctx Env newPgm with | .ok r => pure r @@ -600,7 +601,8 @@ def pyAnalyzeLaurelToGotoCommand : Command where | .error msg => exitFailure msg let sourceText := (← tryReadPythonSource filePath).map (·.2) let baseName := deriveBaseName filePath - match ← Strata.inlineCoreToGotoFiles coreProgram baseName sourceText |>.toBaseIO with + match ← Strata.inlineCoreToGotoFiles coreProgram baseName sourceText + (factory := Strata.Python.PythonFactory) |>.toBaseIO with | .ok () => pure () | .error msg => exitFailure msg diff --git a/StrataTest/Languages/Python/AnalyzeLaurelTest.lean b/StrataTest/Languages/Python/AnalyzeLaurelTest.lean index 16ffc9efc..39498bfbd 100644 --- a/StrataTest/Languages/Python/AnalyzeLaurelTest.lean +++ b/StrataTest/Languages/Python/AnalyzeLaurelTest.lean @@ -7,6 +7,7 @@ module meta import Strata.SimpleAPI meta import Strata.Languages.Python.PySpecPipeline +meta import Strata.Languages.Python.PyFactory meta import StrataTest.Util.Python /-! ## End-to-end tests for `pyAnalyzeLaurel` with dispatch @@ -96,7 +97,7 @@ private meta def runAnalyze (dispatchIon : System.FilePath) match Strata.translateCombinedLaurel laurel with | (some core, []) => -- Also run Core type checking to catch semantic errors (e.g. Heap vs Any) - match Core.typeCheck Core.VerifyOptions.quiet core with + match Core.typeCheck Core.VerifyOptions.quiet core (moreFns := Strata.Python.ReFactory) with | .error diag => return .error s!"Core type checking failed: {diag}" | .ok _ => return .ok core | (_, errors) => return .error s!"Laurel to Core translation failed: {errors}" diff --git a/StrataTest/Languages/Python/Regex/ReToCoreTests.lean b/StrataTest/Languages/Python/Regex/ReToCoreTests.lean index 0e1785d33..d7cc2cf0f 100644 --- a/StrataTest/Languages/Python/Regex/ReToCoreTests.lean +++ b/StrataTest/Languages/Python/Regex/ReToCoreTests.lean @@ -11,6 +11,10 @@ namespace Strata.Python.Tests open Strata.Python +private def pythonRegexToCoreEraseTypes (r : String) (mode : MatchMode := MatchMode.fullmatch) := + let (exp, err) := pythonRegexToCore r mode + (exp.eraseTypes, err) + /-- info: ((~Re.Concat (~Re.Concat (~Str.ToRegEx #a) (~Str.ToRegEx #b)) @@ -20,7 +24,7 @@ info: ((~Re.Concat none) -/ #guard_msgs in -#eval Std.format$ pythonRegexToCore "ab.*" -- Encoded as `ab(|.|..*.)` +#eval Std.format$ pythonRegexToCoreEraseTypes "ab.*" -- Encoded as `ab(|.|..*.)` /-- info: ((~Re.Concat @@ -33,7 +37,7 @@ info: ((~Re.Concat none) -/ #guard_msgs in -#eval Std.format$ pythonRegexToCore "ab(c$)*" +#eval Std.format$ pythonRegexToCoreEraseTypes "ab(c$)*" /-- info: ((~Re.Concat @@ -48,37 +52,37 @@ info: ((~Re.Concat none) -/ #guard_msgs in -#eval Std.format$ pythonRegexToCore "ab(^c$)*" +#eval Std.format$ pythonRegexToCoreEraseTypes "ab(^c$)*" /-- info: ((~Re.Concat (~Str.ToRegEx #a) (~Str.ToRegEx #b)), none) -/ #guard_msgs in -#eval Std.format$ pythonRegexToCore "ab" +#eval Std.format$ pythonRegexToCoreEraseTypes "ab" /-- info: ((~Re.Union (~Str.ToRegEx #a) (~Str.ToRegEx #b)), none) -/ #guard_msgs in -#eval Std.format$ pythonRegexToCore "a|b" +#eval Std.format$ pythonRegexToCoreEraseTypes "a|b" /-- info: ((~Re.Concat (~Re.Concat (~Str.ToRegEx #) (~Str.ToRegEx #a)) (~Str.ToRegEx #b)), none) -/ #guard_msgs in -#eval Std.format$ pythonRegexToCore "^ab" +#eval Std.format$ pythonRegexToCoreEraseTypes "^ab" /-- info: ((~Re.Concat (~Re.Concat (~Re.Concat (~Str.ToRegEx #) (~Str.ToRegEx #a)) (~Str.ToRegEx #b)) (~Str.ToRegEx #)), none) -/ #guard_msgs in -#eval Std.format$ pythonRegexToCore "^ab$" +#eval Std.format$ pythonRegexToCoreEraseTypes "^ab$" /-- info: ((~Re.Concat (~Re.Concat (~Str.ToRegEx #a) ~Re.None) (~Str.ToRegEx #b)), none) -/ #guard_msgs in -#eval Std.format$ pythonRegexToCore "(a$)b" +#eval Std.format$ pythonRegexToCoreEraseTypes "(a$)b" /-- info: ((~Re.Concat @@ -89,7 +93,7 @@ info: ((~Re.Concat none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "^^^a$$" +#eval Std.format $ pythonRegexToCoreEraseTypes "^^^a$$" /-- info: ((~Re.Concat @@ -100,7 +104,7 @@ info: ((~Re.Concat none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "^(^^a$$)" +#eval Std.format $ pythonRegexToCoreEraseTypes "^(^^a$$)" /-- info: ((~Re.Union @@ -109,7 +113,7 @@ info: ((~Re.Union none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "(^a$)|(^b$)" +#eval Std.format $ pythonRegexToCoreEraseTypes "(^a$)|(^b$)" /-- info: ((~Re.Concat @@ -118,7 +122,7 @@ info: ((~Re.Concat none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "c((^a)|(^b))" +#eval Std.format $ pythonRegexToCoreEraseTypes "c((^a)|(^b))" /-- info: ((~Re.Concat @@ -127,13 +131,13 @@ info: ((~Re.Concat none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "((a$)|(b$))c" +#eval Std.format $ pythonRegexToCoreEraseTypes "((a$)|(b$))c" /-- info: ((~Re.Concat (~Re.Union (~Re.Concat (~Str.ToRegEx #a) ~Re.None) (~Str.ToRegEx #b)) (~Str.ToRegEx #c)), none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "((a$)|(b))c" +#eval Std.format $ pythonRegexToCoreEraseTypes "((a$)|(b))c" /-- info: ((~Re.Concat @@ -144,19 +148,19 @@ info: ((~Re.Concat none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "c((a$)|(^b$))" +#eval Std.format $ pythonRegexToCoreEraseTypes "c((a$)|(^b$))" /-- info: ((~Re.Concat (~Re.Union (~Re.Concat (~Str.ToRegEx #a) ~Re.None) (~Str.ToRegEx #b)) (~Str.ToRegEx #c)), none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "((a$)|(b))c" +#eval Std.format $ pythonRegexToCoreEraseTypes "((a$)|(b))c" /-- info: ((~Re.Concat (~Re.Concat (~Str.ToRegEx #) ~Re.None) (~Str.ToRegEx #b)), none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "^$b" +#eval Std.format $ pythonRegexToCoreEraseTypes "^$b" /-- info: ((~Re.Union @@ -165,7 +169,7 @@ info: ((~Re.Union none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "^a$|^$b" +#eval Std.format $ pythonRegexToCoreEraseTypes "^a$|^$b" /-- info: ((~Re.Concat @@ -176,7 +180,7 @@ info: ((~Re.Concat none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "c(^a|b$)d" +#eval Std.format $ pythonRegexToCoreEraseTypes "c(^a|b$)d" /-- info: ((~Re.Concat @@ -187,7 +191,7 @@ info: ((~Re.Concat none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "(c(^a|b$))d" +#eval Std.format $ pythonRegexToCoreEraseTypes "(c(^a|b$))d" /-- info: ((~Re.Concat @@ -196,7 +200,7 @@ info: ((~Re.Concat none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "(^a|b$)(^c|d$)" +#eval Std.format $ pythonRegexToCoreEraseTypes "(^a|b$)(^c|d$)" /-- info: ((~Re.Concat @@ -207,81 +211,81 @@ info: ((~Re.Concat none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "((^a|b$)^)c" +#eval Std.format $ pythonRegexToCoreEraseTypes "((^a|b$)^)c" /-- info: ((~Re.Concat (~Re.Union (~Str.ToRegEx #) ~Re.None) (~Str.ToRegEx #c)), none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "(^|$)c" +#eval Std.format $ pythonRegexToCoreEraseTypes "(^|$)c" /-- info: ((~Re.Concat (~Str.ToRegEx #) (~Str.ToRegEx #)), none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "^^" +#eval Std.format $ pythonRegexToCoreEraseTypes "^^" /-- info: ((~Re.Concat (~Re.Concat (~Re.Concat (~Str.ToRegEx #) (~Str.ToRegEx #)) (~Str.ToRegEx #)) (~Str.ToRegEx #)), none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "^$$^" +#eval Std.format $ pythonRegexToCoreEraseTypes "^$$^" /-- info: ((~Re.Concat (~Re.Union (~Str.ToRegEx #) (~Str.ToRegEx #)) (~Str.ToRegEx #)), none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "(^|$)^" +#eval Std.format $ pythonRegexToCoreEraseTypes "(^|$)^" /-- info: ((~Re.Concat (~Re.Concat (~Str.ToRegEx #) (~Str.ToRegEx #a)) (~Str.ToRegEx #)), none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "^a$" .fullmatch +#eval Std.format $ pythonRegexToCoreEraseTypes "^a$" .fullmatch /-- info: (~Re.All, some Pattern error at position 1: Invalid repeat bounds {100,2}: maximum 2 is less than minimum 100 in pattern 'x{100,2}') -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "x{100,2}" .fullmatch +#eval Std.format $ pythonRegexToCoreEraseTypes "x{100,2}" .fullmatch -- (unmatchable) /-- info: ((~Re.Concat (~Re.Concat (~Str.ToRegEx #a) ~Re.None) (~Str.ToRegEx #b)), none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "a^b" .fullmatch +#eval Std.format $ pythonRegexToCoreEraseTypes "a^b" .fullmatch /-- info: ((~Re.Concat (~Re.Concat (~Re.Concat (~Str.ToRegEx #) (~Str.ToRegEx #a)) ~Re.None) (~Str.ToRegEx #b)), none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "^a^b" .fullmatch +#eval Std.format $ pythonRegexToCoreEraseTypes "^a^b" .fullmatch /-- info: ((~Re.Concat (~Re.Concat (~Str.ToRegEx #a) ~Re.None) (~Str.ToRegEx #b)), none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "a$b" .fullmatch +#eval Std.format $ pythonRegexToCoreEraseTypes "a$b" .fullmatch /-- info: ((~Re.Inter ~Re.AllChar (~Re.Comp (~Str.ToRegEx #b))), none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "[^b]" .fullmatch +#eval Std.format $ pythonRegexToCoreEraseTypes "[^b]" .fullmatch /-- info: ((~Re.Inter ~Re.AllChar (~Re.Comp (~Re.Range #A #Z))), none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "[^A-Z]" .fullmatch +#eval Std.format $ pythonRegexToCoreEraseTypes "[^A-Z]" .fullmatch /-- info: ((~Re.Inter ~Re.AllChar (~Re.Comp (~Str.ToRegEx #^))), none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "[^^]" .fullmatch +#eval Std.format $ pythonRegexToCoreEraseTypes "[^^]" .fullmatch /-- info: ((~Str.ToRegEx #a), none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "a" .fullmatch +#eval Std.format $ pythonRegexToCoreEraseTypes "a" .fullmatch /-- info: ((~Re.Union @@ -294,7 +298,7 @@ info: ((~Re.Union none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "a" .match +#eval Std.format $ pythonRegexToCoreEraseTypes "a" .match -- search mode tests /-- @@ -324,7 +328,7 @@ info: ((~Re.Union none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "a" .search +#eval Std.format $ pythonRegexToCoreEraseTypes "a" .search /-- info: ((~Re.Union @@ -353,12 +357,12 @@ info: ((~Re.Union none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "^a$" .search +#eval Std.format $ pythonRegexToCoreEraseTypes "^a$" .search /-- info: ((~Re.Concat (~Str.ToRegEx #) (~Str.ToRegEx #a)), none) -/ #guard_msgs in -#eval Std.format $ pythonRegexToCore "^a" .fullmatch +#eval Std.format $ pythonRegexToCoreEraseTypes "^a" .fullmatch end Strata.Python.Tests diff --git a/StrataTest/Languages/Python/expected_laurel/test_regex_negative.expected b/StrataTest/Languages/Python/expected_laurel/test_regex_negative.expected new file mode 100644 index 000000000..fd7882d62 --- /dev/null +++ b/StrataTest/Languages/Python/expected_laurel/test_regex_negative.expected @@ -0,0 +1,74 @@ + +==== Verification Results ==== +List_get_body_calls_List_get_0: ✅ pass +List_take_body_calls_List_take_0: ✅ pass +List_drop_body_calls_List_drop_0: ✅ pass +List_slice_body_calls_List_drop_0: ✅ pass +List_slice_body_calls_List_take_1: ✅ pass +List_set_body_calls_List_set_0: ✅ pass +DictStrAny_get_body_calls_DictStrAny_get_0: ✅ pass +Any_get_body_calls_DictStrAny_get_0: ✅ pass +Any_get_body_calls_List_get_1: ✅ pass +Any_get_body_calls_List_slice_2: ✅ pass +Any_get_body_calls_List_drop_3: ✅ pass +Any_get!_body_calls_DictStrAny_get_0: ✅ pass +Any_get!_body_calls_List_get_1: ✅ pass +Any_set_body_calls_List_set_0: ✅ pass +Any_set!_body_calls_List_set_0: ✅ pass +PFloorDiv_body_calls_Int.SafeDiv_0: ✅ pass +PFloorDiv_body_calls_Int.SafeDiv_1: ✅ pass +PFloorDiv_body_calls_Int.SafeDiv_2: ✅ pass +PFloorDiv_body_calls_Int.SafeDiv_3: ✅ pass +PAnd_body_calls_Any_to_bool_0: ✅ pass +POr_body_calls_Any_to_bool_0: ✅ pass +ret_type: ✅ pass (in prelude file) +ret_type: ✅ pass (in prelude file) +ret_pos: ✅ pass (in prelude file) +assert_name_is_foo: ✅ pass (in prelude file) +assert_opt_name_none_or_str: ✅ pass (in prelude file) +assert_opt_name_none_or_bar: ✅ pass (in prelude file) +ensures_maybe_except_none: ✅ pass (in prelude file) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(272)_calls_Any_to_bool_0: ✅ pass (at line 10, col 4) +assert(272): ❓ unknown (at line 10, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(365)_calls_Any_to_bool_0: ✅ pass (at line 13, col 4) +assert(365): ❓ unknown (at line 13, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(465)_calls_Any_to_bool_0: ✅ pass (at line 16, col 4) +assert(465): ❓ unknown (at line 16, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(603)_calls_Any_to_bool_0: ✅ pass (at line 20, col 4) +assert(603): ❓ unknown (at line 20, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(702)_calls_Any_to_bool_0: ✅ pass (at line 23, col 4) +assert(702): ❓ unknown (at line 23, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(797)_calls_Any_to_bool_0: ✅ pass (at line 26, col 4) +assert(797): ❓ unknown (at line 26, col 4) +set_m_calls_re_match_0: ✅ pass +assert_assert(888)_calls_Any_to_bool_0: ✅ pass (at line 29, col 4) +assert(888): ❓ unknown (at line 29, col 4) +set_p_calls_re_compile_0: ✅ pass +set_m_calls_re_search_0: ✅ pass +assert_assert(1038)_calls_Any_to_bool_0: ✅ pass (at line 34, col 4) +assert(1038): ❓ unknown (at line 34, col 4) +set_m_calls_re_match_0: ✅ pass +assert_assert(1133)_calls_Any_to_bool_0: ✅ pass (at line 37, col 4) +assert(1133): ❓ unknown (at line 37, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(1495)_calls_Any_to_bool_0: ✅ pass (at line 47, col 4) +assert(1495): ❓ unknown (at line 47, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(1667)_calls_Any_to_bool_0: ✅ pass (at line 54, col 4) +assert(1667): ❓ unknown (at line 54, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(1846)_calls_Any_to_bool_0: ✅ pass (at line 61, col 4) +assert(1846): ❓ unknown (at line 61, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(2015)_calls_Any_to_bool_0: ✅ pass (at line 68, col 4) +assert(2015): ❓ unknown (at line 68, col 4) +set_m_calls_re_match_0: ✅ pass +assert_assert(2193)_calls_Any_to_bool_0: ✅ pass (at line 75, col 4) +assert(2193): ❓ unknown (at line 75, col 4) +ite_cond_calls_Any_to_bool_0: ✅ pass diff --git a/StrataTest/Languages/Python/expected_laurel/test_regex_positive.expected b/StrataTest/Languages/Python/expected_laurel/test_regex_positive.expected new file mode 100644 index 000000000..1ee32a6bb --- /dev/null +++ b/StrataTest/Languages/Python/expected_laurel/test_regex_positive.expected @@ -0,0 +1,453 @@ + +==== Verification Results ==== +List_get_body_calls_List_get_0: ✅ pass +List_take_body_calls_List_take_0: ✅ pass +List_drop_body_calls_List_drop_0: ✅ pass +List_slice_body_calls_List_drop_0: ✅ pass +List_slice_body_calls_List_take_1: ✅ pass +List_set_body_calls_List_set_0: ✅ pass +DictStrAny_get_body_calls_DictStrAny_get_0: ✅ pass +Any_get_body_calls_DictStrAny_get_0: ✅ pass +Any_get_body_calls_List_get_1: ✅ pass +Any_get_body_calls_List_slice_2: ✅ pass +Any_get_body_calls_List_drop_3: ✅ pass +Any_get!_body_calls_DictStrAny_get_0: ✅ pass +Any_get!_body_calls_List_get_1: ✅ pass +Any_set_body_calls_List_set_0: ✅ pass +Any_set!_body_calls_List_set_0: ✅ pass +PFloorDiv_body_calls_Int.SafeDiv_0: ✅ pass +PFloorDiv_body_calls_Int.SafeDiv_1: ✅ pass +PFloorDiv_body_calls_Int.SafeDiv_2: ✅ pass +PFloorDiv_body_calls_Int.SafeDiv_3: ✅ pass +PAnd_body_calls_Any_to_bool_0: ✅ pass +POr_body_calls_Any_to_bool_0: ✅ pass +ret_type: ✅ pass (in prelude file) +ret_type: ✅ pass (in prelude file) +ret_pos: ✅ pass (in prelude file) +assert_name_is_foo: ✅ pass (in prelude file) +assert_opt_name_none_or_str: ✅ pass (in prelude file) +assert_opt_name_none_or_bar: ✅ pass (in prelude file) +ensures_maybe_except_none: ✅ pass (in prelude file) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(215)_calls_Any_to_bool_0: ✅ pass (at line 8, col 4) +assert(215): ✅ pass (at line 8, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(308)_calls_Any_to_bool_0: ✅ pass (at line 11, col 4) +assert(308): ✅ pass (at line 11, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(440)_calls_Any_to_bool_0: ✅ pass (at line 15, col 4) +assert(440): ✅ pass (at line 15, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(540)_calls_Any_to_bool_0: ✅ pass (at line 18, col 4) +assert(540): ✅ pass (at line 18, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(672)_calls_Any_to_bool_0: ✅ pass (at line 22, col 4) +assert(672): ✅ pass (at line 22, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(790)_calls_Any_to_bool_0: ✅ pass (at line 25, col 4) +assert(790): ✅ pass (at line 25, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(921)_calls_Any_to_bool_0: ✅ pass (at line 29, col 4) +assert(921): ✅ pass (at line 29, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(1021)_calls_Any_to_bool_0: ✅ pass (at line 32, col 4) +assert(1021): ✅ pass (at line 32, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(1147)_calls_Any_to_bool_0: ✅ pass (at line 36, col 4) +assert(1147): ✅ pass (at line 36, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(1239)_calls_Any_to_bool_0: ✅ pass (at line 39, col 4) +assert(1239): ✅ pass (at line 39, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(1332)_calls_Any_to_bool_0: ✅ pass (at line 42, col 4) +assert(1332): ✅ pass (at line 42, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(1446)_calls_Any_to_bool_0: ✅ pass (at line 46, col 4) +assert(1446): ✅ pass (at line 46, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(1539)_calls_Any_to_bool_0: ✅ pass (at line 49, col 4) +assert(1539): ✅ pass (at line 49, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(1666)_calls_Any_to_bool_0: ✅ pass (at line 53, col 4) +assert(1666): ✅ pass (at line 53, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(1766)_calls_Any_to_bool_0: ✅ pass (at line 56, col 4) +assert(1766): ✅ pass (at line 56, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(1864)_calls_Any_to_bool_0: ✅ pass (at line 59, col 4) +assert(1864): ✅ pass (at line 59, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(1984)_calls_Any_to_bool_0: ✅ pass (at line 63, col 4) +assert(1984): ✅ pass (at line 63, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(2090)_calls_Any_to_bool_0: ✅ pass (at line 66, col 4) +assert(2090): ✅ pass (at line 66, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(2198)_calls_Any_to_bool_0: ✅ pass (at line 69, col 4) +assert(2198): ✅ pass (at line 69, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(2333)_calls_Any_to_bool_0: ✅ pass (at line 73, col 4) +assert(2333): ✅ pass (at line 73, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(2436)_calls_Any_to_bool_0: ✅ pass (at line 76, col 4) +assert(2436): ✅ pass (at line 76, col 4) +set_m_calls_re_match_0: ✅ pass +assert_assert(2696)_calls_Any_to_bool_0: ✅ pass (at line 81, col 4) +assert(2696): ✅ pass (at line 81, col 4) +set_m_calls_re_match_0: ✅ pass +assert_assert(2787)_calls_Any_to_bool_0: ✅ pass (at line 84, col 4) +assert(2787): ✅ pass (at line 84, col 4) +set_m_calls_re_match_0: ✅ pass +assert_assert(2892)_calls_Any_to_bool_0: ✅ pass (at line 87, col 4) +assert(2892): ✅ pass (at line 87, col 4) +set_m_calls_re_match_0: ✅ pass +assert_assert(2985)_calls_Any_to_bool_0: ✅ pass (at line 90, col 4) +assert(2985): ✅ pass (at line 90, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(3241)_calls_Any_to_bool_0: ✅ pass (at line 95, col 4) +assert(3241): ✅ pass (at line 95, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(3341)_calls_Any_to_bool_0: ✅ pass (at line 98, col 4) +assert(3341): ✅ pass (at line 98, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(3441)_calls_Any_to_bool_0: ✅ pass (at line 101, col 4) +assert(3441): ✅ pass (at line 101, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(3531)_calls_Any_to_bool_0: ✅ pass (at line 104, col 4) +assert(3531): ✅ pass (at line 104, col 4) +set_p_calls_re_compile_0: ✅ pass +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(3791)_calls_Any_to_bool_0: ✅ pass (at line 111, col 4) +assert(3791): ✅ pass (at line 111, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(3881)_calls_Any_to_bool_0: ✅ pass (at line 114, col 4) +assert(3881): ✅ pass (at line 114, col 4) +set_m_calls_re_match_0: ✅ pass +assert_assert(3981)_calls_Any_to_bool_0: ✅ pass (at line 117, col 4) +assert(3981): ✅ pass (at line 117, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(4077)_calls_Any_to_bool_0: ✅ pass (at line 120, col 4) +assert(4077): ✅ pass (at line 120, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(4378)_calls_Any_to_bool_0: ✅ pass (at line 126, col 4) +assert(4378): ✅ pass (at line 126, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(4474)_calls_Any_to_bool_0: ✅ pass (at line 129, col 4) +assert(4474): ✅ pass (at line 129, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(4593)_calls_Any_to_bool_0: ✅ pass (at line 133, col 4) +assert(4593): ✅ pass (at line 133, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(4672)_calls_Any_to_bool_0: ✅ pass (at line 136, col 4) +assert(4672): ✅ pass (at line 136, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(4794)_calls_Any_to_bool_0: ✅ pass (at line 140, col 4) +assert(4794): ✅ pass (at line 140, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(4886)_calls_Any_to_bool_0: ✅ pass (at line 143, col 4) +assert(4886): ✅ pass (at line 143, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(5008)_calls_Any_to_bool_0: ✅ pass (at line 147, col 4) +assert(5008): ✅ pass (at line 147, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(5092)_calls_Any_to_bool_0: ✅ pass (at line 150, col 4) +assert(5092): ✅ pass (at line 150, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(5173)_calls_Any_to_bool_0: ✅ pass (at line 153, col 4) +assert(5173): ✅ pass (at line 153, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(5264)_calls_Any_to_bool_0: ✅ pass (at line 156, col 4) +assert(5264): ✅ pass (at line 156, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(5373)_calls_Any_to_bool_0: ✅ pass (at line 160, col 4) +assert(5373): ✅ pass (at line 160, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(5464)_calls_Any_to_bool_0: ✅ pass (at line 163, col 4) +assert(5464): ✅ pass (at line 163, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(5563)_calls_Any_to_bool_0: ✅ pass (at line 166, col 4) +assert(5563): ✅ pass (at line 166, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(5657)_calls_Any_to_bool_0: ✅ pass (at line 169, col 4) +assert(5657): ✅ pass (at line 169, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(5960)_calls_Any_to_bool_0: ✅ pass (at line 175, col 4) +assert(5960): ✅ pass (at line 175, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(6038)_calls_Any_to_bool_0: ✅ pass (at line 178, col 4) +assert(6038): ✅ pass (at line 178, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(6116)_calls_Any_to_bool_0: ✅ pass (at line 181, col 4) +assert(6116): ✅ pass (at line 181, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(6194)_calls_Any_to_bool_0: ✅ pass (at line 184, col 4) +assert(6194): ✅ pass (at line 184, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(6273)_calls_Any_to_bool_0: ✅ pass (at line 187, col 4) +assert(6273): ✅ pass (at line 187, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(6353)_calls_Any_to_bool_0: ✅ pass (at line 190, col 4) +assert(6353): ✅ pass (at line 190, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(6443)_calls_Any_to_bool_0: ✅ pass (at line 193, col 4) +assert(6443): ✅ pass (at line 193, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(6568)_calls_Any_to_bool_0: ✅ pass (at line 197, col 4) +assert(6568): ✅ pass (at line 197, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(6648)_calls_Any_to_bool_0: ✅ pass (at line 200, col 4) +assert(6648): ✅ pass (at line 200, col 4) +set_m_calls_re_match_0: ✅ pass +assert_assert(6727)_calls_Any_to_bool_0: ✅ pass (at line 203, col 4) +assert(6727): ✅ pass (at line 203, col 4) +set_m_calls_re_match_0: ✅ pass +assert_assert(6799)_calls_Any_to_bool_0: ✅ pass (at line 206, col 4) +assert(6799): ✅ pass (at line 206, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(6875)_calls_Any_to_bool_0: ✅ pass (at line 209, col 4) +assert(6875): ✅ pass (at line 209, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(6949)_calls_Any_to_bool_0: ✅ pass (at line 212, col 4) +assert(6949): ✅ pass (at line 212, col 4) +set_m_calls_re_match_0: ✅ pass +assert_assert(7239)_calls_Any_to_bool_0: ✅ pass (at line 218, col 4) +assert(7239): ✅ pass (at line 218, col 4) +set_m_calls_re_match_0: ✅ pass +assert_assert(7303)_calls_Any_to_bool_0: ✅ pass (at line 221, col 4) +assert(7303): ✅ pass (at line 221, col 4) +set_m_calls_re_match_0: ✅ pass +assert_assert(7379)_calls_Any_to_bool_0: ✅ pass (at line 224, col 4) +assert(7379): ✅ pass (at line 224, col 4) +set_m_calls_re_match_0: ✅ pass +assert_assert(7484)_calls_Any_to_bool_0: ✅ pass (at line 228, col 4) +assert(7484): ✅ pass (at line 228, col 4) +set_m_calls_re_match_0: ✅ pass +assert_assert(7556)_calls_Any_to_bool_0: ✅ pass (at line 231, col 4) +assert(7556): ✅ pass (at line 231, col 4) +set_m_calls_re_match_0: ✅ pass +assert_assert(7636)_calls_Any_to_bool_0: ✅ pass (at line 234, col 4) +assert(7636): ✅ pass (at line 234, col 4) +set_m_calls_re_match_0: ✅ pass +assert_assert(7706)_calls_Any_to_bool_0: ✅ pass (at line 237, col 4) +assert(7706): ✅ pass (at line 237, col 4) +set_m_calls_re_match_0: ✅ pass +assert_assert(7790)_calls_Any_to_bool_0: ✅ pass (at line 240, col 4) +assert(7790): ✅ pass (at line 240, col 4) +set_m_calls_re_match_0: ✅ pass +assert_assert(7865)_calls_Any_to_bool_0: ✅ pass (at line 243, col 4) +assert(7865): ✅ pass (at line 243, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(8114)_calls_Any_to_bool_0: ✅ pass (at line 249, col 4) +assert(8114): ✅ pass (at line 249, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(8189)_calls_Any_to_bool_0: ✅ pass (at line 252, col 4) +assert(8189): ✅ pass (at line 252, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(8294)_calls_Any_to_bool_0: ✅ pass (at line 256, col 4) +assert(8294): ✅ pass (at line 256, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(8371)_calls_Any_to_bool_0: ✅ pass (at line 259, col 4) +assert(8371): ✅ pass (at line 259, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(8453)_calls_Any_to_bool_0: ✅ pass (at line 262, col 4) +assert(8453): ✅ pass (at line 262, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(8554)_calls_Any_to_bool_0: ✅ pass (at line 266, col 4) +assert(8554): ✅ pass (at line 266, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(8627)_calls_Any_to_bool_0: ✅ pass (at line 269, col 4) +assert(8627): ✅ pass (at line 269, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(8711)_calls_Any_to_bool_0: ✅ pass (at line 272, col 4) +assert(8711): ✅ pass (at line 272, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(8790)_calls_Any_to_bool_0: ✅ pass (at line 275, col 4) +assert(8790): ✅ pass (at line 275, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(8914)_calls_Any_to_bool_0: ✅ pass (at line 279, col 4) +assert(8914): ✅ pass (at line 279, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(8988)_calls_Any_to_bool_0: ✅ pass (at line 282, col 4) +assert(8988): ✅ pass (at line 282, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(9070)_calls_Any_to_bool_0: ✅ pass (at line 285, col 4) +assert(9070): ✅ pass (at line 285, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(9300)_calls_Any_to_bool_0: ✅ pass (at line 290, col 4) +assert(9300): ✅ pass (at line 290, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(9381)_calls_Any_to_bool_0: ✅ pass (at line 293, col 4) +assert(9381): ✅ pass (at line 293, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(9472)_calls_Any_to_bool_0: ✅ pass (at line 296, col 4) +assert(9472): ✅ pass (at line 296, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(9551)_calls_Any_to_bool_0: ✅ pass (at line 299, col 4) +assert(9551): ✅ pass (at line 299, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(9638)_calls_Any_to_bool_0: ✅ pass (at line 302, col 4) +assert(9638): ✅ pass (at line 302, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(9718)_calls_Any_to_bool_0: ✅ pass (at line 305, col 4) +assert(9718): ✅ pass (at line 305, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(9806)_calls_Any_to_bool_0: ✅ pass (at line 308, col 4) +assert(9806): ✅ pass (at line 308, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(10048)_calls_Any_to_bool_0: ✅ pass (at line 313, col 4) +assert(10048): ✅ pass (at line 313, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(10134)_calls_Any_to_bool_0: ✅ pass (at line 316, col 4) +assert(10134): ✅ pass (at line 316, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(10224)_calls_Any_to_bool_0: ✅ pass (at line 319, col 4) +assert(10224): ✅ pass (at line 319, col 4) +set_m_calls_re_match_0: ✅ pass +assert_assert(10310)_calls_Any_to_bool_0: ✅ pass (at line 322, col 4) +assert(10310): ✅ pass (at line 322, col 4) +set_m_calls_re_match_0: ✅ pass +assert_assert(10390)_calls_Any_to_bool_0: ✅ pass (at line 325, col 4) +assert(10390): ✅ pass (at line 325, col 4) +set_m_calls_re_match_0: ✅ pass +assert_assert(10478)_calls_Any_to_bool_0: ✅ pass (at line 328, col 4) +assert(10478): ✅ pass (at line 328, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(10718)_calls_Any_to_bool_0: ✅ pass (at line 333, col 4) +assert(10718): ✅ pass (at line 333, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(10808)_calls_Any_to_bool_0: ✅ pass (at line 336, col 4) +assert(10808): ✅ pass (at line 336, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(10898)_calls_Any_to_bool_0: ✅ pass (at line 339, col 4) +assert(10898): ✅ pass (at line 339, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(10988)_calls_Any_to_bool_0: ✅ pass (at line 342, col 4) +assert(10988): ✅ pass (at line 342, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(11071)_calls_Any_to_bool_0: ✅ pass (at line 345, col 4) +assert(11071): ✅ pass (at line 345, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(11162)_calls_Any_to_bool_0: ✅ pass (at line 348, col 4) +assert(11162): ✅ pass (at line 348, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(11245)_calls_Any_to_bool_0: ✅ pass (at line 351, col 4) +assert(11245): ✅ pass (at line 351, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(11339)_calls_Any_to_bool_0: ✅ pass (at line 354, col 4) +assert(11339): ✅ pass (at line 354, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(11429)_calls_Any_to_bool_0: ✅ pass (at line 357, col 4) +assert(11429): ✅ pass (at line 357, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(11521)_calls_Any_to_bool_0: ✅ pass (at line 360, col 4) +assert(11521): ✅ pass (at line 360, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(11606)_calls_Any_to_bool_0: ✅ pass (at line 363, col 4) +assert(11606): ✅ pass (at line 363, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(11701)_calls_Any_to_bool_0: ✅ pass (at line 366, col 4) +assert(11701): ✅ pass (at line 366, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(11829)_calls_Any_to_bool_0: ✅ pass (at line 370, col 4) +assert(11829): ✅ pass (at line 370, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(11910)_calls_Any_to_bool_0: ✅ pass (at line 373, col 4) +assert(11910): ✅ pass (at line 373, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(11995)_calls_Any_to_bool_0: ✅ pass (at line 376, col 4) +assert(11995): ✅ pass (at line 376, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(12253)_calls_Any_to_bool_0: ✅ pass (at line 381, col 4) +assert(12253): ✅ pass (at line 381, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(12333)_calls_Any_to_bool_0: ✅ pass (at line 384, col 4) +assert(12333): ✅ pass (at line 384, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(12428)_calls_Any_to_bool_0: ✅ pass (at line 387, col 4) +assert(12428): ✅ pass (at line 387, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(12519)_calls_Any_to_bool_0: ✅ pass (at line 390, col 4) +assert(12519): ✅ pass (at line 390, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(12611)_calls_Any_to_bool_0: ✅ pass (at line 393, col 4) +assert(12611): ✅ pass (at line 393, col 4) +set_m_calls_re_match_0: ✅ pass +assert_assert(12702)_calls_Any_to_bool_0: ✅ pass (at line 396, col 4) +assert(12702): ✅ pass (at line 396, col 4) +set_m_calls_re_match_0: ✅ pass +assert_assert(12796)_calls_Any_to_bool_0: ✅ pass (at line 399, col 4) +assert(12796): ✅ pass (at line 399, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(13063)_calls_Any_to_bool_0: ✅ pass (at line 404, col 4) +assert(13063): ✅ pass (at line 404, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(13156)_calls_Any_to_bool_0: ✅ pass (at line 407, col 4) +assert(13156): ✅ pass (at line 407, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(13253)_calls_Any_to_bool_0: ✅ pass (at line 410, col 4) +assert(13253): ✅ pass (at line 410, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(13345)_calls_Any_to_bool_0: ✅ pass (at line 413, col 4) +assert(13345): ✅ pass (at line 413, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(13455)_calls_Any_to_bool_0: ✅ pass (at line 417, col 4) +assert(13455): ✅ pass (at line 417, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(13541)_calls_Any_to_bool_0: ✅ pass (at line 420, col 4) +assert(13541): ✅ pass (at line 420, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(13631)_calls_Any_to_bool_0: ✅ pass (at line 423, col 4) +assert(13631): ✅ pass (at line 423, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(13724)_calls_Any_to_bool_0: ✅ pass (at line 426, col 4) +assert(13724): ✅ pass (at line 426, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(13954)_calls_Any_to_bool_0: ✅ pass (at line 431, col 4) +assert(13954): ✅ pass (at line 431, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(14044)_calls_Any_to_bool_0: ✅ pass (at line 434, col 4) +assert(14044): ✅ pass (at line 434, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(14136)_calls_Any_to_bool_0: ✅ pass (at line 437, col 4) +assert(14136): ✅ pass (at line 437, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(14220)_calls_Any_to_bool_0: ✅ pass (at line 440, col 4) +assert(14220): ✅ pass (at line 440, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(14307)_calls_Any_to_bool_0: ✅ pass (at line 443, col 4) +assert(14307): ✅ pass (at line 443, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(14392)_calls_Any_to_bool_0: ✅ pass (at line 446, col 4) +assert(14392): ✅ pass (at line 446, col 4) +set_p_calls_re_compile_0: ✅ pass +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(14608)_calls_Any_to_bool_0: ✅ pass (at line 453, col 4) +assert(14608): ✅ pass (at line 453, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(14686)_calls_Any_to_bool_0: ✅ pass (at line 456, col 4) +assert(14686): ✅ pass (at line 456, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(14768)_calls_Any_to_bool_0: ✅ pass (at line 459, col 4) +assert(14768): ✅ pass (at line 459, col 4) +set_m_calls_re_match_0: ✅ pass +assert_assert(14856)_calls_Any_to_bool_0: ✅ pass (at line 462, col 4) +assert(14856): ✅ pass (at line 462, col 4) +set_m_calls_re_match_0: ✅ pass +assert_assert(14936)_calls_Any_to_bool_0: ✅ pass (at line 465, col 4) +assert(14936): ✅ pass (at line 465, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(15360)_calls_Any_to_bool_0: ✅ pass (at line 473, col 4) +assert(15360): ✅ pass (at line 473, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(15469)_calls_Any_to_bool_0: ✅ pass (at line 476, col 4) +assert(15469): ✅ pass (at line 476, col 4) +set_m_calls_re_fullmatch_0: ✅ pass +assert_assert(15585)_calls_Any_to_bool_0: ✅ pass (at line 479, col 4) +assert(15585): ✅ pass (at line 479, col 4) +set_m_calls_re_search_0: ✅ pass +assert_assert(15691)_calls_Any_to_bool_0: ✅ pass (at line 482, col 4) +assert(15691): ✅ pass (at line 482, col 4) +set_m_calls_re_match_0: ✅ pass +assert_assert(15806)_calls_Any_to_bool_0: ✅ pass (at line 485, col 4) +assert(15806): ✅ pass (at line 485, col 4) +ite_cond_calls_Any_to_bool_0: ✅ pass diff --git a/StrataTest/Languages/Python/run_py_analyze_sarif.py b/StrataTest/Languages/Python/run_py_analyze_sarif.py index bac0bcc39..6d4dd7c0e 100755 --- a/StrataTest/Languages/Python/run_py_analyze_sarif.py +++ b/StrataTest/Languages/Python/run_py_analyze_sarif.py @@ -40,6 +40,8 @@ "test_multi_function", "test_multiple_except", "test_nested_calls", + "test_regex_negative", + "test_regex_positive", "test_return_types", "test_subscription", "test_try_except", diff --git a/StrataTest/Languages/Python/tests/test_regex_negative.py b/StrataTest/Languages/Python/tests/test_regex_negative.py new file mode 100644 index 000000000..17e5e944c --- /dev/null +++ b/StrataTest/Languages/Python/tests/test_regex_negative.py @@ -0,0 +1,78 @@ +import re + +def main(): + # ── Expected failures ── + # These assertions are intentionally wrong. The solver should disprove + # them, but currently returns 'unknown' instead of 'fail'. + + # Claim a non-match is a match + m = re.fullmatch(r"a", "b") + assert m != None, "EXPECTED_FAIL: fullmatch a on b" + + m = re.fullmatch(r"abc", "abd") + assert m != None, "EXPECTED_FAIL: fullmatch abc on abd" + + m = re.fullmatch(r"[a-z]+", "ABC") + assert m != None, "EXPECTED_FAIL: fullmatch [a-z]+ on ABC" + + # Anchors should prevent match + m = re.fullmatch(r"^abc$", "abcd") + assert m != None, "EXPECTED_FAIL: fullmatch ^abc$ on abcd" + + m = re.search(r"^abc", "xabc") + assert m != None, "EXPECTED_FAIL: search ^abc in xabc" + + m = re.search(r"abc$", "abcx") + assert m != None, "EXPECTED_FAIL: search abc$ in abcx" + + m = re.match(r"^a$", "ab") + assert m != None, "EXPECTED_FAIL: match ^a$ in ab" + + # Compiled pattern with anchors + p = re.compile(r"^abc$") + m = re.search(p, "xabc") + assert m != None, "EXPECTED_FAIL: compiled ^abc$ search xabc" + + m = re.match(p, "abcx") + assert m != None, "EXPECTED_FAIL: compiled ^abc$ match abcx" + + # ── Malformed patterns (try/except) ──────────────────────────────── + # These currently return 'unknown'. + + caught = False + try: + m = re.fullmatch(r"(abc", "abc") + except Exception: + caught = True + assert caught, "malformed: unmatched paren should raise" + + caught = False + try: + m = re.fullmatch(r"a**", "a") + except Exception: + caught = True + assert caught, "malformed: nothing to repeat should raise" + + caught = False + try: + m = re.fullmatch(r"x{100,2}", "x") + except Exception: + caught = True + assert caught, "malformed: bad bounds should raise" + + caught = False + try: + m = re.search(r"(abc", "xabcx") + except Exception: + caught = True + assert caught, "malformed: search with bad pattern should raise" + + caught = False + try: + m = re.match(r"a**", "aaa") + except Exception: + caught = True + assert caught, "malformed: match with bad pattern should raise" + +if __name__ == "__main__": + main() diff --git a/StrataTest/Languages/Python/tests/test_regex_positive.py b/StrataTest/Languages/Python/tests/test_regex_positive.py new file mode 100644 index 000000000..042dbb9bd --- /dev/null +++ b/StrataTest/Languages/Python/tests/test_regex_positive.py @@ -0,0 +1,488 @@ +import re + +def main(): + # ── re.fullmatch: entire string must match ────────────────────────── + + # Literal match + m = re.fullmatch(r"abc", "abc") + assert m != None, "fullmatch literal should match" + + m = re.fullmatch(r"abc", "abcd") + assert m == None, "fullmatch literal should reject extra chars" + + # Character class + m = re.fullmatch(r"[a-z]+", "hello") + assert m != None, "fullmatch char class should match" + + m = re.fullmatch(r"[a-z]+", "Hello") + assert m == None, "fullmatch char class should reject uppercase" + + # Negated class + m = re.fullmatch(r"[^0-9]+", "hello") + assert m != None, "fullmatch negated class should match non-digits" + + m = re.fullmatch(r"[^0-9]+", "hello123") + assert m == None, "fullmatch negated class should reject digits" + + # Dot (any char) + m = re.fullmatch(r".+", "anything") + assert m != None, "fullmatch dot-plus should match non-empty" + + m = re.fullmatch(r".", "ab") + assert m == None, "fullmatch single dot should reject two chars" + + # Quantifiers: star + m = re.fullmatch(r"a*", "") + assert m != None, "fullmatch a* should match empty" + + m = re.fullmatch(r"a*", "aaa") + assert m != None, "fullmatch a* should match repeated" + + m = re.fullmatch(r"a*", "b") + assert m == None, "fullmatch a* should reject non-a" + + # Quantifiers: plus + m = re.fullmatch(r"a+", "") + assert m == None, "fullmatch a+ should reject empty" + + m = re.fullmatch(r"a+", "aaa") + assert m != None, "fullmatch a+ should match one-or-more" + + # Quantifiers: optional + m = re.fullmatch(r"ab?c", "ac") + assert m != None, "fullmatch ab?c should match without b" + + m = re.fullmatch(r"ab?c", "abc") + assert m != None, "fullmatch ab?c should match with b" + + m = re.fullmatch(r"ab?c", "abbc") + assert m == None, "fullmatch ab?c should reject two b's" + + # Alternation + m = re.fullmatch(r"cat|dog", "cat") + assert m != None, "fullmatch alternation should match first" + + m = re.fullmatch(r"cat|dog", "dog") + assert m != None, "fullmatch alternation should match second" + + m = re.fullmatch(r"cat|dog", "bird") + assert m == None, "fullmatch alternation should reject other" + + # Concatenation + m = re.fullmatch(r"[a-z]+[0-9]+", "abc123") + assert m != None, "fullmatch concat should match" + + m = re.fullmatch(r"[a-z]+[0-9]+", "123abc") + assert m == None, "fullmatch concat should reject wrong order" + + # ── re.match: anchored at start ───────────────────────────────────── + + m = re.match(r"[0-9]+", "123abc") + assert m != None, "match should match at start" + + m = re.match(r"[0-9]+", "abc123") + assert m == None, "match should reject when not at start" + + m = re.match(r"hello", "hello world") + assert m != None, "match should match prefix" + + m = re.match(r"world", "hello world") + assert m == None, "match should reject non-prefix" + + # ── re.search: match anywhere ─────────────────────────────────────── + + m = re.search(r"[0-9]+", "abc123def") + assert m != None, "search should find digits in middle" + + m = re.search(r"[0-9]+", "abcdef") + assert m == None, "search should reject when no digits" + + m = re.search(r"xyz", "abcxyzdef") + assert m != None, "search should find substring" + + m = re.search(r"xyz", "abcdef") + assert m == None, "search should reject missing substring" + + # ── re.compile then match/search/fullmatch ────────────────────────── + + p = re.compile(r"[a-z]+") + + m = re.fullmatch(p, "hello") + assert m != None, "compiled fullmatch should match" + + m = re.fullmatch(p, "Hello") + assert m == None, "compiled fullmatch should reject uppercase" + + m = re.match(p, "hello123") + assert m != None, "compiled match should match prefix" + + m = re.search(p, "123hello456") + assert m != None, "compiled search should find in middle" + + # ── Edge cases ────────────────────────────────────────────────────── + + # Empty pattern + m = re.fullmatch(r"", "") + assert m != None, "fullmatch empty pattern on empty string" + + m = re.fullmatch(r"", "a") + assert m == None, "fullmatch empty pattern on non-empty string" + + # Single char + m = re.fullmatch(r"a", "a") + assert m != None, "fullmatch single char" + + m = re.fullmatch(r"a", "b") + assert m == None, "fullmatch single char mismatch" + + # Nested quantifiers + m = re.fullmatch(r"(ab)+", "ababab") + assert m != None, "fullmatch nested group-plus" + + m = re.fullmatch(r"(ab)+", "abba") + assert m == None, "fullmatch nested group-plus mismatch" + + # Range with loop + m = re.fullmatch(r"a{2,4}", "aa") + assert m != None, "fullmatch loop min" + + m = re.fullmatch(r"a{2,4}", "aaaa") + assert m != None, "fullmatch loop max" + + m = re.fullmatch(r"a{2,4}", "a") + assert m == None, "fullmatch loop below min" + + m = re.fullmatch(r"a{2,4}", "aaaaa") + assert m == None, "fullmatch loop above max" + + # Group loops + m = re.fullmatch(r"(ab){2}", "abab") + assert m != None, "fullmatch group loop match" + + m = re.fullmatch(r"(ab){2}", "ab") + assert m == None, "fullmatch group loop too few" + + m = re.fullmatch(r"(ab){2,3}", "ababab") + assert m != None, "fullmatch group loop 3 reps" + + m = re.fullmatch(r"(ab){2,3}", "ab") + assert m == None, "fullmatch group loop 1 rep" + + # ── Anchors: basic behavior ────────────────────────────────────── + + # fullmatch: ^ and $ are redundant (whole string must match) + m = re.fullmatch(r"^a", "a") + assert m != None, "fullmatch ^a match" + + m = re.fullmatch(r"^a", "ba") + assert m == None, "fullmatch ^a reject" + + m = re.fullmatch(r"a$", "a") + assert m != None, "fullmatch a$ match" + + m = re.fullmatch(r"a$", "ab") + assert m == None, "fullmatch a$ reject" + + m = re.fullmatch(r"^a$", "a") + assert m != None, "fullmatch ^a$ match" + + m = re.fullmatch(r"^a$", "ab") + assert m == None, "fullmatch ^a$ reject trailing" + + m = re.fullmatch(r"^a$", "ba") + assert m == None, "fullmatch ^a$ reject leading" + + # ^$ matches only the empty string + m = re.fullmatch(r"^$", "") + assert m != None, "fullmatch ^$ on empty" + + m = re.fullmatch(r"^$", "a") + assert m == None, "fullmatch ^$ on non-empty" + + m = re.match(r"^$", "") + assert m != None, "match ^$ on empty" + + m = re.match(r"^$", "a") + assert m == None, "match ^$ on non-empty" + + m = re.search(r"^$", "") + assert m != None, "search ^$ on empty" + + m = re.search(r"^$", "a") + assert m == None, "search ^$ on non-empty" + + # ── Anchors in match mode ──────────────────────────────────────── + + # ^ is a no-op in match (already anchored at start) + m = re.match(r"^a", "a") + assert m != None, "match ^a" + + m = re.match(r"^a", "ab") + assert m != None, "match ^a trailing ok" + + m = re.match(r"^a", "ba") + assert m == None, "match ^a reject" + + # $ cuts off trailing content + m = re.match(r"^a$", "a") + assert m != None, "match ^a$ exact" + + m = re.match(r"^a$", "ab") + assert m == None, "match ^a$ reject trailing" + + m = re.match(r"a$", "a") + assert m != None, "match a$ exact" + + m = re.match(r"a$", "ab") + assert m == None, "match a$ reject trailing" + + m = re.match(r"a.*$", "axyz") + assert m != None, "match a.*$ accepts" + + m = re.match(r"a.*$", "b") + assert m == None, "match a.*$ rejects" + + # ── Anchors in search mode ─────────────────────────────────────── + + # basic search + m = re.search(r"a", "xax") + assert m != None, "search a in middle" + + m = re.search(r"a", "xyz") + assert m == None, "search a not found" + + # ^ prevents free prefix + m = re.search(r"^a", "abc") + assert m != None, "search ^a at start" + + m = re.search(r"^a", "xabc") + assert m == None, "search ^a reject non-start" + + m = re.search(r"^a", "a") + assert m != None, "search ^a exact" + + # $ prevents free suffix + m = re.search(r"a$", "ba") + assert m != None, "search a$ at end" + + m = re.search(r"a$", "ab") + assert m == None, "search a$ reject non-end" + + m = re.search(r"a$", "xyzba") + assert m != None, "search a$ deep end" + + m = re.search(r"a$", "xyzbax") + assert m == None, "search a$ reject trailing" + + # ^...$ in search: forces exact match + m = re.search(r"^a$", "a") + assert m != None, "search ^a$ exact" + + m = re.search(r"^a$", "xa") + assert m == None, "search ^a$ reject prefix" + + m = re.search(r"^a$", "ax") + assert m == None, "search ^a$ reject suffix" + + # ── Multi-char anchors in search ───────────────────────────────── + + m = re.search(r"^abc", "abcxyz") + assert m != None, "search ^abc at start" + + m = re.search(r"^abc", "xabc") + assert m == None, "search ^abc reject non-start" + + m = re.search(r"abc$", "xyzabc") + assert m != None, "search abc$ at end" + + m = re.search(r"abc$", "abcx") + assert m == None, "search abc$ reject non-end" + + m = re.search(r"^abc$", "abc") + assert m != None, "search ^abc$ exact" + + m = re.search(r"^abc$", "xabc") + assert m == None, "search ^abc$ reject prefix" + + m = re.search(r"^abc$", "abcx") + assert m == None, "search ^abc$ reject suffix" + + # ── Anchors with quantifiers ───────────────────────────────────── + + m = re.fullmatch(r"^a{3}$", "aaa") + assert m != None, "fullmatch ^a{3}$ match" + + m = re.fullmatch(r"^a{3}$", "aa") + assert m == None, "fullmatch ^a{3}$ too few" + + m = re.fullmatch(r"^a{3}$", "aaaa") + assert m == None, "fullmatch ^a{3}$ too many" + + m = re.match(r"^a{3}$", "aaa") + assert m != None, "match ^a{3}$ exact" + + m = re.match(r"^a{3}$", "aaab") + assert m == None, "match ^a{3}$ reject trailing" + + m = re.match(r"a{3}", "aaab") + assert m != None, "match a{3} trailing ok" + + # ── Escaped metacharacters ─────────────────────────────────────── + + m = re.fullmatch(r"a\.b", "a.b") + assert m != None, "escaped dot matches literal" + + m = re.fullmatch(r"a\.b", "axb") + assert m == None, "escaped dot rejects non-dot" + + m = re.fullmatch(r"a\+b", "a+b") + assert m != None, "escaped plus matches literal" + + m = re.fullmatch(r"a\+b", "ab") + assert m == None, "escaped plus rejects" + + m = re.fullmatch(r"a\*b", "a*b") + assert m != None, "escaped star matches literal" + + m = re.fullmatch(r"a\*b", "aab") + assert m == None, "escaped star rejects" + + m = re.fullmatch(r"a\?b", "a?b") + assert m != None, "escaped question matches literal" + + m = re.fullmatch(r"a\?b", "ab") + assert m == None, "escaped question rejects" + + m = re.fullmatch(r"a\(b\)", "a(b)") + assert m != None, "escaped parens match literal" + + m = re.fullmatch(r"a\(b\)", "ab") + assert m == None, "escaped parens reject" + + m = re.fullmatch(r"a\\b", "a\\b") + assert m != None, "escaped backslash matches literal" + + m = re.fullmatch(r"a\\b", "ab") + assert m == None, "escaped backslash rejects" + + # Escaped metacharacters with search + m = re.search(r"a\.b", "xa.by") + assert m != None, "search escaped dot" + + m = re.search(r"a\\b", "xa\\by") + assert m != None, "search escaped backslash" + + m = re.search(r"a\\b", "xaby") + assert m == None, "search escaped backslash reject" + + # ── Colon in patterns ──────────────────────────────────────────── + + m = re.fullmatch(r"a:b", "a:b") + assert m != None, "colon literal match" + + m = re.fullmatch(r"a:b", "ab") + assert m == None, "colon literal reject" + + m = re.fullmatch(r"[a-z]+:[0-9]+", "foo:42") + assert m != None, "colon class match" + + m = re.fullmatch(r"[a-z]+:[0-9]+", "foo42") + assert m == None, "colon class reject" + + m = re.search(r"[a-z]+:[0-9]+", "xfoo:42y") + assert m != None, "search colon class" + + m = re.match(r"^[a-z]+:[0-9]+$", "foo:42") + assert m != None, "match anchored colon" + + m = re.match(r"^[a-z]+:[0-9]+$", "foo:42x") + assert m == None, "match anchored colon reject trailing" + + # ── Multi-char patterns ────────────────────────────────────────── + + m = re.fullmatch(r"abc.*def", "abcdef") + assert m != None, "wildcard empty middle" + + m = re.fullmatch(r"abc.*def", "abcXXdef") + assert m != None, "wildcard non-empty middle" + + m = re.fullmatch(r"abc.*def", "abcXXdeg") + assert m == None, "wildcard wrong ending" + + m = re.search(r"abc.*def", "xabcXXdefy") + assert m != None, "search wildcard" + + # Multi-char alternation + m = re.fullmatch(r"abc|def", "abc") + assert m != None, "multi-char alt first" + + m = re.fullmatch(r"abc|def", "def") + assert m != None, "multi-char alt second" + + m = re.fullmatch(r"abc|def", "abcdef") + assert m == None, "multi-char alt reject concat" + + m = re.search(r"abc|def", "xdefy") + assert m != None, "search multi-char alt" + + # ── Anchors inside alternation ─────────────────────────────────── + + m = re.fullmatch(r"^a|b$", "a") + assert m != None, "fullmatch ^a|b$ first branch" + + m = re.fullmatch(r"^a|b$", "b") + assert m != None, "fullmatch ^a|b$ second branch" + + m = re.fullmatch(r"^a|b$", "ab") + assert m == None, "fullmatch ^a|b$ reject" + + m = re.search(r"^a|b$", "axyz") + assert m != None, "search ^a|b$ start anchor" + + m = re.search(r"^a|b$", "xyzb") + assert m != None, "search ^a|b$ end anchor" + + m = re.search(r"^a|b$", "xyzc") + assert m == None, "search ^a|b$ neither" + + # ── Compile + anchors: mode applied at match time ──────────────── + + p = re.compile(r"^abc$") + + m = re.fullmatch(p, "abc") + assert m != None, "compiled ^abc$ fullmatch" + + m = re.search(p, "abc") + assert m != None, "compiled ^abc$ search exact" + + m = re.search(p, "xabc") + assert m == None, "compiled ^abc$ search reject prefix" + + m = re.match(p, "abc") + assert m != None, "compiled ^abc$ match exact" + + m = re.match(p, "abcx") + assert m == None, "compiled ^abc$ match reject trailing" + + # ── Malformed patterns (pattern errors) ────────────────────────── + # Our pipeline returns exception(RePatternError(...)) for genuinely + # malformed patterns, modeling Python's re.error. + # The solver proves exception(...) != from_none(), so these pass. + + m = re.fullmatch(r"(abc", "abc") + assert m != None, "malformed: unmatched paren is exception, not None" + + m = re.fullmatch(r"a**", "a") + assert m != None, "malformed: nothing to repeat is exception, not None" + + m = re.fullmatch(r"x{100,2}", "x") + assert m != None, "malformed: bad bounds is exception, not None" + + m = re.search(r"(abc", "xabcx") + assert m != None, "malformed: search with bad pattern is exception, not None" + + m = re.match(r"a**", "aaa") + assert m != None, "malformed: match with bad pattern is exception, not None" + +if __name__ == "__main__": + main()