QPQ-AG/sophia
10
0
Fork 0
Code Issues 41 Pull Requests 5 Actions Packages Projects Releases 16 Wiki Activity

Upgraded weakening and constraint anns

Browse Source
This commit is contained in:
radrow 2021-09-11 16:37:29 +02:00
parent 0ca23009b4
commit 737673ffe5
3 changed files with 36 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
src/aeso_ast_refine_types.erl
View File

@ -1211,7 +1211,7 @@ constr_expr(Env, ?typed_p(Expr, Type), S0) ->
{ExprT, S1} = constr_expr(Env, Expr, Base, S0),
{ExprT,
%% Inferred type <: Declared type, because the user can generalize Cat to Animal
[ {subtype, constr_id(typed), ?ann_of(Type), Env, ExprT, DType}
[ {subtype, constr_id(typed), ?ann_of(ExprT), Env, ExprT, DType}
, {well_formed, constr_id(typed), Env, DType}
| S1
]
@ -2191,7 +2191,7 @@ valid_in({subtype, _Ref, Ann, Env,
true;
false ->
%?DBG("~s -> ~s", [name(SupId), name(SubId)]),
%?DBG("CONTRADICT ON ~p \n~s\n<:\n~s", [_Ref, aeso_pretty:pp(predicate, strip_typed(pred_of(Assg, Env) ++ AssumpPred)), aeso_pretty:pp(predicate, strip_typed(ConclPred))]),
?DBG("CONTRADICT ON ~p \n~s\n<:\n~s", [_Ref, aeso_pretty:pp(predicate, strip_typed(pred_of(Assg, Env) ++ AssumpPred)), aeso_pretty:pp(predicate, strip_typed(ConclPred))]),
%?DBG("IN\n~s", [aeso_pretty:pp(predicate, strip_typed(pred_of(Assg, Env1)))]),
SimpAssump = simplify_pred(Assg, Env1,
pred_of(Assg, Env1) ++ AssumpPred),
@ -2228,9 +2228,13 @@ weaken({subtype, _Ref, _, Env,
AssumpPred = apply_subst(SubId, Id, SubPred),
Env1 = bind_var(Id, Base, Env),
Filtered =
partial_impl_assump(
Assg, Env1, AssumpPred,
fun() ->
[Q || Q <- Pred,
impl_holds(Assg, Env1, AssumpPred, apply_subst([{SupId, Id}|Subst], Q))
],
partial_impl_holds(apply_subst([{SupId, Id}|Subst], Q))
]
end),
%% ?DBG("WEAKENED (~s <: ~s --> ~s) ~p\nUNDER\n~s\nFROM\n~s\nTO\n~s", [name(SubId), name(SupId), name(Id), _Ref, aeso_pretty:pp(predicate, AssumpPred), aeso_pretty:pp(predicate, Pred), aeso_pretty:pp(predicate, Filtered)]),
NewLtinfo = Ltinfo#ltinfo{
predicate = Filtered
@ -2365,13 +2369,24 @@ impl_holds(Assg, Env, Assump, Concl) when not is_list(Concl) ->
impl_holds(Assg, Env, Assump, [Concl]);
impl_holds(_, _, _, []) -> true;
impl_holds(Assg, Env, Assump, Concl) ->
ConclExpr = {app, ?ann(), {'&&', ?ann()}, Concl}, %% Improper Sophia expr but who cares
partial_impl_assump(Assg, Env, Assump, fun() -> partial_impl_holds(Concl) end).
partial_impl_assump(Assg, Env, Assump, Callback) ->
aeso_smt:scoped(
fun() ->
declare_type_binds(Assg, Env),
[ aeso_smt:assert(expr_to_smt(Expr))
|| Expr <- Assump
],
Callback()
end).
partial_impl_holds([]) -> true;
partial_impl_holds(E) when not is_list(E) -> partial_impl_holds([E]);
partial_impl_holds(Concl) ->
aeso_smt:scoped(
fun() ->
ConclExpr = {app, ?ann(), {'&&', ?ann()}, Concl}, %% Improper Sophia expr but who cares
aeso_smt:assert(expr_to_smt(?op(?ann(), '!', ConclExpr))),
case aeso_smt:check_sat() of
{error, Err} -> throw({smt_error, Err});

3
src/aeso_parser.erl
View File

@ -85,7 +85,8 @@ mk_error({Pos, include_error, File}) ->
mk_p_err(Pos, Msg).
mk_pos({Line, Col}) -> aeso_errors:pos(Line, Col);
mk_pos({File, Line, Col}) -> aeso_errors:pos(File, Line, Col).
mk_pos({File, Line, Col}) -> aeso_errors:pos(File, Line, Col);
mk_pos([H|T]) -> try mk_pos(H) catch _:_ -> mk_pos(T) end.
%% -- Parsing rules ----------------------------------------------------------

16
test/contracts/hagia/simple.aes
View File

@ -1,5 +1,15 @@
contract XD =
contract DoubleStore =
type state = {x1 : int | x1 >= 0} * {x2 : int | x2 >= 0}
entrypoint gasdas() = 123
function f() = Some(() => ())
stateful entrypoint withdraw(amount : int) =
require(amount > 0 && amount =< Contract.balance, "INVALID_AMOUNT")
let (s1, s2) = state
if(amount =< s1 && Call.caller == ak_2nqfyixM9K5oKApAroETHEV4rxTTCAhAJvjYcUV3PF1326LUsx)
put((s1 - amount, s2))
Chain.spend(Call.caller, amount)
elif(amount =< s1 && Call.caller == ak_2CvLDbcJaw3CkyderTCgahzb6LpibPYgeodmCGcje8WuV5kiXR)
put((s1, s2 - amount))
Chain.spend(Call.caller, amount)
else
abort("INVALID_WITHDRAW")