CristalCaveGem » LustreC

#include <mpfr.h>

#include "mpfr_lustre.h"

void MPFR_LUSTRE_INIT () {

  return;

}

void MPFR_LUSTRE_CLEAR () {

  return;

}

void MPFRNeq_step (mpfr_t i1, mpfr_t i2, 

                          _Bool (*out)

                          )

{

  *out = mpfr_lessgreater_p(i1, i2);

}

void MPFREq_step (mpfr_t i1, mpfr_t i2, 

                         _Bool (*out)

                         )

{

  *out = mpfr_equal_p(i1, i2);

}

void MPFRGt_step (mpfr_t i1, mpfr_t i2, 

                         _Bool (*out)

                         )

{

  *out = mpfr_greater_p(i1, i2);

}

void MPFRGe_step (mpfr_t i1, mpfr_t i2, 

                         _Bool (*out)

                         )

{

  *out = mpfr_greaterequal_p(i1, i2);

}

extern void MPFRLt_step (mpfr_t i1, mpfr_t i2, 

                         _Bool (*out)

                         )

{

  *out = mpfr_less_p(i1, i2);

}

void MPFRLe_step (mpfr_t i1, mpfr_t i2, 

                         _Bool (*out)

                         )

{

  *out = mpfr_lessequal_p(i1, i2);

}

void MPFRDiv_step (mpfr_t i1, mpfr_t i2, 

                          mpfr_t out

                          )

{

  mpfr_div(out, i1, i2, MPFR_RNDN);

}

void MPFRTimes_step (mpfr_t i1, mpfr_t i2, 

                            mpfr_t out

                            )

{

  mpfr_mul(out, i1, i2, MPFR_RNDN);

}

void MPFRMinus_step (mpfr_t i1, mpfr_t i2, 

                            mpfr_t out

                            )

{

  mpfr_sub(out, i1, i2, MPFR_RNDN);

}

void MPFRPlus_step (mpfr_t i1, mpfr_t i2, 

                           mpfr_t out

                           )

{

  mpfr_add(out, i1, i2, MPFR_RNDN);

}

void MPFRUminus_step (mpfr_t i, 

                             mpfr_t out

                             )

{

  mpfr_neg(out, i, MPFR_RNDN);

}

void MPFRInit(mpfr_t i, mpfr_prec_t prec)

{

  mpfr_init2(i, prec);

}

void MPFRClear(mpfr_t i)

{

  mpfr_clear(i);

}

function MPFRUminus(i: real) returns (out: real) lib gmp lib mpfr;

function MPFRPlus(i1, i2: real) returns (out: real);

function MPFRMinus(i1, i2: real) returns (out: real);

function MPFRTimes(i1, i2: real) returns (out: real);

function MPFRDiv(i1, i2: real) returns (out: real);

function MPFRLe(i1, i2: real) returns (out: bool);

function MPFRLt(i1, i2: real) returns (out: bool);

function MPFRGe(i1, i2: real) returns (out: bool);

function MPFRGt(i1, i2: real) returns (out: bool);

function MPFREq(i1, i2: real) returns (out: bool);

function MPFRNeq(i1, i2: real) returns (out: bool);

let type_env : (Types.type_expr Env.t) ref = ref Env.initial

let clock_env : (Clocks.clock_expr Env.t) ref = ref Env.initial

let basename = ref ""

let main_node = ref ""

module TypeEnv =

struct

let lookup_value ident = Env.lookup_value !type_env ident

let exists_value ident = Env.exists_value !type_env ident

let iter f = Env.iter !type_env f

let pp pp_fun fmt () = Env.pp_env pp_fun fmt !type_env

end

let initialize () =

  begin

    main_node := !Options.main_node;

  end

(* Local Variables: *)

(* compile-command:"make -C .." *)

(* End: *)

(********************************************************************)

(*                                                                  *)

(*  The LustreC compiler toolset   /  The LustreC Development Team  *)

(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)

(*                                                                  *)

(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)

(*  under the terms of the GNU Lesser General Public License        *)

(*  version 2.1.                                                    *)

(*                                                                  *)

(********************************************************************)

open Utils

open LustreSpec

open Corelang

open Normalization

open Machine_code

let mpfr_module = mktop (Open(false, "mpfr_lustre"))

let mpfr_rnd () = "MPFR_RNDN"

let mpfr_prec () = !Options.mpfr_prec

let inject_id = "MPFRId"

let inject_copy_id = "mpfr_set"

let inject_real_id = "mpfr_set_flt"

