I wish to model the following common construction in code via a finite state automaton for the purposes of static analysis:
s = <string matching regex R1> t = s.replace(<regex R2>, <string matching regex R3>) # What is the set of possible strings of t?
More formally, given DFAs $R_1$, $R_2$, and $R_3$, I want to find some automaton $R_o$ that is the result of replacing substrings of $R_1$ that are accepted by $R_2$ by some string that is accepted by $R_3$.
Unfortunately, while the literature seems to discuss this, I am unable to pin down a precise implementation of this operation. In addition, I am having trouble even defining the set of strings that $R_o$ should accept. Does there exist an algorithm to solve this problem? Is it even solvable in general?