How to create model for a powerful language whose programs are guaranteed to terminate?

I'm creating a powerful regular expression matching system that can be augmented by adding small microprograms to deterministic finite automaton (DFA) states. The microprogram solves the big bang issue where a rule of the form .*ab.*cd doubles the state count of the DFA.

The solution for the "big bang" problem is to create a program-augmented-DFA like this:

.*ab
{
var=1;
}
.*cd
{
if (var)
{
raise();
}
}


Now, a problem with programming languages in general is that programs written in nontrivial languages may end up in infinite loop or in infinite recursion. Thus, I'm planning to implement a bytecode where backwards jumps are strictly forbidden but forwards jumps are allowed. The bytecode would contain the following opcodes:

• EXIT, RAISE
• PUSH_BYTE, PUSH_WORD, PUSH_DWORD, PUSH_QWORD
• EQ, NE, LT, GT, LE, GE for equality and inequality
• LOGICAL_AND, LOGICAL_NOT, LOGICAL_OR, BITWISE_AND, BITWISE_OR, BITWISE_XOR, BITWISE_NOT
• SHL, SHR
• ADD, SUB, MUL, DIV, MOD, UNARY_MINUS
• JMP_FWD, IF_FALSE_JUMP_FWD for nonconditional and conditional jumps (only forwards)
• NOP for padding
• SET_VAR for setting a variable in the variable structure
• PUSH_VAR for pushing a variable in the variable structure into stack
• POP and POP_MANY for popping variables from the stack
• perhaps some other opcodes like for ++, --, += operators etc.

The additional data structures accessed by programs are the variable structure (permanent) and stack (nonpermanent). Nonnegative variables (0, 1, 2, 3, ...) are in the variable structure and negative variables (-1, -2, -3, -4, ...) refer to the stack. So, in the example .*ab / .*cd program, var would be in the variable structure as it's permanent.

I have already verified that arbitrary logical expressions and complex if-else structures can be implemented in this bytecode.

Is there some kind of formal model for bytecodes whose microprograms always are guaranteed to terminate?

Note function calls are missing. Would the language become more powerful if I allowed function calls forwards, but never function calls backwards (thus making recursion impossible)? If the program can manipulate the stack, I assume a secondary stack for just instruction pointer return locations would be needed. Would such a secondary stack that cannot be manipulated allow supporting function calls in a language whose programs are guaranteed to terminate?

At least without function calls I know that there is an upper bound for the stack size: if one instruction can push at most one item into the stack, if there are N instructions, an upper bound for the stack size is N. Would the upper bound change if function calls were supported?

Also, without function calls, a program of N instructions takes at most N cycles. Would this change if function calls were supported? For example, would it be possible to have a program with N instructions that takes $$2^N$$ cycles to execute?

As practical example of a similar language, my online search found this that may be applicable: https://en.wikipedia.org/wiki/Sieve_(mail_filtering_language)

• Take a look at bloop. – Pål GD Jan 20 at 14:16