let inject_init_id = "mpfr_init2"

let inject_clear_id = "mpfr_clear"

let mpfr_t = "mpfr_t"

let unfoldable_value value =

  not (Types.is_real_type value.value_type && is_const_value value)

let inject_id_id expr =

  let e = mkpredef_call expr.expr_loc inject_id [expr] in

  { e with

    expr_type = Type_predef.type_real;

    expr_clock = expr.expr_clock;

  }

let pp_inject_real pp_var pp_val fmt var value =

  Format.fprintf fmt "%s(%a, %a, %s);"

    inject_real_id

    pp_var var

    pp_val value

    (mpfr_rnd ())

let inject_assign expr =

  let e = mkpredef_call expr.expr_loc inject_copy_id [expr] in

  { e with

    expr_type = Type_predef.type_real;

    expr_clock = expr.expr_clock;

  }

let pp_inject_copy pp_var fmt var value =

  Format.fprintf fmt "%s(%a, %a, %s);"

    inject_copy_id

    pp_var var

    pp_var value

    (mpfr_rnd ())

let rec pp_inject_assign pp_var fmt var value =

  if is_const_value value

  then

    pp_inject_real pp_var pp_var fmt var value

  else

    pp_inject_copy pp_var fmt var value

let pp_inject_init pp_var fmt var =

  Format.fprintf fmt "%s(%a, %i);"

    inject_init_id

    pp_var var

    (mpfr_prec ())

let pp_inject_clear pp_var fmt var =

  Format.fprintf fmt "%s(%a);"

    inject_clear_id

    pp_var var

let base_inject_op id =

  match id with

  | "+"      -> "MPFRPlus"

  | "-"      -> "MPFRMinus"

  | "*"      -> "MPFRTimes"

  | "/"      -> "MPFRDiv"

  | "uminus" -> "MPFRUminus"

  | "<="     -> "MPFRLe"

  | "<"      -> "MPFRLt"

  | ">="     -> "MPFRGe"

  | ">"      -> "MPFRGt"

  | "="      -> "MPFREq"

  | "!="     -> "MPFRNeq"

  | _        -> raise Not_found

let inject_op id =

  try

    base_inject_op id

  with Not_found -> id

let homomorphic_funs =

  List.fold_right (fun id res -> try base_inject_op id :: res with Not_found -> res) Basic_library.internal_funs []

let is_homomorphic_fun id =

  List.mem id homomorphic_funs

let inject_call expr =

  match expr.expr_desc with

  | Expr_appl (id, args, None) when not (Basic_library.is_expr_internal_fun expr) ->

    { expr with expr_desc = Expr_appl (inject_op id, args, None) }

  | _ -> expr

let expr_of_const_array expr =

  match expr.expr_desc with

  | Expr_const (Const_array cl) ->

    let typ = Types.array_element_type expr.expr_type in

    let expr_of_const c =

      { expr_desc = Expr_const c;

	expr_type = typ;

	expr_clock = expr.expr_clock;

	expr_loc = expr.expr_loc;

	expr_delay = Delay.new_var ();

	expr_annot = None;

	expr_tag = new_tag ();

      }

    in { expr with expr_desc = Expr_array (List.map expr_of_const cl) }

  | _                           -> assert false

(* inject_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *)

let rec inject_list alias node inject_element defvars elist =

  List.fold_right

    (fun t (defvars, qlist) ->

      let defvars, norm_t = inject_element alias node defvars t in

      (defvars, norm_t :: qlist)

    ) elist (defvars, [])

let rec inject_expr ?(alias=true) node defvars expr =

