Fix missing case in semantics for string replace function (#3910)

fixes: #3896 --------- Co-authored-by: rv-jenkins <[email protected]>
runtimeverification · Jan 22, 2024 · 2743d63 · 2743d63
1 parent ef0eb64
commit 2743d63
Showing 1 changed file with 6 additions and 2 deletions.
diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md
@@ -1881,11 +1881,15 @@ of the above operations in K.
         requires findString(Source, ToReplace, 0) <Int 0
 
 
+  // Note that the replace function is undefined when Count < 0. This allows different backends to
+  // implement their own behavior without contradicting these semantics. For instance, a symbolic
+  // backend can return #Bottom for that case, while a concrete backend can throw an exception.
   rule replace(Source:String, ToReplace:String, Replacement:String, Count:Int) =>
        substrString(Source, 0, findString(Source, ToReplace, 0)) +String Replacement +String
        replace(substrString(Source, findString(Source, ToReplace, 0) +Int lengthString(ToReplace), lengthString(Source)), ToReplace, Replacement, Count -Int 1)
-        requires Count >Int 0
-  rule replace(Source:String, _, _, 0) => Source
+        requires Count >Int 0 andBool findString(Source, ToReplace, 0) >=Int 0
+  rule replace(Source:String, _, _, Count) => Source
+        requires Count >=Int 0 [owise]
   rule replaceAll(Source:String, ToReplace:String, Replacement:String) => replace(Source, ToReplace, Replacement, countAllOccurrences(Source, ToReplace))
 
 endmodule