# Modelling regex replacement via a DFA

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?

Depending on the exact semantics of the replace operation (regarding multiple matches, overlapping matches, etc.), it can likely be modelled as a finite-state transducer. The set of possible values of s can be modelled as a regular language. It is known that the application of a finite-state transducer to a regular language gives you another regular language, and there are standard algorithms for computing it, using the product construction.