let res=

  match expr.expr_desc with

  | Expr_const (Const_real _)  -> mk_expr_alias_opt alias node defvars expr

  | Expr_const (Const_array _) -> inject_expr ~alias:alias node defvars (expr_of_const_array expr)

  | Expr_const (Const_struct _) -> assert false

  | Expr_ident _

  | Expr_const _  -> defvars, expr

  | Expr_array elist ->

    let defvars, norm_elist = inject_list alias node (fun _ -> inject_expr ~alias:true) defvars elist in

    let norm_expr = { expr with expr_desc = Expr_array norm_elist } in

    defvars, norm_expr

  | Expr_power (e1, d) ->

    let defvars, norm_e1 = inject_expr node defvars e1 in

    let norm_expr = { expr with expr_desc = Expr_power (norm_e1, d) } in

    defvars, norm_expr

  | Expr_access (e1, d) ->

    let defvars, norm_e1 = inject_expr node defvars e1 in

    let norm_expr = { expr with expr_desc = Expr_access (norm_e1, d) } in

    defvars, norm_expr

  | Expr_tuple elist -> 

    let defvars, norm_elist =

      inject_list alias node (fun alias -> inject_expr ~alias:alias) defvars elist in

    let norm_expr = { expr with expr_desc = Expr_tuple norm_elist } in

    defvars, norm_expr

  | Expr_appl (id, args, r) ->

    let defvars, norm_args = inject_expr node defvars args in

    let norm_expr = { expr with expr_desc = Expr_appl (id, norm_args, r) } in

    mk_expr_alias_opt alias node defvars (inject_call norm_expr)

  | Expr_arrow _ -> defvars, expr

  | Expr_pre e ->

    let defvars, norm_e = inject_expr node defvars e in

    let norm_expr = { expr with expr_desc = Expr_pre norm_e } in

    defvars, norm_expr

  | Expr_fby (e1, e2) ->

    let defvars, norm_e1 = inject_expr node defvars e1 in

    let defvars, norm_e2 = inject_expr node defvars e2 in

    let norm_expr = { expr with expr_desc = Expr_fby (norm_e1, norm_e2) } in

    defvars, norm_expr

  | Expr_when (e, c, l) ->

    let defvars, norm_e = inject_expr node defvars e in

    let norm_expr = { expr with expr_desc = Expr_when (norm_e, c, l) } in

    defvars, norm_expr

  | Expr_ite (c, t, e) ->

    let defvars, norm_c = inject_expr node defvars c in

    let defvars, norm_t = inject_expr node defvars t in

    let defvars, norm_e = inject_expr node defvars e in

    let norm_expr = { expr with expr_desc = Expr_ite (norm_c, norm_t, norm_e) } in

    defvars, norm_expr

  | Expr_merge (c, hl) ->

    let defvars, norm_hl = inject_branches node defvars hl in

    let norm_expr = { expr with expr_desc = Expr_merge (c, norm_hl) } in

    defvars, norm_expr

in

(*Format.eprintf "inject_expr %B %a = %a@." alias Printers.pp_expr expr Printers.pp_expr (snd res);*)

res

and inject_branches node defvars hl =

 List.fold_right

   (fun (t, h) (defvars, norm_q) ->

     let (defvars, norm_h) = inject_expr node defvars h in

     defvars, (t, norm_h) :: norm_q

   )

   hl (defvars, [])

let rec inject_eq node defvars eq =

  let (defs', vars'), norm_rhs = inject_expr ~alias:false node defvars eq.eq_rhs in

  let norm_eq = { eq with eq_rhs = norm_rhs } in

  norm_eq::defs', vars'

(** normalize_node node returns a normalized node, 

    ie. 

    - updated locals

    - new equations

    - 

*)

let inject_node node = 

  cpt_fresh := 0;

  let inputs_outputs = node.node_inputs@node.node_outputs in

  let is_local v =

    List.for_all ((!=) v) inputs_outputs in

  let orig_vars = inputs_outputs@node.node_locals in

  let defs, vars = 

    List.fold_left (inject_eq node) ([], orig_vars) (get_node_eqs node) in

  (* Normalize the asserts *)

  let vars, assert_defs, asserts = 

    List.fold_left (

    fun (vars, def_accu, assert_accu) assert_ ->

      let assert_expr = assert_.assert_expr in

      let (defs, vars'), expr = 

	inject_expr 

	  ~alias:false 

	  node 

	  ([], vars) (* defvar only contains vars *)

	  assert_expr

      in

      vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu

    ) (vars, [], []) node.node_asserts in

  let new_locals = List.filter is_local vars in

  (* Compute traceability info: 

     - gather newly bound variables

     - compute the associated expression without aliases     

  *)

  (* let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals)) new_locals in *)

  let node =

  { node with 

    node_locals = new_locals; 

    node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);

  }

  in ((*Printers.pp_node Format.err_formatter node;*) node)

let inject_decl decl =

  match decl.top_decl_desc with

  | Node nd ->

    {decl with top_decl_desc = Node (inject_node nd)}

  | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl

let inject_prog decls = 

  List.map inject_decl decls

(* Local Variables: *)

(* compile-command:"make -C .." *)

(* End: *)

open LustreSpec

module type PluginType =

sig

end

