Richard Smith b4418e29ec Properly check that a constraint appears after `is`. (#2304) 3 år sedan
..
BUILD 9feff92f22 Track witnesses wherever possible (#2263) 3 år sedan
README.md 873e78f605 cleanup and docs for tracing output (#1320) 3 år sedan
action.cpp 04d49cebd8 Consistently use a `Witness` rather than an expression to represent a possibly-symbolic witness. (#2245) 3 år sedan
action.h 04d49cebd8 Consistently use a `Witness` rather than an expression to represent a possibly-symbolic witness. (#2245) 3 år sedan
action_stack.cpp 8f0f69b65f Remove RuntimeError / CompilationError. (#2258) 3 år sedan
action_stack.h 04d49cebd8 Consistently use a `Witness` rather than an expression to represent a possibly-symbolic witness. (#2245) 3 år sedan
address.h 066b103881 Spelling (#1580) 3 år sedan
builtins.cpp 8f0f69b65f Remove RuntimeError / CompilationError. (#2258) 3 år sedan
builtins.h 69d4363ea5 Adds division to multiplicative expression. (#2091) 3 år sedan
dictionary.h 20728dbd3a CARBON_ header guards (#1261) 4 år sedan
exec_program.cpp 8f0f69b65f Remove RuntimeError / CompilationError. (#2258) 3 år sedan
exec_program.h 8f0f69b65f Remove RuntimeError / CompilationError. (#2258) 3 år sedan
field_path.h 663ed32b1b Initial support for associated constants (#1376) 3 år sedan
heap.cpp 8f0f69b65f Remove RuntimeError / CompilationError. (#2258) 3 år sedan
heap.h 52ee050019 Initial implementation of unformed state for local variables. (#1387) 3 år sedan
heap_allocation_interface.h 20728dbd3a CARBON_ header guards (#1261) 4 år sedan
impl_scope.cpp 4b679510e7 Check equality constraints when checking whether a constraint is satisfied (#2294) 3 år sedan
impl_scope.h 4b679510e7 Check equality constraints when checking whether a constraint is satisfied (#2294) 3 år sedan
interpreter.cpp 4b679510e7 Check equality constraints when checking whether a constraint is satisfied (#2294) 3 år sedan
interpreter.h e4a2d0f047 Addr Keyword Implementation (#1255) 3 år sedan
pattern_analysis.cpp 0191e2e41e implement checking for pattern match exhaustiveness and for unreachable cases (#2164) 3 år sedan
pattern_analysis.h 0191e2e41e implement checking for pattern match exhaustiveness and for unreachable cases (#2164) 3 år sedan
resolve_control_flow.cpp 7f7b9a4086 Implement support for `extends` and `impl as` declarations in interfaces (#2279) 3 år sedan
resolve_control_flow.h 20728dbd3a CARBON_ header guards (#1261) 4 år sedan
resolve_names.cpp 7f7b9a4086 Implement support for `extends` and `impl as` declarations in interfaces (#2279) 3 år sedan
resolve_names.h 20728dbd3a CARBON_ header guards (#1261) 4 år sedan
resolve_unformed.cpp 7f7b9a4086 Implement support for `extends` and `impl as` declarations in interfaces (#2279) 3 år sedan
resolve_unformed.h b28fd7ebc9 Implement more flows on unformed static analysis (#1923) 3 år sedan
stack.h 20728dbd3a CARBON_ header guards (#1261) 4 år sedan
type_checker.cpp b4418e29ec Properly check that a constraint appears after `is`. (#2304) 3 år sedan
type_checker.h 4b679510e7 Check equality constraints when checking whether a constraint is satisfied (#2294) 3 år sedan
value.cpp 4b679510e7 Check equality constraints when checking whether a constraint is satisfied (#2294) 3 år sedan
value.h 4b679510e7 Check equality constraints when checking whether a constraint is satisfied (#2294) 3 år sedan

README.md

explorer execution

The code in this directory defines all phases of program execution after parsing, including typechecking, name resolution, and execution. The overall flow can be found in ExecProgram, which executes each phase in sequence.

The Carbon abstract machine

Execution is specified in terms of an abstract machine, which executes minimal program steps in a loop until the program terminates. The state of the Carbon program (including the stack as well as the heap) is represented explicitly in C++ data structures, rather than implicitly in the C++ call stack. The Interpreter class represents an instance of the abstract machine, and is responsible for maintaining those data structures and implementing the steps of abstract machine execution.

The control-flow state of the abstract machine is encapsulated in an ActionStack object, which a represents a stack of Actions. An Action represents a self-contained computation (such as evaluation of an expression or execution of a statement) as a state machine, and the abstract machine proceeds by repeatedly executing the next state transition of the Action at the top of the stack. Executing a step may modify the internal state of the Action, and may also modify the Action stack, for example by pushing a new Action onto it. When an Action is done executing, it can optionally produce a value as its result, which is made available to the Action below it on the stack.

Carbon values are represented as Value objects, both at compile time and at run time. Note that in Carbon, a type is a kind of value, so types are represented as Values. More subtly, Value can also represent information that isn't a true Carbon value, but needs to be propagated through channels that use Value. Most notably, certain kinds of Value are used to represent the result of "evaluating" a Pattern, which evaluates all the subexpressions nested within it, while preserving the structure of the non-expression parts for use in pattern matching.

Values are always immutable. The abstract machine's mutable memory is represented using the Heap class, which is essentially a mapping of Addresses to Values.

Example

To evaluate the expression ((1 + 2) + 4), the interpreter starts by pushing an Action onto the stack that corresponds to the whole expression:

((1 + 2) + 4) .0. ## ...

In this notation, we're expressing the stack as a sequence of Actions separated by ##, with the top at the left, and representing each Action as the expression it evaluates, followed by its state. An Action consists of:

  • The syntax for the part of the program being executed, in this case ((1 + 2) + 4).
  • An integer pos for position, which is initially 0 and usually counts the number of steps executed. Here that's denoted with a number between two periods.
  • A vector results, which collects the results of any sub-Actions spawned by the Action. Above the results are omitted because they are currently empty.
  • A scope mapping variables to their values, for those variables whose lifetimes are associated with this action.

Then the interpreter proceeds by repeatedly taking the next step of the Action at the top of the stack. For expression Actions, pos typically identifies the operand that the next step should begin evaluation of. In this case, that operand is the expression (1 + 2), so we push a new Action onto the stack, and increment pos on the old one:

(1 + 2) .0. ## ((1 + 2) + 4) .1. ## ...

The next step spawns an action to evaluate 1:

1 .0. ## (1 + 2) .1. ## ((1 + 2) + 4) .1. ## ...

That expression can be fully evaluated in a single step, so the next step evaluates it, appends the result to the next Action down the stack, and pops the now-completed Action off the stack:

(1 + 2) .1. [[1]] ## ((1 + 2) + 4) .1. ## ...

The result 1 has been stored in the results list of the top Action, which is displayed between [[ and ]]. The top Action's pos is 1, so the next step begins evaluation of the second operand:

2 .0. ## (1 + 2) .2. [[1]] ## ((1 + 2) + 4) .1. ## ...

Which again can be evaluated immediately:

(1 + 2) .2. [[1, 2]] ## ((1 + 2) + 4) .1. ## ...

This expression has two operands, so now that pos is 2, all operands have been evaluated, and their results are in the corresponding entries of results. Thus, the next step can compute the expression value, passing it down to the parent Action and popping the completed action as before:

((1 + 2) + 4) .1. [[3]] ## ...

Evaluation now proceeds to the second operand:

4 .0. ## ((1 + 2) + 4) .2. [[3]] ## ...

Which, again, can be evaluated immediately:

((1 + 2) + 4) .2. [[3, 4]] ## ...

pos now indicates that all subexpressions have been evaluated, so the next step computes the final result of 7.