Rename Cretonne to Cranelift!
This commit is contained in:
@@ -1,4 +1,4 @@
|
||||
"""Definitions for the semantics segment of the Cretonne language."""
|
||||
"""Definitions for the semantics segment of the Cranelift language."""
|
||||
from cdsl.ti import TypeEnv, ti_rtl, get_type_env
|
||||
from cdsl.operands import ImmediateKind
|
||||
from cdsl.ast import Var
|
||||
|
||||
@@ -1,7 +1,7 @@
|
||||
"""
|
||||
Tools to elaborate a given Rtl with concrete types into its semantically
|
||||
equivalent primitive version. Its elaborated primitive version contains only
|
||||
primitive cretonne instructions, which map well to SMTLIB functions.
|
||||
primitive cranelift instructions, which map well to SMTLIB functions.
|
||||
"""
|
||||
from .primitives import GROUP as PRIMITIVES, prim_to_bv, prim_from_bv
|
||||
from cdsl.xform import Rtl
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
"""
|
||||
Cretonne primitive instruction set.
|
||||
Cranelift primitive instruction set.
|
||||
|
||||
This module defines a primitive instruction set, in terms of which the base set
|
||||
is described. Most instructions in this set correspond 1-1 with an SMTLIB
|
||||
@@ -26,9 +26,9 @@ y = Operand('x', BV, doc="A semantic value Y (same width as X)")
|
||||
a = Operand('a', BV, doc="A semantic value A (same width as X)")
|
||||
cond = Operand('b', TypeVar.singleton(b1), doc='A b1 value')
|
||||
|
||||
real = Operand('real', Real, doc="A real cretonne value")
|
||||
real = Operand('real', Real, doc="A real cranelift value")
|
||||
fromReal = Operand('fromReal', Real.to_bitvec(),
|
||||
doc="A real cretonne value converted to a BV")
|
||||
doc="A real cranelift value converted to a BV")
|
||||
|
||||
#
|
||||
# BV Conversion/Materialization
|
||||
|
||||
@@ -186,14 +186,16 @@ def equivalent(r1, r2, inp_m, out_m):
|
||||
(q1, m1) = to_smt(r1)
|
||||
(q2, m2) = to_smt(r2)
|
||||
|
||||
# Build an expression for the equality of real Cretone inputs of r1 and r2
|
||||
# Build an expression for the equality of real Cranelift inputs of
|
||||
# r1 and r2
|
||||
args_eq_exp = [] # type: List[ExprRef]
|
||||
|
||||
for (v1, v2) in inp_m.items():
|
||||
assert isinstance(v2, Var)
|
||||
args_eq_exp.append(mk_eq(m1[v1], m2[v2]))
|
||||
|
||||
# Build an expression for the equality of real Cretone outputs of r1 and r2
|
||||
# Build an expression for the equality of real Cranelift outputs of
|
||||
# r1 and r2
|
||||
results_eq_exp = [] # type: List[ExprRef]
|
||||
for (v1, v2) in out_m.items():
|
||||
assert isinstance(v2, Var)
|
||||
|
||||
Reference in New Issue
Block a user