let inline_annots rename_var_fun annot_list =

  List.map (

    fun ann -> 

      { ann with 

	annots = List.fold_left (

	  fun accu (sl, eexpr) -> 

	    let items = 

	      match sl with 

	      | plugin_name::args -> 

		if plugin_name = "salsa" then

		  match args with

		  | ["ranges";varname] -> 

		    [["salsa";"ranges";(rename_var_fun varname)], eexpr]

		  | _ -> [(sl, eexpr)]

		else

		  [(sl, eexpr)]

	    | _ -> assert false

	    in

	    items@accu

	) [] ann.annots

      }

  ) annot_list

(* Local Variables: *)

(* compile-command:"make -C .." *)

(* End: *)

#!/bin/bash

eval set -- $(getopt -n $0 -o "-aciwvh:" -- "$@")

declare c i w h a v

declare -a files

SRC_PREFIX=@SRC_PATH@-tests/

#SRC_PREFIX=`svn info --xml | grep wcroot | sed "s/<[^>]*>//g"`/lustre_compiler

NOW=`date "+%y%m%d%H%M"`

report=`pwd`/report-@PACKAGE_VERSION@-$NOW

LUSTREC=lustrec

mkdir -p build

build=`pwd`"/build"

gcc_compile() {

    if [ $verbose -gt 1 ]; then

	echo "gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ $1.c > /dev/null"

    fi

    gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$1".c > /dev/null;

    if [ $? -ne 0 ]; then

	rgcc="INVALID";

    else

	rgcc="VALID"

    fi

}

lustrec_compile() {

    if [ $verbose -gt 1 ]; then

       echo "$LUSTREC $@"

    fi

    $LUSTREC "$@";

    if [ $? -ne 0 ]; then

        rlustrec="INVALID";

    else

        rlustrec="VALID"

    fi

}

base_compile() {

    while IFS=, read -r file main opts

    do

	name=`basename "$file" .lus`

        ext=".lus"

	if [ `dirname "$file"`/"$name" = "$file" ]; then

	    name=`basename "$file" .lusi`

	    ext=".lusi"

	fi

        dir=${SRC_PREFIX}/`dirname "$file"`

	pushd $dir > /dev/null

	if [ "$main" != "" ]; then

	    lustrec_compile -d $build -verbose 0 $opts -node $main $name$ext;

	else

	    lustrec_compile -d $build -verbose 0 $opts $name$ext

	fi

	pushd $build > /dev/null

	if [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then

            gcc_compile "$name";

	else

	    rgcc="NONE"

	fi

	popd > /dev/null

	popd > /dev/null

	if [ $verbose -gt 0 ]; then

	    echo "lustrec ($rlustrec), gcc($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;

	else

	    echo "lustrec ($rlustrec), gcc($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"

	fi;

    done < $file_list

}

inline_compile () {

    while IFS=, read -r file main opts

    do

	name=`basename "$file" .lus`

	ext=".lus"

	if [ `dirname "$file"`/"$name" = "$file" ]; then

	    name=`basename "$file" .lusi`

	    ext=".lusi"

	fi

	dir=${SRC_PREFIX}/`dirname "$file"`

	pushd $dir > /dev/null

	if [ "$main" != "" ]; then

	    lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name$ext;

	else

	    if [ "$ext" = ".lusi" ]; then

		lustrec_compile -d $build -verbose 0 $opts $name$ext;

	    else

		rlustrec="NONE"

		rgcc="NONE"

	    fi

	fi

	pushd $build > /dev/null

	if [ "$main" != "" ] && [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then

	    gcc_compile "$name";

	else

	    rgcc="NONE"

	fi

	popd > /dev/null

	popd > /dev/null

	if [ $verbose -gt 0 ]; then

	    echo "lustrec inlined ($rlustrec), gcc ($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;

	else

	    echo "lustrec inlined ($rlustrec), gcc ($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"

	fi;

    done < $file_list

}

inline_compile_with_check () {

# Checking inlining

    while IFS=, read -r file main opts

    do

	name=`basename "$file" .lus`

	ext=".lus"

	if [ `dirname "$file"`/"$name" = "$file" ]; then

	    name=`basename "$file" .lusi`

	    ext=".lusi"

	fi

	dir=${SRC_PREFIX}/`dirname "$file"`

	pushd $dir > /dev/null

	if [ "$main" != "" ]; then

	    lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name$ext;

	else

	    if [ "$ext" = ".lusi" ]; then

		lustrec_compile -d $build -verbose 0 $opts $name$ext;

	    else

		rlustrec="NONE"

		rgcc="NONE"

	    fi

	fi

	popd > /dev/null

	pushd $build > /dev/null

	if [ "$main" != "" ] && [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then

	    gcc_compile "$name";

	else

	    rgcc="NONE"

	fi

	# Cheching witness

	if [ "$main" != "" ] && [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then

	    mv ${name}_witnesses/inliner_witness.lus ${name}_inliner_witness.lus

	    lustrec_compile -verbose 0 -horn-traces -node check ${name}_inliner_witness.lus

	    z3="`z3 -T:10 ${name}_inliner_witness.smt2 | xargs`"

	    if [ "x`echo $z3 | grep -o unsat`" == "xunsat" ]; then

		rinlining="VALID";

	    elif [ "x`echo $z3 | xargs | grep -o error`" == "xerror" ]; then

		rinlining="ERROR";

	    elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then

		rinlining="UNKNOWN";

	    elif [ "x`echo $z3 | xargs | grep -o timeout`" == "xtimeout" ]; then

		rinlining="TIMEOUT"

	    else

		rinlining="INVALID"

	    fi

	else

	    rinlining="NONE"

	fi

	popd > /dev/null

	if [ $verbose -gt 0 ]; then

	    echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining check ($rinlining), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;

	else

	    echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining check ($rinlining), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "TIMEOUT\|INVALID\|ERROR\|UNKNOWN"

	fi

done < $file_list

}

check_prop () {

    while IFS=, read -r file main opts

    do

	name=`basename "$file" .lus`

	if [ "$name" = "$file" ]; then

	    return 0

	fi

	dir=${SRC_PREFIX}/`dirname "$file"`

	pushd $dir > /dev/null

    # Checking horn backend

    if [ "$main" != "" ]; then

	lustrec_compile -horn-traces -horn-query -d $build -verbose 0 $opts -node $main $name".lus";

    else

	lustrec_compile -horn-traces -horn-query -d $build -verbose 0 $opts $name".lus"

    fi

    # echo "z3 $build/$name".smt2 

    # TODO: This part of the script has to be optimized

    z3="`z3 -T:10 ${build}/${name}.smt2 | xargs`"

    if [ "x`echo $z3 | grep -o unsat`" == "xunsat" ]; then

	rhorn="VALID";

    elif [ "x`echo $z3 | xargs | grep -o error`" == "xerror" ]; then

	rhorn="ERROR";

    elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then

	rhorn="UNKNOWN";

    elif [ "x`echo $z3 | xargs | grep -o timeout`" == "xtimeout" ]; then

	rhorn="TIMEOUT"

    else

	rhorn="INVALID"

    fi

    if [ $verbose -gt 0 ]; then

	echo "lustrec ($rlustrec), horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;

    else

	echo "lustrec ($rlustrec), horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"

    fi

    popd > /dev/null

done < $file_list

}

usage () {

echo "usage: $0 [-aciwh] file_list"

echo "-a: perform all steps"

echo "-c: basic compilation"

echo "-i: compile with inline mode"

echo "-w: compile with inline mode. Check the inlining with z3"

echo "-h: check files with the horn-pdf backend (requires z3)"

echo "-v <int>: verbose level"

}

verbose=0

nobehavior=1

while [ $# -gt 0 ] ; do

        case "$1" in

	        -v) shift ; verbose="$1"; shift ;;

	        -a) nobehavior=0; c=1 ; w=1; h=1; shift ;;

                -c) nobehavior=0; c=1 ; shift ;;

                -i) nobehavior=0; i=1 ; shift ;;

                -w) nobehavior=0; w=1 ; shift ;;

                -h) nobehavior=0; h=1 ; shift ;;

                --) shift ;;

                -*) echo "bad option '$1'" ; exit 1 ;;

                *) files=("${files[@]}" "$1") ; shift ;;

         esac

done

file_list=${files[0]}

if [ ${#files} -eq 0 ] ; then

    echo input list required

    usage

    exit 1

fi

# cleaning directory $build

rm -f "$build"/* 2> /dev/null

# executing tests

[ ! -z "$c" ] && base_compile

[ ! -z "$i" ] && inline_compile

[ ! -z "$w" ] && inline_compile_with_check

[ ! -z "$h" ] && check_prop

[ "$nobehavior" -eq 1 ] && echo "Must provide an argument in [aciwh]" && usage

	# Removing Generated lusi file

	#grep generated ../${file}i > /dev/null

	#if [ $? -ne 1 ];then

	#  rm ../${file}i

	#fi